Created at: Tuesday, 22 April 2025 8:16:43 pm Last Modify: Tuesday, 22 April 2025 8:16:43 pm

Used Alloy Syntax

+, -, &

S1 + S2 is the set of all elements in either S1 or S2 (set union).

S1 - S2 is the set of all elements in S1 but not S2 (set difference).

S1 & S2 is the set of all elements in both S1 and S2 (set intersection).

++

rel1 ++ rel2 is the union of the two relations, with one exception: if any relations in rel1 that share a “key” with a relation in rel2 are dropped. Think of it like merging two dictionaries.

-> used as an operator

Given two sets, Set1 -> Set2 is the Cartesian product of the two: the set of all relations that map any element of Set1 to any element of Set2.

Set1 = {A, B}
Set2 = {X, Y, Z}

Set1 -> Set2 = {
  A -> X, A -> Y, A -> Z,
  B -> X, B -> Y, B -> Z
}

As with other operators, a standalone atom is the set containing that atom. So we can write A -> (X + Y) to get (A -> X + A -> Y).

|

Set Comprehensions Set comprehensions are written as

{x: Set1 | expr[x]}

The expression evaluates to the set of all elements of Set1 where expr[x] is true. expr can be any expression and may be inline. Set comprehensions can be used anywhere a set or set expression is valid.

Set comprehensions can use multiple inputs.

{x: Set1, y: Set2, ... | expr[x,y]}

In this case this comprehension will return relations in Set1 -> Set2.