A Guide to Alloy
Dynamics II
We will proceed to adding dynamic behaviour to our model. In particular, 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 }
This is very similar to an operation schema in Object-Z: the instances of put consist of the state before(m), inputs(v), state after(m') and outputs of the operation. As in Object-Z, the convention is to use ' to decorate the state after the operation.

+ is the set union operator. The above constraint therefore reads as:
		"The set of values after is equal to the union of the set of values before with the extra mapping from k to v"
(Note how m.values is again treated as a set of tuples).

We execute this predicate with the usual command:
	run put for 3 but exactly 2 Map, exactly 1 Key, exactly 1 Value
Alloy produces the following instance which illustrates the functionality of the put operation:
module examples/tutorial/Map
abstract sig Object {}
sig Key, Value extends Object {}
sig Map {
	values: Key -> lone Value
assert mappingIsUnique {
	all m:Map, k:Key, v, v':Value |
		k -> v in m.values 
		and k -> v' in m.values
			implies v = v'
pred put(m, m':Map, k:Key, v:Value) { 
	m'.values = m.values + k -> v 
run put for 3 but exactly 2 Map, 
exactly 1 Key, exactly 1 Value


State before
State after
The assertion putLocal checks that put does not change the existing mappings in the set:
	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 an example of a function in Alloy. It uses the . operator to return all values that are associated with the Key k in the Map m, i.e. the set {v | (k, v) in m.values}. Note that the arguments to a function are enclosed in square brackets []. This is new in Alloy 4; in older versions (such as the one used in the official tutorial on the MIT website), they were enclosed in parentheses ().

We check that the assertion holds as before:
	check putLocal
Alloy informs us that no counter-examples were found. This is also the case if we increase the scope (to 15, say). Confident that our assertion may be valid, we stop here.

This already marks the end of our short tutorial. If you want to learn more about Alloy, we suggest looking at the following excellent resources: