Quantifiers

The Alloy quantifiers are

• all x:X | formula - every x of type X satisfies formula. If there are no X, then this statement is trivially true.
• some x:X | formula - one or more x of type X satisfy formula. If there are no X, then this statement is trivially false.
• no x:X | formula - exactly zero x of type X satisfy formula
• one x:X | formula - exactly one x of type X satisfies formula
• lone x:X | formula - either zero or one x of type X satisfies formula

Note that a 'formula' is something that evaluates to a boolean value, as opposed to an 'expression' which evaluates to a (relational) value. With "some", "no", one", and "lone", you can also apply them to a set or a relation like this:

• some X - there is at least one X
• no X - there are no X's
• one X - there is exactly one X
• lone X - there are either zero or one X's

The basic format for a quantifier is

  quantifier variable:type | formula

where the formula may includes references to the quantifier variable. An alternative notation is:

  quantifier variable:type { formula }

Examples:

  //Does any directory contain itself?
  some d: Dir | d.parent = d

  //every file is some directory
  all f:File | some d:Dir | f.parent = d

  //no two directories have exactly the same contents
  no dir1, dir2: Dir | dir1!=dir2 && dir1.contents=dir2.contents

The above features can, of course, be combined to produce arbitrarily complex formulas.

However, be warned that nested quantifiers may cause your model to become intractable. In generaly, try not to stack more than two or three of them together.