Alloy modelling tips

Improved visualisation with auxiliary relations

You might have realised that the instance visualizer plays an essential role in the validation of Alloy specifications. A key feature in this process is the ability to customise the theme so that the relevant information is highlighted (and the irrelevant one hidden). In this section we present another feature of the visualizer that allows further tweaking instance visualization: the introduction of auxiliary relations.

Auxiliary relations in Alloy are introduced through the declaration of functions (much like auxiliary formulas are introduced through the declaration of predicates). These are declared with the keyword fun, followed by the function name, an optional list of function parameters, its return type, and an expression enclosed between braces. The return type can be any relational expression with arbitrary arity. Once declared, these functions can be freely used in relational expressions.

Let’s get back to the file system example from chapter Structural design with Alloy. A function could be declared to retrieve, for instance, all empty directories, which would be defined as follows.

fun empty_dirs : set Dir  {
  File - entries.Entry
}

At first sight, if we wanted to show the set of empty directories when visualizing an instance, we would have to declare an additional signature and enforce in a fact that its value is equal to the set empty_dirs. However, this signature would have to be solved by the Analyzer without actually introducing anything new in the specification. Besides the obvious benefit of declaring re-usable expressions, Alloy functions without parameters have an additional interesting feature: they are introduced by the visualizer in the depiction of instances, and are shown along the declared signatures and fields. Moreover, since they are introduced by the visualizer after the solving process, they can be freely abused without undermining the performance of the analysis. For instance, running the last version of the example command from chapter Structural design with Alloy, will now yield the depiction below.

../_images/viz1.png

Notice how the empty directory at the bottom has an additional label $empty_dirs. All visualization elements introduced by the visualizer are prefixed with a $. Since empty_dirs returns a set, it is interpreted as a sub-signature of Dir which by default are shown as labels in the theme. As expected, their depiction can be customised as any other signature. For instance, to highlight empty directories in the depiction, open the theme customisation menu, set $empty_dirs to be coloured in yellow and the displayed name to empty. The resulting depiction is below, where empty directories are clearly distinguished from non-empty ones.

../_images/viz2.png

Note

What’s with these other $-prefixed variables?

You may have noticed that sometimes $-prefixed sets (or relations) appear in the visualizer even without declaring auxiliary functions. This is because some existential quantifications in run commands (or universal ones in check commands), are solved through a process known as Skolemization. This process involves creating a relation corresponding to a witness of the quantification to which the solver will attempt to assign a value. Besides improving the performance of the analysis if used sensibly (the depth level can be configured in Options ‣ Skolem level, with 2 as default), this actually allows the execution of commands with certain higher-order quantifications.

Since these variables are solved by finding a value to a relation, they can also be depicted when visualizing the instance. This is useful since it helps us identify witnesses of quantifications. Their name is prefixed with $ and the context in which the quantification occurs. Consider, for instance, the following command.

check no_empty_dirs {
  all d : Dir | d in empty_dirs }

The universal quantification on a check will be solved through Skolemization. This property is obviously false, and returned counter-examples have assigned a value to the Skolem relation of d that has broken the property. Since the context of the quantification is the no_empty_dirs command, the Skolem relation is named $no_empty_dirs_d.

../_images/viz6.png

Like any other sub-signature, the visualization of Skolem relations can be configured in the theme, and can be hidden if we feel they are cluttering the depiction.

Auxiliary functions without parameters are actually introduced by the visualizer regardless of its arity, resulting in additional edges for relations of arity higher than 1. For instance, if we wanted to depict directly the relation between directories and their content, hiding the entries in the middle, we could define the binary relation below.

fun contents : Dir -> Object {
  entries.object
}

Running the command again results in the depiction below, with $contents edges between directories and objects.

../_images/viz3.png

Once we start introducing derived relations, it is often useful to hide others elements in order to unclutter the visualizer. In this case, we simply set Show to Off for the Entry signature, resulting in the depiction below where the content of directories is evident.

../_images/viz4.png

A consequence of short-circuiting entries in the visualizer is that we can no longer see the name of the objects. Relations with arity higher than 2 are depicted in the visualizer as edges with labels. Thus, a ternary relation with type Dir->Name->Object could be used to keep the content edges between directories and objects but also show the name of the object. Defining such relations is often not trivial, and usually requires defining relations by comprehension. In this case such relation could be defined as follows.

