A Guide to Alloy
Statics
In this tutorial, we will be using Alloy to model a linked list implementation of a Queue: Each queue has a root node and each node has a reference to the next node in the queue.

Each Alloy model starts with the module declaration:

module examples/tutorial/Queue
This is similar to declaring a class Queue in the package examples.tutorial in Java. Similar to Java, the file should be named 'Queue.als' and be located in the subfolder examples/tutorial of the project folder.

The first step is to declare the signature for the queue and its nodes:

sig Queue { root: lone Node } sig Node { next: lone Node }
You can think of root and next as being fields of type Node. lone is a multiplicity keyword which indicates that each Queue has less than or equal to one root (similarly for next).

A signature in Alloy is similar to the signature of a schema in that it defines the vocabulary for the model.

We can already visualize what we have written so far. The common way of doing this is to write a predicate and then make Alloy produce instances that satisfy this predicate. Asking Alloy to find instances is similar to finding a model of a given schema.

Because we want any instance of the Queue so far, the predicate has no constraints:

pred show() { }
To get sample instances of the predicate we use the command run:

run show for 2
A very important fact about Alloy is that it is only designed to search for instances within a finite scope. In the above case this scope is set to at most 2 objects in each signature (i.e. at most two Queues and at most two Nodes). Note that this is always an upper bound; Alloy may return a smaller instance.

In order to produce and visualize an instance, we first execute the run command by clicking on the Execute button. After the execution has finished, Alloy will tell us that it has found an instance which we can visualize by clicking on the Show button.
module examples/tutorial/Queue sig Queue { root: Node } sig Node { next: lone Node } pred show() {} run show for 2

In the above image, we see that Node1 is its own successor. As this is not what we usually expect from a linked list, we add a fact to constrain our model:

fact nextNotReflexive { no n:Node | n = n.next }
Facts in Alloy are 'global' in that they always apply, they correspond to the axioms of a schema. When Alloy is searching for instances it will discard any that violate the facts of the model. The constraint above can be read just like in first order logic: there is no Node n at is equal to its successor.

Executing "run show" now produces the following instance:
module examples/tutorial/Queue sig Queue { root: Node } sig Node { next: lone Node } fact nextNotReflexive { no n:Node | n = n.next } pred show() {} run show for 2 }

We no longer have a Node that is its own successor, but now notice another problem of our model: There are Nodes that do not belong to any Queue. We add another 'fact':

fact allNodesBelongToSomeQueue { all n:Node | some q:Queue | n in q.root.*next }
all and some behave exactly like the forall and exists quantifiers in predicate logic. The .* operator represents the reflexive transitive closure: It returns the set consisting of all elements

q.root, q.root.next, q.root.next.next, ...

If we press Execute, Alloy tells us that it found an instance. However, when we ask it to visualize the instance, it tells us that every atom is hidden. In order to get the next solution, we click "Next" at the top. Browsing through the instances, we find that one of them contains a cycle:
module examples/tutorial/Queue sig Queue { root: Node } sig Node { next: lone Node } fact nextNotReflexive { no n:Node | n = n.next } fact allNodesBelongToSomeQueue { all n:Node | some q:Queue | n in q.root.*next } pred show() {} run show for 2 }
In order to fix our model we add another fact:

fact nextNotCyclic { no n:Node | n in n.^next }
In contrast to the .* operator, .^ represents the non-reflexive transitive closure which returns the set consisting of all elements:

n.next, n.next.next, n.next.next.next, ...
(Note that this set does not include n itself).

Executing, visualizing and browsing through a few instances, we spot another error:
module examples/tutorial/Queue sig Queue { root: Node } sig Node { next: lone Node } fact nextNotReflexive { no n:Node | n = n.next } fact allNodesBelongToSomeQueue { all n:Node | some q:Queue | n in q.root.*next } fact nextNotCyclic { no n:Node | n in n.^next } pred show() {} run show for 2
The problem here is that Node0 belongs to two different queues. This is because allNodesBelongToSomeQueue constrains a Node to belong to "some" Queue, while it should actually belong to exactly one. To fix this we modify the fact:

fact allNodesBelongToOneQueue { all n:Node | one q:Queue | n in q.root.*next }
Browsing through the instances for this version of the model, Alloy soon tells us that 'there are no more satisfying instances'. All the solutions found within the scope provided seem to be correct. To gain more confidence, we increase the scope further:

run show for 3
Still, we cannot find any instances that clash with our definition of a linked list and conclude that this seems to be a good model for a linked list implementation of a queue. However, note that this does not prove that our model is correct! We can only guarantee that it corresponds with our definition for at most three Queues and three Nodes. As Alloy only ever searches a finite scope, it never allows you to prove that your model is correct. However, you can gain a fair amount of confidence that the main errors have been eliminated [Link to Small Scope Hypothesis on MIT website].

Now that we have seen how to model the static aspects of a system, we will move on to modelling dynamic behaviour and adding operations. For this, we will consider a different example.