Alloy 6 introduces an easier way of expressing temporal logic. With temporal logic you can model possible state transitions. This allows you to precisely describe operations on data structures.

Using the new temporal syntax

I was able to find only a few of articles on this topic. Here are some links:

• 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.

Temporal relation syntax so far

I have recently started working through the Alloy teaching book Software Abstractions by Daniel Jackson. The latest edition of the book is from 2016. The new syntax wasn’t available then. I used this as an opportunity transcribe some examples in the book and learn the new syntax.

Before, temporal relations between two entities were often 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 moment in Time. To make it interesting, I define further constraints and then show how to translate them to use the new temporal syntax.

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

You can express the first two with just a few lines. Alloy should 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. They can also hold constraints. Time predicates take in two entities, representing something that I want to model at two different points in time. Often these are t and t".

You may be referencing a lot of temporal relations. Predicate signatures and structures become tedious and verbose to type throughout an Alloy model.

The Software Abstractions book uses single quotes (') as a convention to express the next state of an entity. Alloy 6 instead requires you to use double quotes ("). Single quotes are now a part of the new temporal syntax, which I show 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]
}

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

If you want to generate relevant instances of this model, you have to project over Time in the visualizer. You can then see how entities relate to each other over time. This is a common and tedious task.

It turns out I started learning Alloy at just the right time. Alloy Analyzer 6 solves a lot of problems.

Translating the example

I now take a look at how to express the preceding Alloy model using the new temporal syntax. To use temporal signatures you don’t need an ordered Time signature anymore.

module newSyntax

sig TheThing {
}

sig TheOtherThing {
 	var theThing: TheThing,
}

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

You can write the first two facts by replacing any mention of all t: Time with always. See the following example:

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
}

To express temporal relations between sets, you can write the relation name with a single quote after it. You don’t have to explicitly pass around before and after states. You can express the not twice in a row with much less code:

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 always map an entity to a TheThing. The previous TheThing relation could have also been empty if it weren’t for the other constraint.

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

run {
	some TheOtherThing
}

Keep in mind that this is a simplified example showing the most prominent syntactic differences. Executing the solver and opening the visualizer also shows you more than before. You don’t have to projecting over time anymore, and the UI shows before and after side by side.

With the new visualizer you can step through and understand state transitions. Before, one had to visually compare two states by clicking between both of them. Like in of those Spot the mistake pictures you had to 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 section 6.2.4 in Software Abstractions are difficult to map to temporal syntax. The events emerge as soon as a condition holds true. You might want to pay attention when expressing this in Alloy 6. Look at this excerpt of the model 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 hold true. Before, pre and post were explicitly stated. You had to define the precise points at which the conditions hold true. Alloy 6 doesn’t give you a handle on specific points in time.

Instead, if to translate this, you need to make sure that the amount of entities can vary over time. That means that an entity isn’t required to always be present at every time step. It also means that signature conditions don’t have to always hold true.

As a consequence, you can also avoid events hanging around at points in time where they don’t happen. If events are always visible, Alloy’s visualization loses visual clarity. With a variable signature, an Entry event is only there when the Entry happens. You can write this 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
	}
}

I have only shown you how to translate the Entry signature in the preceding two listings. You can use a similar approach for the other Event signatures in the hotel keycard example.

Without using an explicit Time signature, you can’t reference the pre and post Time relations anymore. The new temporal syntax doesn’t provide a handle to a time step in which to evaluate a constraint. You have to “catch” the right moment in Time for the Entry signature constraints to hold true some other way.

Maybe you want your entities to exist for the whole duration of a model. You can instead specify that at some moment in Time, the conditions specified in the Entry signature hold true. In Alloy, you can express this constraint like so:

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. This could be now or in at least one future step.

See this list of temporal operators in Alloy for a detailed listing of all possible operators. You can also compose these operators. 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.

Since the new visualizer shows before and after side by side, window sizes can become unusably large and unwieldy for complex models. Yet, being able to not only see the before and after, but also which event happens at which step means an improvement in productivity.