fun named_contents : Dir -> Name -> Object {
  { d : Dir, n : Name, o : Object |
    some e : Entry | e in d.entries and e.name = n and e.object = o }
}

Here, we are collecting all triples d->n->o such that there is an entry in d that has name n and object o. The resulting depiction is shown below, where the labels of relation $named_contents have the names of the objects appended.

../_images/viz5.png

Although we focused on an example without mutable signatures or fields, this strategy also works in that context, as we shall see in section An idiom to depict events. That’s because auxiliary relations are evaluated in the state they are called from, and when depicting traces, the visualizer will evaluate them at each individual state.

As a last note, recall that these auxiliary functions (and predicates) can always be called from the evaluator, so they may be useful for debugging instances even if we are not interested in showing them in the visualizer.

An idiom to depict events

In the chapter An overview of Alloy, we remarked that the Alloy visualizer does not show the event or events corresponding to a given transition. This is because we modelled them as predicates and there’s no way for Alloy to know that these particular predicates should be interpreted as events. In this section, building on the feature we presented in section Improved visualisation with auxiliary relations, we will devise an idiom (a modelling pattern) that precisely allows to depict events in the visualiser. As an opportune side effect, it also facilitates the writing of certain classes of formulas.

To illustrate this idiom, let’s consider the leader election example from chapter Protocol design with Alloy again. The full corresponding specification is shown below for completeness but the idiom doesn’t depend on the bodies of facts and predicates.

open util/ordering[Id]

sig Node {
  succ : one Node,
  id : one Id,
  var inbox : set Id,
  var outbox : set Id
}

var sig Elected in Node {}

sig Id {}

fact {
  // at least one node
  some Node
}

fact {
  // succ forms a ring
  all n : Node | Node in n.^succ
}

fact {
  // ids are unique
  all i : Id | lone id.i
}

fact {
  // initially inbox and outbox are empty
  no inbox and no outbox
  // initially there are no elected nodes
  no Elected
}

pred initiate[n : Node] {
  // node n initiates the protocol

  historically n.id not in n.outbox           // guard

  n.outbox' = n.outbox + n.id                 // effect on n.outbox
  all m : Node - n | m.outbox' = m.outbox     // effect on the outboxes of other nodes

  inbox'   = inbox                            // frame condition on inbox
  Elected' = Elected                          // frame condition on Elected
}

pred send[n : Node, i : Id] {
  // i is sent from node n to its successor

  i in n.outbox                              // guard

  n.outbox' = n.outbox - i                   // effect on n.outbox
  all m : Node - n | m.outbox' = m.outbox    // effect on the outboxes of other nodes

  n.succ.inbox' = n.succ.inbox + i           // effect on n.succ.inbox
  all m : Node - n.succ | m.inbox' = m.inbox // effect on the inboxes of other nodes

  Elected' = Elected                         // frame condition on Elected
}

pred process[n : Node, i : Id] {
  // i is read and processed by node n

  i in n.inbox                                // guard

  n.inbox' = n.inbox - i                      // effect on n.succ.inbox
  all m : Node - n | m.inbox' = m.inbox       // effect on the inboxes of other nodes

  gt[i,n.id] implies n.outbox' = n.outbox + i // effect on n.outbox
             else    n.outbox' = n.outbox
  all m : Node - n | m.outbox' = m.outbox     // effect on the outboxes of other nodes

  i = n.id implies Elected' = Elected + n     // effect on Elected
           else Elected' = Elected
}

pred stutter {
  outbox'  = outbox
  inbox'   = inbox
  Elected' = Elected
}

fact {
  // possible events
  always (
    stutter or
    some n : Node | initiate[n] or
    some n : Node, i : Id | send[n,i] or
    some n : Node, i : Id | process[n,i]
  )
}

run example {
  eventually some Elected
} for exactly 3 Node, exactly 3 Id

Let’s consider an instance returned when executing command example. After a short examination, and based upon our knowledge of the specification, we can determine that in this trace a stutter event happens in state 7.

../_images/instance1.png

However, in the general case, for more complex specifications, the fact that events aren’t displayed makes their interpretation tedious and error-prone. The crux of the idiom presented here is to use auxiliary relations to represent the events happening in a given state.

