Using the new temporal syntax

Alloy 6 introduces an easier way of expressing temporal logic. With temporal logic it is possible to model state transitions and precisely describe operations on data structures. I was able to find only a handful of links on this topic, some of which are:

• A post by Hillel Wayne showing the new syntax using a graph theory example
• Alloy Documentation by Hillel Wayne on the syntax
• Official announcement on Alloy 6
• Formal Software Design with Alloy 6

I am using Alloy Analyzer 6.1.0 to run the below Alloy listings.

How temporal relations were expressed so far

I have recently started working through the Alloy teaching book Software Abstractions by Daniel Jackson. The latest edition of the book has been released in 2016, so the new syntax has not been available at that point in time. I used this as an opportunity to transcribe some of the examples in the book to learn the new syntax.

Before, temporal relations between two entities were commonly written like this:

module oldSyntax
open util/ordering[Time]

sig Time {}

sig TheThing {
}

sig TheOtherThing {
 	theThing: TheThing one -> Time,
}

This describes a model in which a given TheOtherThing entity can relate to exactly one TheThing entity at any point in time. To make it interesting, we define some additional constraints and then show how to translate them to use the new temporal syntax.

• At any point in time, TheOtherThing is related to a TheThing.
• At any point in time, TheThing is related to exactly one TheOtherThing.
• TheOtherThing may not related to the same set of TheThing twice in a row.

The first two are easy to express. We map over all Time entities and all TheThing and TheOtherThing respectively and assert a quantity like so:

fact "TheOtherThing has TheThing" {
	all t: Time, th: TheOtherThing |
		th.theThing.t
}

fact "TheThing belongs to exactly one TheOtherThing" {
	all t: Time, th: TheThing |
		one (theThing.t).th
}

The third constraint compares TheOtherThing at two sequential points in time. Predicates are commonly used to encapsulate complex relationships, but also constraints. Such a predicate usually takes in two entities representing something that is being modeled at two different points in time, like t and t". When a lot of temporal relations are referenced, predicate signatures and structures becomes tedious and verbose to type throughout an Alloy model.

The original Software Abstractions book uses single quotes (') as a convention to express the next state of an entity, whereas writing this in Alloy 6 requires us to use double quotes ("). Single quotes have become elements of the the new temporal syntax, which I demonstrate further below.

pred notTheSame(t, t": Time, th: TheOtherThing) {
	th.theThing.t != th.theThing.t"
}

fact "not twice in a row" {
	all th: TheOtherThing, t: Time - last |
		let t" = t.next |
			notTheSame[t, t", th]
}

We can execute and visualize this with the default and implicit run command and see the following:

If we want to evaluate instances of this model, we have to choose to project over Time in the visualizer to clearly see how entities relate to each other over time. Having to do this is common, and again tedious.

It turns out I started learning Alloy at a good point in time then, since all of the above mentioned problems have been solved in Alloy Analyzer 6.

Translating the example

We now take a look at how to express the above Alloy model using the new temporal syntax. First, we write the signatures. We note that an ordered Time signature is not needed anymore.

module newSyntax

sig TheThing {
}

sig TheOtherThing {
 	var theThing: TheThing,
}

The var keyword indicates that a relation can change between time steps.

The first two facts can be expressed simply by replacing any mention of all t: Time with always, as can be seen below:

fact "TheOtherThing has TheThing" {
	always all th: TheOtherThing |
		some th.theThing
}

fact "TheThing belongs to exactly one TheOtherThing" {
	always all th: TheThing |
		one theThing.th
}

In order to express temporal relations between sets, we write the relation name with a single quote appended. We do not have to explicitly pass around before and after states. The fact that we have previously defined can therefore be made much shorter

pred notTheSame(th: TheOtherThing) {
	th.theThing != th.theThing'
}

fact "not twice in a row" {
	always all th: TheOtherThing |
		notTheSame[th]
}

Importantly, the first fact becomes irrelevant. The new signature for TheOtherThing will always map an entity to a TheThing, whereas before the theThing relation could have also been empty if it were not for the additional constraint.

To make sure that we see some examples with at least one TheOtherThing, we define a run predicate like so:

run {
	some TheOtherThing
}

Keep in mind that this is a really simple example that is meant to demonstrate the most obvious syntactic differences. Executing the solver and opening the visualizer also shows us more than before. It is not needed anymore to project over Time, and the before and after are shown side by side.

With the new visualizer it is easy to step through and understand state transitions. Previously one had to visually compare two states by clicking between both of them and like one of those Spot the mistake pictures pick out the thing that went wrong in a model instance.

Challenges when translating

Models that generate events as a side effect, such as the hotel key card example from the chapter 6.2.4 in Software Abstractions are difficult to map to temporal syntax. The events emerge as soon as a condition is satisfied at a point in time. Special care is needed when expressing this in Alloy 6. Take this excerpt of the model, taken from figure 6.10 in Software Abstractions:

abstract sig Event {
	pre, post: Time,
	guest: Guest
}

abstract sig RoomKeyEvent extends Event {
	room: Room,
	key: Key,
}

sig Entry extends RoomKeyEvent {} {
	key in guest.keys.pre
	let ck = room.currentKey | (
		key = ck.pre
		or key = nextKey [ck.pre, room.keys])
	currentKey.post = currentKey.pre ++ room -> key
}

An Entry event can only exist if the conditions given in the signature are satisfied. Before, pre and post were explicitly stated, so the precise points at which the conditions shall be true are defined. Alloy 6 does not give us a handle on specific points in time.

Instead, if we want to translate this we have to make sure that the amount of entities can vary over time. That means that an entity is not required to always be present at every time step and therefore the signature conditions do not have to be satisfied at all times.

As a consequence of this, we can also avoid events hanging around at points in time where they do not happen. If they were the to needlessly be shown, our visualization would lack visual clarity. With a variable signature, an Entry event is only there when the Entry happens. It can therefore be written like so:

var abstract sig Event {
	var guest: Guest
}

var abstract sig RoomKeyEvent extends Event {
	var room: Room,
	var key: Key,
}

var sig Entry extends RoomKeyEvent {} {
	always {
		key in guest.keys
		let ck = room.currentKey | (
			key = ck
			or key = nextKey[ck, room.keys])
		currentKey' = currentKey ++ room -> key
	}
}

We only show how we have treated the Entry signature in the above two listings, but a similar approach can be used for the other Event signatures in the hotel keycard example.

Since we do not use an explicit Time signature anymore, we cannot assign a pre and post Time reference. As a consequence, Event drops its pre and post relations. Since the temporal syntax does not provide a handle to a time step in which a constraint is evaluated, we have to wait for the right point in time for the Entry signature constraints to hold true somehow and use a variable signature.

In the case that we are interested in entities existing for the whole duration of a model, we instead specify that at some point in time, the conditions specified in the Entry signature hold true. We can write something like the following in Alloy.

sig Entry extends RoomKeyEvent {} {
	eventually {
		key in guest.keys
		let ck = room.currentKey | (
			key = ck
			or key = nextKey[ck, room.keys])
		currentKey' = currentKey ++ room -> key
	}
}

This means that for an entity to be a valid Entry event, the conditions specified have to hold true eventually, meaning now or in at least one future step.

See this list of temporal operators in Alloy for a detailed listing of all possible operators. These can be composed, so if you would like to specify that a predicate P should hold true only after the first step and then always, you can specify after always P, and so on.

Since two sequential points in time are shown side by side in the new visualizer, the UI can get quite large for complex models. On the other hand being able to not only see the before and after, and also clearly see which event happens at which step means an improvement in productivity.