Logical Operations

Alloy supports the standard boolean operators:

  !F      // negations: not F
  F && G  // conjunction: F and G
  F || G  // disjunction: F or G

It's useful to have a variety of implication operators:

  F => G         // implication: same as !F || G
  G <=> G        // bi-implication: same as (F => G) && (G => F)
  F => G else H  // conditional: if F then G else H; same as (F => G) && (!F=> H)

If you do not write sufficient parentheses, Alloy assumes that certain operations bind tighter than others. In order from tightest to loosest:

  not (!)
  and (&&)
  implication/conditional (=>)
  bi-implication (<=>)
  or (||)

Thus, the following pairs of expressions are equivalent

  !A && B        //  (!A) && B
  A && B || C    //  (A && B) || C
  A || B && C    //  A || (B && C)
  A => B => C    //  (A => B) => C

You are permitted to add excess parentheses at your judgement. Thus, A, (A), and ((A)) are all equivalent.

If you write several statements in the curly braces of the body of a fact, assert, or quantifier, those statements are implicityly conjoined (&&). That is,

fact Fibbles {
  (no X) && (all y:Y | y in Foo)

could be written as

fact Fibbles {
  no X
  all y:Y | y in Foo


all x: e | F && G && H

could be written as

all x: e {F G H}