This may not seem immediately obvious as auxiliary relations define relations based on existing signatures, while we haven’t got any such signature for events, only predicates. No problem! Let’s introduce a signature (more precisely: an enumeration, as we won’t need to add fields) representing event names. Observe how we use the capitalised names of predicates (corresponding to events) as elements of the enumeration, in order to enhance readability.

enum Event { Stutter, Initiate, Send, Process } // event names

Also, in the theme customisation menu, change the shape and colour of events, for instance to a red parallelogram. Then set Hide unconnected nodes to On for Event nodes, as we don’t want to see all event names at all states, but only those corresponding to events occurring in a given state.

Now, let’s introduce a first auxiliary relation, which should be populated when the stutter event happens. Recall that auxiliary relations that refer to mutable elements are evaluated in the state they are being called from.

fun stutter_happens : set Event {
  { e: Stutter | stutter }
}

This definition may seem strange at first but this is indeed what we want: the stutter_happens auxiliary relation yields, in every state, a subset of Event that will be populated (by the name Stutter) if the stutter predicate is true, and empty otherwise.

Observe the effect of adding this auxiliary relation on visualisation. First, open the theme customisation menu and set both Hide unconnected nodes and Show as labels to Off for stutter_happens. This will override the hiding of Event nodes that belong to stutter_happens. Then head to the last states of the trace (where the stutter event happens). You will now be able to observe the event happening, as shown below.

../_images/instance2.png

Now, let’s consider the initiate event. This event takes a node as a parameter. In this case, the auxiliary relation shouldn’t just yield the Initiate name as we wouldn’t be able to tell for which node or nodes it is satisfied. We rather return the set of all pairs whose first coordinate is the Initiate name and whose second coordinate is a node on which the initiate event happens:

fun initiate_happens : Event -> Node {
  { e: Initiate, n: Node | initiate[n] }
}

Now the first state of the trace is as follows. Since Event nodes related by initiate_happens are no longer unconnected, they will show up in the visualization.

../_images/instance3.png

We can finally proceed with the last two events:

fun send_happens : Event -> Node -> Id {
  { e: Send, n: Node, i: Id | send[n, i] }
}

fun process_happens : Event -> Node -> Id {
  { e: Process, n: Node, i: Id | process[n, i] }
}

As you start visualising a trace, you may realise that the depiction of events without further theming is deficient when an event takes two parameters or more. A possible enhancement is to show event parameters as labels rather than edges. To do so, we can introduce a further auxiliary relation that just returns the set of names of all occurring events.

fun events : set Event {
  stutter_happens + initiate_happens.Node + (send_happens + process_happens).Id.Node
}

Note that, for instance, expression initiate_happens.Node projects away any parameter of initiate events and keeps only the event name. Then the following theme can be configured:

  • Uncheck Hide unconnected nodes for the events set and set Show as labels to Off.

  • In the relations part, set all auxiliary relations for events to Show as attribute and change the displayed name for the auxiliary relations to args.

This way, we get the following depiction. Notice how the arguments of events can be seen clearly (e.g. Node0 and Id2 for the event send in state 1).

../_images/instance4.png

This is it for the idiom enabling a more informative depiction of traces!

At the beginning of this section, however, we also said that the idiom is useful to specify certain classes of formulas in a nice way. Let’s explore this aspect. First, the idiom allows to greatly simplify the traces fact!

fact traces {
  // possible events
  always some events
}

You may also check whether it is possible to witness the occurrence of two events in the same state, which happens to be the case.

check at_most_one_event {
  always lone events
} for exactly 3 Node, exactly 3 Id

However, if, for example, we remove the guard from event initiate this property yields the following counter-example, where an occurrence of initiate is undistinguishable from stuttering. This was an issue already explored back in chapter Protocol design with Alloy.

../_images/instance6.png

More importantly, notice that predicates and functions belong to different namespaces in Alloy. Additionally, they can always be disambiguated based on the syntactic context. For this reason, it is possible to give to the functions defined above the same name as the respective predicates!

fun stutter : set Event {
  { e: Stutter | stutter }
}

fun initiate : Event -> Node {
  { e: Initiate, n: Node | initiate[n] }
}

fun send : Event -> Node -> Id {
  { e: Send, n: Node, i: Id | send[n, i] }
}

