Syntax for fact statements

  fact [name] {
       constraint1
       constraint2
       constraint3
  }

Facts do not need to have names, and are never refered to by name. However, good names improve clarity tremendously.

A warning: When Alloy searches for examples, it discards any which violate any fact. Thus, if the fact is trivially false, then you will simply get no examples of anything, even if the assertion you are checking has counterexamples. It will appear the same as if the model were bug free and the assertion you are checking is correct. You can use the run command to check for such simpleminded overconstraints. More advanced overconstraint detection tools will be available in future versions of Alloy.

Many facts can also be written as appended facts, which can make your models clearer and more concise.