Analyzing Different Approaches for Key Constraint in Hotel Room Allocation

Each hotel guest has a set of keys and no two guests have the same key Roger L. Costello April 3, 2018

We want each room to have its own unique set of keys Keys for Room1 K3 K4 K5 K0 K1 K2 K6 Keys for Room0 Keys for Room2 K7 K8

keys Room0 K0 This declaration: Room0 K1 Room0 K2 sig Room {keys: set Key} Same key used in three rooms ouch! Room1 K0 Room1 K4 allows undesirable instances such as the one shown on the right. Notice that K0 is used by rooms 0, 1, and 2. Room1 K5 Room2 K0 Room2 K7 Room2 K8

sig Room {keys: set Key} We need to specify a constraint on the set of Key values.

Heres one approach to constraining keys pred DisjointKeySet { keys in Room lone -> Key } constrain sig Room {keys: set Key} Each Key value is associated to at most one Room.

Heres another approach sig Room {keys: disjset Key} Each room has a set of key and each set is disjoint.

Are the two approaches equivalent? I believe they are. To be certain, however, let s get the Alloy Analyzer to compare the two approaches and search for counterexamples. How to do this? How to write the proper assert?

The book Software Abstractions says (p. 274) equivalent sig S {f: disj e} sig S {f: e} pred Every_S_has_a_different_value_for_f { all a,b: S | a != b => no a.f & b.f }

Therefore, equivalent sig S {f: disj e} sig S {f: e} pred Every_S_has_a_different_value_for_f { all a,b: S | a != b => no a.f & b.f } equivalent sig Room {keys: disjset Key} sig Room {keys: set Key} pred Every_Room_has_a_different_set_of_keys{ all r, r': Room | r != r' => no r.keys & r'.keys }

sig Key {} sig Room { keys: set Key } pred DisjointKeySet_v1 { keys in Room lone -> Key } pred DisjointKeySet_v2 { all r, r': Room | r != r' => no r.keys & r'.keys } assert Equivalent { DisjointKeySet_v1 iff DisjointKeySet_v2 } check Equivalent