Alloy 3 Quick Start

Getting things running

Download the Alloy binary for your platform from the Alloy Website Download Page. For starters, download the latest Release Candidate (not the Nightly Build), and unzip the download.

Open the unzipped folder and run the Alloy executable. It probably looks like this:

Open the sample file examples/toys/ceilingsAndFloors.als (using the icon bar or File menu). The left half of the screen shows the text of the model, the top-right area displays feedback and visualizations, and the bottom-right corner lets you quickly switch between models that are currently open.

This example model has a few 'sig' declarations (which define sets), 'fact' paragraphs (which constrain the model), and 'pred' declarations (which declare predicates). Towards the bottom of the model are some 'assert' statements (which make claims about the model's behavior) and some 'check' statements (telling Alloy to analyze those assertions).

Now that we've got the model up on the screen, let's analyze it.

Select a command from the pull-down bar at the top of the screen. For starters, choose "chk BelowToo [2] (exp 1)", which checks an assertion about the model which is incorrect.

That assertion is false, so Alloy will produce a counterexample; the visualizer will be automatically opened, showing a diagram of a situation that violates the assertion.

Choose the Layout option on the icon bar to customize the solution. When you do so, the left hand side of the screen (the model text) is replaced by a set of customization options. The right hand side still displays the diagram of the solution Alloy found. Select the rightmost tab on the top of the left window and play around with the customization options. You can hide, rename, and recolor nodes and arcs in the diagram. Choose "Update" on the right end of the icon bar () to apply any changes you make.

Now close the customizer () and select "chk BelowToo' [2] (exp 0)" from the pull-down command selection bar. This one checks an assertion about the model that is correct, so you won't get a counterexample.

Execute that command (icon bar or Tools menu). Note that you do not need to re-build the model when you select a new command; you only need to re-build if you change the text of the model.

What does "valid within the specified scope" mean? When you check an assertion with the Alloy Analyzer, you have to provide bounds (or a 'scope') on each signature. Alloy guarantees that if there is a counterexample within the given bounds, then a counterexample will be found, and that if a counterexample is found, then it is a real one. However, it will miss any counterexamples that are larger than the given bounds.

You can learn more about modeling with the Alloy language from the Tutorial, the Reference Manual, and the FAQ. You can learn more about the research behind Alloy from our publications page. A good place to start is with the 'Micromodularity' paper and the 'Intentional Naming' case study. If you are an Alloy 2 user, you should read about what's new in Alloy 3.

Please send suggestions and bug reports to . For other questions, try out the alloy-discuss yahoo group.

Tiago Massoni Rohit Gheyi, and Paulo Borba have written a short list of hints and tips for using Alloy: