Syntax for the run command

The run command lets you generate sample solutions to your model.

  run pred-name for # but # sig-name, # sig-name
  run pred-name for # sig-name, # sig-name, # sig-name, # sig-name

If no default is given (the first # in the first of the two templates shown above, then it is assumed to be 3).

One benefit of using the run is that it will increase your confidence that your model is not underconstrained. When you use run to generate an example of an underconstrained model, you will usually see an absurd situation in one of the first few attempts. Of course, there are no guarantees that you won't happen to see only good examples -- that's what check statements are for!

Doing runs to periodically check up on your system helps identify overconstraint; if Alloy is unable to find any solutions when it should have, then your model is surely overconstrained.