fun process : Event -> Node -> Id {
  { e: Process, n: Node, i: Id | process[n, i] }
}

fun events : set Event {
  stutter + initiate.Node + (send + process).Id.Node
}

Now suppose you want to see the example of a trace in which two process events happen in a row (for some arguments). Until now, you would have had to write this in a rather contrived way, for instance as follows.

run two_process_in_a_row {
  eventually (
    (some n: Node, i: Id | process[n, i]) and
    after (some n: Node, i: Id | process[n, i])
  )
} for exactly 3 Node, exactly 3 Id

Yet, the auxiliary relations defined above are also useful to say that an event happens (for some parameters). Indeed, it is enough to say that the corresponding auxiliary relation is non-empty!

run two_process_in_a_row {
  eventually (some process and after some process)
} for exactly 3 Node, exactly 3 Id

Thus, giving the same name to a predicate (representing an event) and to the respective auxiliary relations makes it easy to say that an event e happens: you just have to write some e!

As a final remark, notice that this idiom doesn’t entail any performance penalty:

  • If auxiliary relations are only used for the depiction of events, they are only computed when visualising instances.

  • If they are also used in formulas, to say for instance that an event happens, they actually use less variables than the version where a predicate is passed arguments quantified existentially.

Thus, the only price to pay is a small but systematic inflation, albeit admittedly tedious, of our models. In the future, an extension to Alloy may be proposed to automate this task.

Defining test scenarios with formulas

As an Alloy specification increases in size and complexity, its validation through the exploration of arbitrary instances in the visualizer becomes less useful, since getting varied instances is increasingly unlikely. This is even more patent when exploring trace instances, despite the exploration operations provided by the visualizer. At that point, one must combine this exploration with the specification of finer run commands. Note that often we don’t want the command completely fix the instances since we want to be able to explore the design. Instead, we want to partially specify interesting scenarios that the Analyzer will complete by solving the specification’s constraints. This is not necessarily trivial for complex specifications.

This first issue we often face is the inability to refer to concrete atoms in Alloy specifications. Let’s start with the specification of scenarios for instances without mutable signatures and fields, on which we will later build to specify trace scenarios. Let’s consider the structural part of the leader election example from chapter Protocol design with Alloy and say that we want to explore scenarios with 3 nodes with sequential identifiers.

We can achieve through an idiom based on some/disj patterns. For instance, the scenario above could be defined as follows.

run scenario {
  some disj n1, n2, n3 : Node, i1, i2, i3 : Id {
    Node = n1 + n2 + n3
    Id   = i1 + i2 + i3
    next = i1 -> i2 + i2 -> i3
    succ = n1 -> n2 + n2 -> n3 + n3 -> n1
    id   = n1 -> i1 + n2 -> i2 + n3 -> i3
  }
} for 3

The disj keyword is needed in order to avoid the assignment of the same atom to different variables. For instance, without disj here a single node atom assigned to n1, n2 and n3, pointing to itself, would be a valid instance. Moreover, the equality test with Node guarantees that no other atom will exist in Node besides the 3 quantified. The subsequent lines enforce the value of the fields to define the desired ring topology. Always make sure that there are enough atoms in the scope to represent the scenario, otherwise the command will be trivially unsatisfiable.

Due to the mechanics explained in section Improved visualisation with auxiliary relations, the quantified variables appear identified in the visualizer, prefixed by a $ and the name of the command, as shown below. This can be customized in the theme.

../_images/sce1.png

Note that, as with anything Alloy, these specifications can be mixed with other constraints. For instance, the same scenario, where identifiers are sequential, could be equally specified as follows.

run scenario {
  some disj n1, n2, n3 : Node, i1, i2, i3 : Id {
    Node = n1 + n2 + n3
    Id   = i1 + i2 + i3

    all n : Node | n.id.(next + last -> first) = n.succ.id
  }
} for 3

As run commands become more restricted, they become less interesting for validation, since the room for unpredictable results is reduced. However, these commands also serve a second purpose: they can be used as a kind of regression testing, commands that we know must hold (or fail) for our specification, and that can be re-executed whenever the specification evolves. Alloy has an expects keyword for commands that can help managing these commands.

Note

What about multiplicity one signatures?

