Performing Analyses on Alloy Models

Loading the Model

When executing commands in an Alloy model, Alloy always uses the current content in the text editor as the model to compile. Therefore, if you made some changes to the model, you do not have to save them before running the model.

Performing an Analysis on Alloy Models

A run command is used to search for solutions that satisfy the specification and a predicate, while a check command is used to search for solutions that satisfy the specification but violate an assertion.

To run either type of analysis, select the command to be run from the run menu, or click the "run" toolbar button.

The run menu will display the list of check and run commands present in the model. You can execute the commands one at a time, or click "run all" to execute them all.

The run toolbar button will executes the most recently executed command. If no command has been executed, it will execute the first command in the model.

The analysis will either terminate with a solution or indicate that one cannot be found within the search space specified by the type scopes of the command. If a solution is found, it can be displayed by clicking on the blue clickable hyperlink in the message panel. Or, if you enable "visualize automatically" in the Options menu, then the solution will be displayed automatically.


Here are some of the common errors that may be encountered:

Things that may affect execution speed

Various things may affect the speed of analysis. These include: