Tutorial

Introduction

This brief tutorial to Electrum is aimed at users already fluent in Alloy.

We also suppose that Electrum Analyzer is already installed.

What is Electrum?

In a nutshell, Electrum is an extension of Alloy with:

1. A keyword ("var") to declare some fields and signature as variable (i.e. their valuation may vary along time);
2. Connectives from Linear Temporal Logic with Past (PLTL) to express properties of traces;
3. Primed expressions that represent the value of the said expressions in the next instant (so the prime sign is, contrary to Alloy, not a valid character for identifiers);
4. Bounded and unbounded model-checking procedures to analyze the resulting specifications.

Transitioning from Alloy

If you are used to modelling Alloy specifications using the "local state idiom", then the shift is quite easy:

1. Most of the relations that were indexed by Time will usually be just tagged var;
2. You need not join variable expressions with an expression denoting an instant;
3. You must replace quantifications over time by the corresponding, classic LTL operators (e.g. always, eventually...);
4. Specifications are interpreted over infinite sequences of states, hence there is no hypothetical last state of a trace to consider (but it also means that if your specification models a system that terminates, you must still ensure traces are infinite, otherwise your specification would be inconsistent: this can for instance be done by changing the specification so that your system loops endlessly in the last state, typically doing nothing).

Modelling example: leader election

We take as an example the "leader election" case study presented in Daniel Jackson's book and present in the Alloy sample models. Do not hesitate to compare the Alloy version and this one. (Notice this example is also available in the Electrum sample models.)

The aim of this protocol is to elect a leader in a ring-shaped network, in a decentralized way. The network is made of processes and every process has an identifier (it may for instance be an address). Furthermore, each process holds a set of identifiers (a message buffer, really) that it should send to its successor in the ring: this set only contains identifiers greater that its own one. When a process receives its own identifier, it means it was the greatest in the whole network, and so this process is actually the leader.

State modelling

In Electrum modelling terms, the above is summed up by introducing a Process signature, with three fields:

• its identifier id of a totally-ordered type Id (this is not strictly necessary, as we could have specified a total order on Process itself, but it makes the exposition a bit easier to follow);
• a "pointer" succ to its successor process;
• a set toSend of identifiers to send to the successor: obviously, due to the network dynamics, this field should be declared as variable:

open util/ordering[Id]

sig Id {}

sig Process {
  succ: Process,
  var toSend: set Id, // mind the 'var' keyword
  id : Id } 

fact distinctIds {
  id in Process lone -> Id }

Formally, the specification says that toSend denotes a binary relations from Process to Id, the valuation of which may change at every instant. But notice that Process and Id denote themselves static sets.

We now stipulate that processes form a ring-shaped network:

fact ring { all p: Process | Process in p.^succ }

Now, we want to prove that a unique process will be elected. To avoid overspecification, we stipulate that there is a set of elected processes, and then we will show later that it will ultimately be a singleton. This set may have a different value at every instant (e.g. it will be empty at the beginning), and this is nicely expressed in Electrum by declaring a variable signature as a subset of the set of processes:

var sig elected in Process {} // mind the 'var' keyword

Intuitively, you may think of this as the same as introducing a dummy singleton signature holding a corresponding field. So we could have written the following instead:

one sig Globals { var elected : set Process }

Variable signatures can contain fields (which is not needed here), but only variable ones as a static relation between variable sets wouldn't make much sense.

Now, how shall the elected signature take its values?

Well, we say first that, in the initial state, the set of elected processes is empty.

Then, at every instant, the set will contain in the next instant processes that will just have received their own identifier (i.e. they don't hold it the current instant):

fact defineElected {
  no elected  // empty in the inital state
  always elected' = { p: Process | (after p.id in p.toSend) and p.id !in p.toSend } }

This fact introduces three new Electrum constructs:

• always is the connective from Linear Temporal Logic (LTL): it means that the constraint that follows is true is any future instant, including the instant where this connective is evaluated.
• after is also an LTL connective. It says that the following constraint is true in the next instant. (Usually, this connective is called "next" in LTL, but next is already used in the util/ordering Alloy module, that we kept in Electrum, so we chose to call this operator after to avoid name clashes.)
• finally, the prime symbol (following elected) is a facility to talk about the value of elected at the next instant (so after applies to constraints while the prime symbol applies to expressions).

Past operators

We could also have used past operators here to make the specification a bit easier to read (with before to consider the preceding instant), but there is -at the time of writing- a bug with past operators, so better avoid using them for the time being.

Events

Essentially, there is one kind of event that may happen in the ring, namely communication between two successive processes: a process sends an identifier from its pool to its successor. If this identifier is greater than some identifiers already present in the receiver's pool, then those are deleted from the said pool as they are necessarily superseded by the greatest one (notice the absence of frame conditions concerning other processes, as these may also communicate in parallel).

pred communication [p: Process] {
  some identifier: p.toSend {
    p.toSend' = p.toSend - identifier
    p.succ.toSend' = p.succ.toSend + (identifier - prevs[p.succ.id]) } }

Traces

As in plain Alloy, we define the shape of traces of the protocol:

• in the initial state, every process only contains its own identifier in its pool of identifiers to send;
• then, at every instant, every process must be part of a communication (either as a sender or a receiver) or do nothing.

pred init { all p: Process | p.toSend = p.id }

fact traces {
  init
  always all p: Process | communication[p] or communication[p.~succ] or doNothing [p] }

pred doNothing [p: Process] { p.toSend' = p.toSend }

Checking safety

Safety properties assert that "nothing bad happens", which means here that there will always be at most one elected process and it will always be the same:

assert Safety {
  always all x : elected | always all y : elected | x = y }
check Safety for 3 but 20 steps

As explained in the introduction, Electrum specifications range over infinite traces, i.e. infinite sequences of states, where every trace is only made of a finite number of states (as the state space if finite). These infinite traces have a specific shape, related to the finiteness of the state space: they are periodic. Meaning a trace is always of the following form:

• a (possibly-empty) prefix (often corresponding to an initialisation of the modelled system)
• followed by a (non-empty) suffix in which the last state loops back to the first state of the suffix (this is the aforementioned periodicity).

Notice the scope of the command: it contains a bound on the number of steps. This scope states that bounded analysis (as in Alloy) should be performed on infinite traces made of at most 20 different states.

As in Alloy, the scope on these steps can be declared exact using the exactly keyword.

Checking liveness

Liveness properties state that "something good will happen", which means here that a process will eventually, indeed, be elected (supposing there is at least one process in the network):

assert Liveness1 { some Process => eventually some elected }
check Liveness1 for 3 but 20 steps

Executing the Liveness1 command yields a counterexample, however. The Electrum Visualizer is an extended version of the Alloy one. As you can see in the picture (which has a theme applied where relation id is shown as an attribute), some specific information and exploration means were added:

• Two states are shown side-by-side, allowing a better interpretation of the trace.
• An abstract view of the structure of trace is shown above in the center. Here, the trace is in its initial state 0 and the next state is this very same state, which will actually loop forever.
• The 5 buttons in the tool bar allow the exploration of the trace. The last two simply allow navigating the trace forward or backward (also achievable by clicking in a state of the trace). The other operations explore alternative configurations (static component), initial states, or fork the trace in the focused transition (i.e., alternative next state).

All in all, this counterexample is an infinite trace made of a single state. As in Alloy, you may iterate over counterexamples, in which case you may end up guessing that the problem is that nothing prevents the processes from doing nothing endlessly. This is a classical problem with liveness properties.

One solution is to force communication to happen at every step if it's possible. This can be specified as a progress property that says that, as long as there is a non-empty buffer for some process, then at the next instant, at least one process won't do nothing. Executing this command yields no counterexample.

pred progress {
  always (some Process.toSend => after some p: Process | not doNothing[p]) }

assert Liveness2 { (some Process && progress) => eventually some elected }

check Liveness2 for 3 but 20 steps

Proving safety & liveness

Now that we feel our specification is correct, we can check our properties without taking the steps scope into account. In the Options > SAT Solver menu, check either Electrod/NuSMV or Electrod/nuXmv. (In that case, the Electrod backend should be installed, as well as the NuSMV or nuXmv engine(s) (see the Installation instructions to do so).) Then, executing the commands will overlook the specified steps scope and check the assertions over all possible traces of the specification. On the other hand, the scope on the other signatures (the first-order domain) remains bounded as in plain Alloy.

Notice that this form of unbounded analysis may be very long (or even unfeasible in practice), depending on the complexity of your specification. Hence it is probably better to rely on it once you think your specification is correct.

As of this writing, the nuXmv tool is sometimes buggy and may fail unexpectedly for some specifications. On the other hand, it is usually far more efficient than NuSMV.

Complete model

Here is the full model, for completeness:

open util/ordering[Id]

sig Id {}

sig Process {
  succ: Process,
  var toSend: set Id, // mind the 'var' keyword
  id : Id } 

fact distinctIds { id in Process lone -> Id }

fact ring { all p: Process | Process in p.^succ }

var sig elected in Process {} // mind the 'var' keyword

fact defineElected {
  no elected  // empty in the inital state
  always elected' = { p: Process | (after p.id in p.toSend) and p.id !in p.toSend } }

pred communication [p: Process] {
  some identifier: p.toSend {
    p.toSend' = p.toSend - identifier
    p.succ.toSend' = p.succ.toSend + (identifier - prevs[p.succ.id]) } }

pred init { all p: Process | p.toSend = p.id }

pred doNothing [p: Process] { p.toSend' = p.toSend }

fact traces {
  init
  always all p: Process | communication[p] or communication[p.~succ] or doNothing [p] }

pred consistent {}

run consistent for 3

assert Liveness1 { some Process => eventually some elected }

check Liveness1 for 3 but 20 steps

pred progress {
  always (some Process.toSend => after { some p: Process | not doNothing [p]}) }

assert Liveness2 { (some Process && progress) => eventually some elected }

check Liveness2 for 3 but 20 steps

assert Safety {
  always all x : elected | always all y : elected | x = y }

check Safety for 3 but 20 steps