Quantifiers

The Alloy quantifiers are

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:


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 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.