Constraints

Elements of Forge constraints are one of three types: formulas, which evaluate to booleans; expressions, which evaluate to relations, and integer expressions, which evaluate to (bounded) integers.

Formula operators

For the following "fmla" means a formula. The alternate symbols given are the symbols you can use instead of the keywords.

• not <fmla>: true when fmla is false. alt: !
• <fmla-a> and <fmla-b>: true when both fmla-a and fmla-b are true. alt: &&
• <fmla-a> or <fmla-b>: true when either fmla-a is true or fmla-b is true. alt: ||
• <fmla-a> implies <fmla-b>: true when either fmla-a is false or both fmla-a and fmla-b are true. alt: =>
• <fmla-a> iff <fmla-b>: true when fmla-a is true exactly when fmla-b is true. alt: <=>

Cardinality and membership formulas

You can think of a set as a 1-column relation. In the following docs, "relation" means set or relation.

The following produce booleans based on expression arguments

• no <expr>: true when expr is empty
• lone <expr>: true when expr contains zero or one elements
• one <expr>: true when expr contains exactly one element
• some <expr>: true when expr contains at least one element
• <expr-a> in <expr-b>: true when expr-a is a subset of or equal to expr-b
• <expr-a> = <expr-b>: true when expr-a and expr-b contain exactly the same elements

Quantifiers

In the following, "x" is a variable, "expr" is an expression, and "fmla" is a formula (that can use x). You can quantify over a unary expression in the following way.

• no <x>: <expr> | { <fmla> }: true when fmla is false for all elements in expr
• lone <x>: <expr> | { <fmla> }: true when fmla is true for zero or one elements in expr
• one <x>: <expr> | { <fmla> }: true when fmla is true for exactly one element in expr
• some <x>: <expr> | { <fmla> }: true when fmla is true for at least one element in expr
• all <x>: <expr> | { <fmla> }: true when fmla is true for all elements in expr

Note that if you want to quantify over several variables you can also do the following (only some are shown, but the same applies to all the others):

• some <x>: <expr-a>, <y>: <expr-b> | { <fmla> }
• some <x>, <y>: <expr> | { <fmla> }

Warning! Beware combining the no, one, and lone quantifiers with multiple variables at once; the meaning of, e.g., one x, y: A | ... is "there exists a unique pair <x, y> such that ...", which is different from the meaning of one x: A | one y: A | ....

Sometimes, it might be useful to try to quantify over all pairs of elements in A, where the two in the pair are distinct atoms. You can do that using set difference in the following way: some x: Atom, y: Atom - x | { <fmla> }

Relational expressions

There are also the following operators that evaluate to another expr:

• <expr-a> + <expr-b>: returns the union of the two exprs i.e. all elements in either of the two exprs.

• <expr-a> - <expr-b>: returns the set difference of the two exprs i.e. everything in expr-a that is not also in expr-b

• <expr-a> & <expr-b>: returns the intersection of the two exprs i.e. all elements in both expr-a and expr-b

• <expr-a> . <expr-b>: returns the join of the two exprs

• <expr-a> -> <expr-b>: returns the cross product of the two exprs

• <expr-a>[<expr-b>]: is equivalent to <expr-b> . <expr-a>

• ~<expr>: returns the transpose of expr, assuming it is has arity 2

• *<expr>: returns the reflexive-transitive closure of expr, assuming it is has arity 2

• ^<expr>: returns the transitive closure of expr, assuming it is has arity 2

• <fmla> => <expr-a> else <expr-b> returns expr-a if fmla evaluates to true, and expr-b otherwise

Note for Alloy users: Forge does not currently support the <:, :>, or ++ operators; if your models require them, please contact the Forge team.