At first sight, one could declare 3 pairs of signatures with multiplicity one extending Node and Id to specify all the atoms we need, and then call those signatures in run commands. However, this approach has a major disadvantage: introducing such signatures in the specification affects all analysis commands in the specification. For instance, all check commands would only consider instances where there were at least 3 nodes. Perhaps even worse, it would break the symmetry between those atoms, as they would no longer be uninterpreted, and isomorphic instances would be returned. Unless we are dealing with concepts of the domain model, we should not clutter our specifications with additional signatures. The some/disj pattern provides a way to specify scenarios that is local to each command.

Moving to the mutable context, we must now extend such formulas to restrict multiple states. The main issue here is that with the temporal operators we have seen so far, this would result in either nested and/after formulas, or expressions with several appended primes ', neither being a scalable approach. Luckily, Alloy has a sequential temporal operator ; that greatly eases specifying such formulas. For instance, the code below restricts the value of inboxes and outboxes in the first 3 states.

run scenario {
  some disj n1, n2, n3 : Node, i1, i2, i3 : Id {
    Node = n1 + n2 + n3
    Id   = i1 + i2 + i3
    next = i1 -> i2 + i2 -> i3
    succ = n1 -> n2 + n2 -> n3 + n3 -> n1
    id   = n1 -> i1 + n2 -> i2 + n3 -> i3

    no outbox; outbox = n1 -> i1; outbox = n1 -> i1 + n2 -> i2
    no inbox;  no inbox;          no inbox
  }
} for 3 but 10 steps

Again, we can leave these formulas as underspecified as we wish. For instance, we are not restricting the value of Elected, which will be solved during analysis. Moreover, by restricting only 3 states, the succeeding ones will be freely solved by the Analyzer. Again, make sure that there are steps in the scope to represent the scenario. Alternatively, one could enforce a final state forbidding any further changes with a temporal always as follows.

run scenario {
  some disj n1, n2, n3 : Node, i1, i2, i3 : Id {
    Node = n1 + n2 + n3
    Id   = i1 + i2 + i3
    next = i1 -> i2 + i2 -> i3
    succ = n1 -> n2 + n2 -> n3 + n3 -> n1
    id   = n1 -> i1 + n2 -> i2 + n3 -> i3

    no outbox; outbox = n1 -> i1; always outbox = n1 -> i1 + n2 -> i2
    no inbox;  no inbox;          always no inbox
  }
} for 3 but 10 steps

In fact, all formulas inside the sequence can also be temporal, but they become difficult to manage outside this pattern.

The example above followed a relation-wise definition of the trace. Sometimes, however, it’s easier to think about scenarios state-wise, particularly for relations closely related. Following this idiom, this could also be achieved as follows.

run scenario {
  some disj n1, n2, n3 : Node, i1, i2, i3 : Id {
    Node = n1 + n2 + n3
    Id   = i1 + i2 + i3
    next = i1 -> i2 + i2 -> i3
    succ = n1 -> n2 + n2 -> n3 + n3 -> n1
    id   = n1 -> i1 + n2 -> i2 + n3 -> i3

    no outbox + inbox;
    outbox = n1 -> i1 and no inbox;
    always (outbox = n1 -> i1 + n2 -> i2 and no inbox)
  }
} for 3 but 10 steps

As a last tip, sometimes we end up defining multiple scenario commands that share a certain part of the specification. At this point it is often useful to refactor-out parts of the specification into auxiliary predicates. For instance, if we wanted to define multiple scenarios for the same ring topology:

pred seq_ring [n1, n2, n3 : Node, i1, i2, i3 : Id] {
  Node = n1 + n2 + n3
  Id   = i1 + i2 + i3
  next = i1 -> i2 + i2 -> i3
  succ = n1 -> n2 + n2 -> n3 + n3 -> n1
  id   = n1 -> i1 + n2 -> i2 + n3 -> i3
}

run scenario {
  some disj n1, n2, n3 : Node, i1, i2, i3 : Id {
    seq_ring[n1,n2,n3,i1,i2,i3]

    no outbox + inbox;
    outbox = n1 -> i1 and inbox = n1 -> i1;
    always (outbox = n1 -> i1 + n2 -> i2 and inbox = n1 -> i1 + n2 -> i2)
  }
} for 3 but 10 steps

Using the evaluator to debug specifications