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. 

	[Example_01.jpg]

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:

	[Example_02.jpg]

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:

	[Example_03.jpg]

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: 

	[Example_04.jpg]

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. 

------------------------------------------------------------------------------------------------------------------------------------------------------------------

In this part of the tutorial, we will be modelling a Map that associates unique keys with values (eg. java.util.Map in Java) and show how Alloy can be used to explore dynamic behaviour. 

The static aspects are easy to specify:

	module examples/tutorial/Map

	abstract sig Object {}

	sig Key, Value extends Object  {}

	sig Map {
		values: Key -> Value
	}

As in Java, "abstract" ensures that there cannot be any direct 'instances' of Object. Similarly, extends means that Objects can either be Keys or Values, but not both. 

values above is a relation that represents the mapping of Keys to Values. This could be written in a schema as:

	values \subseteq K x V

where K is the set of all Keys and V is the set of all Values.

We can visualize this model as before:

	pred show() {
	}

	run show for 2

The first instance produced by Alloy only consists of a Key and a Value but no Map. We could browse through the various solutions until we find one that actually includes a Map, however there is a better way. 

As mentioned before, Alloy produces instances that satisfy the predicate passed to "run". We can add a constraint that specifies that there is at least one Map: 

	pred show() {
		#Map > 0
	}

	run show for 2

We now get 2 Maps and one Value. To get exactly one Map, we can either change the constraint to

	#Map = 1

or we can modify the run command as follows:

	run show for 2 but exactly 1 Map

Next, let us check that the mapping of keys to values is unique. This can be done in Alloy via assertions: 

	assert mappingIsUnique {
		all m:Map, k:Key, v, v':Value |
			k -> v in m.values and k -> v' in m.values implies
				v = v'
	}

This says that if a Map maps a key to two values v and v' then they must be the same. Note how the relational product operator ("->") in k -> v is used to represent the tuple (k, v) and how m.values is treated as a set of tuples. To check an assertion, we can use the command check. As for run, we have to specify the scope:

	check mappingIsUnique for 2

If we execute this, Alloy tells us that the assertion may be valid. However, if we increase the scope to three, it produces the following counterexample: 

	[Example_2_01.jpg]

To make this even more obvious, we can ask Alloy to project over Map using the Projection button:

	[Example_2_02.jpg]

We see that a key refers to two values. To fix this, we use the lone keyword that we have already seen:

	sig Map {
		values: Key -> lone Value
	}

Now, the assertion even holds for quite large scopes (eg. up to 15). This produces a much larger coverage than any testcase ever could, which gives us a high level of confidence that the assertion is valid. 

To make the instances of later steps less verbose, we include the constraint that all keys (and values) belong to some Map: 

	fact {
	        all k:Key | some v:Value, m:Map | k -> v in m.values
	        all v:Value | some k:Key, m:Map | k -> v in m.values
	}

Unlike in the Queue example, it makes sense for keys and values to belong to different maps. Note that this fact is anoynomous; Alloy does not require you to name facts. 

Now that we have developed the static aspects of the Map, we will be adding dynamic behaviour to the model. We will define the operation of adding entries to the map: 

	pred put(m, m':Map, k:Key, v:Value) {
		m'.values = m.values + k -> v
	}

put is defined as a predicate so it acts a constraint, in this case it describes dynamic behaviour. The arguments of put are m and m', the Map before and after the operation respectively. k and v are the Key and Value to be put into the Map.

A parallel can be drawn here to operation schemas, notice how the decorator ' has the same meaning in both cases.

Informally in English, the above constraint reads as:

	"The set of values after is equal to the union<i> of the set of values before with the extra mapping from k to v"

We execute this predicate with the usual command:

	run put for 3 but exactly 2 Map

The following instance illustrates the functionality of the put operation: 

< TABLE THIS>

	[Example_2_04.jpg] [Before put] (Projected over Map)

	[Example_2_03.jpg] [After put] (Projected over Map)

Before the put operation there is no mapping between Key and Value in Map1.

After the operation there is a mapping between Key and Value in Map0.

</TABLE THIS>

As before, we use an assertion to check that put does not modify any of the existing mappings: 

	assert putLocal() {
		all m, m': Map, k, k': Key, v: Value |
			put[m,m',k,v] and k != k' implies
				lookup[m,k'] = lookup[m',k']
	}

	fun lookup(m: Map, k: Key): set Value {
		k.(m.values)
	}

lookup is defined as the function that returns the set of values that are associated with k in m
Functions in Alloy can be thought of as reusable expressions. For instance, lookup[m, k'] above is equivalent to k'.(m.values). 

Informally, putLocal asserts that adding a mapping k -> v does not change the existing mappings in the set.

As before, we check that the assertion holds:

	check putLocal

Alloy informs us that no counter-examples were found. We increase the scope and see that the assertion holds for eg. at least 15 objects of each signature and stop here. 

This concludes our tutorial. 

If you want to know more:
book
online tutorial/alloy website
3 perspectives

============================================================================================

A more accurate view of our Queue model is to treat the signatures Queue and Node as sets. Adopting this viewpoint, root can be seen as a binary relation which maps each Queue to at most one Node (similarly for next). This means that whilst they are both syntactically contained within the declarations of Queue and Node, semantically they are separate entities.

Going back to the example above, q was defined by:

	q:Queue

This can now be seen as saying "q is an element of the set Queue". 

To go one step further, behind the scenes in Alloy, all values are relations. This means that signatures are actually unary relations, while q above is encapsulated in the singleton unary relation {(q)}. 

q	.	root 			= n
Queue 	. 	(Queue x Node) 		= Node

Following on from this, q.root does not access a field of q, but q is an element of Queue?