Understanding Set Properties in Alloy Modeling

Expressing set properties in Alloy Roger L. Costello March 29, 2018

Want to learn sets? Learn Alloy! Want to learn Alloy? Learn sets! Certain properties of binary relations are so frequently encountered that they have been given names, including reflexive, symmetric, transitive, and connected. All these apply only to relations in a set, i.e., in A x A, not to relations from A to B.

Reflexive property Given a set A and a relation R in A, R is reflexive if and only if all the ordered pairs of the form (x, x) are in R for every x in A. Example: Take the set A = { 1, 2, 3 } and the relation R1= { (1,1), (1,2), (2,2), (2,3), (3,3), (3,1) } in A. R1is reflexive because it contains the ordered pairs (1,1), (2,2), and (3,3). 1 2 3

Each person has the same birthday as themself Take the set A = the set of human beings and the relation R2 = has the same birthday . R2 is reflexive because it contains the ordered pairs: oRoger Costello has the same birthday as Stan Efferding. oRoger Costello has the same birthday as Roger Costello. oStan Efferding has the same birthday as Roger Costello. oStan Efferding has the same birthday as Stan Efferding. o R2 = { (Roger Costello, Stan Efferding), (Roger Costello, Roger Costello), (Stan Efferding, Roger Costello), (Stan Efferding,Stan Efferding), }

Alloy expression that constrains pairs of elem atoms to be reflexive sig A {} sig Test { R: A -> A } { (A <: iden) in R // Constrain R to be reflexive } assert isReflexive { all x: A | (x -> x) in Test.R } check isReflexive

iden Test0 A0 A1 A2 Test0 A0 A1 A2 sig A {} sig Test { R: A -> A } { (A <: iden) in R // Constrain R to be reflexive } assert isReflexive { all x: A | (x -> x) in Test.R } check isReflexive

Reflexive Symmetric Transitive Connected 1 3 4 1 2 3 1 2 8 2 1 2 7 3 3 6 4 5 Nonsymmetric Nontransitive Nonreflexive Nonconnected 3 4 3 1 2 1 2 1 2 1 8 2 3 7 3 Intransitive Asymmetric 6 Irreflexive 4 5 3 4 3 1 2 1 2 1 2 3

Injective Functional 1 2 1 2 3 4 3 5 Not Injective Not Functional 1 2 1 2 3 4 4

The ordering module We have used the ordering module to order sets, e.g., open util/ordering[Snapshot] // Order the set of Snapshots in the goat, cabbage, wolf model open util/ordering[House] // Order the set of Houses in the Einstein model open util/ordering[Desktop] // Order the set of Desktops in the Desktop model

The ordering module creates ordered pairs from your set When the ordering module is called with a set then all these functions are suddenly available on the set: first, last, next. first returns the first atom. last returns the last atom. next returns a set of pairs, such as this: next first returns the first Snapshot first.next returns the second Snapshot first.next.next returns the third Snapshot And so forth Snapshot0 Snapshot1 Snapshot1 Snapshot2 Snapshot2 Snapshot3

Snapshot Snapshot1 Snapshot3 Snapshot2 Snapshot0 Ordering Module first last next: Snapshot0 Snapshot1 Snapshot2 Snapshot3

Which of these properties do we want the relation (ordered pairs) to have? Reflexive Symmetric Transitive Connected 1 3 4 1 2 3 1 2 8 2 1 2 7 3 3 6 4 5 Nonsymmetric Nontransitive Nonreflexive Nonconnected 3 4 3 1 2 1 2 1 2 1 8 2 3 7 3 Intransitive Asymmetric 6 4 Irreflexive 5 3 4 3 1 2 1 2 1 2 3

Which of these properties do we want the relation (ordered pairs) to have? Reflexive Symmetric Transitive Connected 1 3 4 1 2 3 1 2 8 2 1 2 7 3 3 6 4 5 Nonsymmetric Nontransitive Nonreflexive Nonconnected 3 4 3 1 2 1 2 1 2 1 8 2 3 7 3 Intransitive Asymmetric 6 4 Irreflexive 5 3 4 3 1 2 1 2 1 2 3

Injective Functional 1 2 1 2 3 4 3 5 Not Injective Not Functional 1 2 1 2 3 4 4

sig A {} onesig Ord { First: A, Next: A -> A } { no x: A | (x -> First) in Next // First is the first atom in the list irreflexive [A, Next] // Constrain Next to be irreflexive intransitive [A, Next] // Constrain Next to be intransitive asymmetric [A, Next] // Constrain Next to be asymmetric nonconnected [A, Next] // Constrain Next to be non-connected injective [A, Next] // Constrain Next to be injective functional [A, Next] // Constrain Next to be functional #Next = minus[#A, 1] // Constraint Next to contain all atoms in A }

Hold on! The ordering module also creates a prev function The prev function allows you to traverse to the previous atom in the list. The below graphic is not accurate, how should it be changed? first last next: Snapshot0 Snapshot1 Snapshot2 Snapshot3

Arrows must go both directions first last prev next Snapshot0 Snapshot1 Snapshot2 Snapshot3

Now which of these properties do we want the relation (ordered pairs) to have? Reflexive Symmetric Transitive Connected 1 3 4 1 2 3 1 2 8 2 1 2 7 3 3 6 4 5 Nonsymmetric Nontransitive Nonreflexive Nonconnected 3 4 3 1 2 1 2 1 2 1 8 2 3 7 3 Intransitive Asymmetric 6 4 Irreflexive 5 3 4 3 1 2 1 2 1 2 3

Which of these properties do we want the relation (ordered pairs) to have? Reflexive Symmetric Transitive Connected 1 3 4 1 2 3 1 2 8 2 1 2 7 3 3 6 4 5 Nonsymmetric Nontransitive Nonreflexive Nonconnected 3 4 3 1 2 1 2 1 2 1 8 2 3 7 3 Intransitive Asymmetric 6 4 Irreflexive 5 3 4 3 1 2 1 2 1 2 3

Injective Functional 1 2 1 2 3 4 3 5 Not Injective Not Functional 1 2 1 2 3 4 4

sig A {} onesig Ord { First: A, Next: A -> A } { no x: A | (x -> First) in Next // First is the first atom in the list irreflexive [A, Next] // Constrain Next to be irreflexive intransitive [A, Next] // Constrain Next to be intransitive symmetric [A, Next] // Constrain Next to be symmetric nonconnected [A, Next] // Constrain Next to be non-connected injective [A, Next] // Constrain Next to be injective functional [A, Next] // Constrain Next to be functional #Next = minus[#A, 1] // Constraint Next to contain all atoms in A }