Analyzer

The Alloy Analyzer is the tool that actually checks your spec.

Configuring the Analyzer

The analyzer converts the model into a SAT expression to solve. Some of the options are configurable. By default you should not need to change any of these- most performance issues are better solved by improving the spec itself. The following all affect the runtime of the analyzer. All of these are under the “Options” toolbar of the IDE:

  • Allow Warnings: When “no”, the analyzer will halt if the model has any warnings. Warnings usually, but not always, correspond to errors in the spec.
  • Maximum Memory: How much RAM the analyzer is allowed to use when solving.
  • Solver: The SAT solver to use for finding the model. Different solvers may have different performance on different specs. The SAT model and Kodkod model can also be output to a temporary file here. There are additional special options for MiniSat with Unsat Core, below.
  • Skolem Depth: see below
  • Recursion Depth: see below
  • Record the Kodkod input/output: when true, the Kodkod output for the run can be seen by clicking the Predicate link in the output.
../_images/kodkod.png
  • Prevent Overflows: If an arithmetic operation would overflow the model, the predicate is treated as false.

Recursion Depth

Predicates and functions are normally not recursive- they may not call themselves. The following is an invalid predicate:

sig Node {
    edge: set Node
}

fact {no iden & ^edge}

pred binary_tree[n: Node] {
    #n.edge <= 2
    all child: n.edge |
    // recursive call
        binary_tree[child]
}

run {some n: Node | binary_tree[n]}

This is invalid because all Alloy models must be bound, and recursive calls can lead to an unbound model. Normally you should restructure your model to not need a recursive call. If you must have a recursive predicate or function, you can set the recursion depth to a maximum of 3.

The recursion depth is treated as a “fact”: the analyzer will not look for models with a greater recursion depth, even if it would lead to a valid example or counterexample.

Warning

Increasing the recursion depth will slow down your spec.

Unsat Core

By default Alloy is packaged with Minisat, which also has an Unsat Core. When “MiniSat with Unsat Core” is selected as the solver, the analyzer can isolate which constraints prevent the analyzer from finding a counter/example. See here for more information.

Note

By default, the Windows version of Alloy does not come with MiniSAT.

Warning

The “Core Granularity” option is not strictly increasing in terms of information: a slower setting might, in some circumstances, lead to the core providing less information. Given the following model:

sig Node {
    edge: some Node
}

fact {some Node}

run {no edge}

All granularity settings will highlight three formulas except for “expand quantifiers”, which will only highlight two. However, all three constraints are required to make the predicate inconsistent.