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.

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

1. 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 may terminate, you must still ensure traces are infinite, otherwise your specification may be inconsistent: we shall see later how to achieve this).

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 holds an identifier (it may for instance be a MAC 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 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: obvisouly, 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 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 have 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 receive their own identifier (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 not in p.toSend } }

This fact introduces three new Electrum constructs:

• always is the connective from Linear Temporal Logic (LTL): it means that tthe 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 previous 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 (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 }

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

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

Checking consistency

It's always good to check that an Electrum specification, i.e. that it has at least one instance (a model in the logical sense); otherwise, further checks will be trivially true.

pred consistent {}
run consistent for 3

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 Time

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 an undeclared signature Time. Time is actually a reserved keyword in Electrum and this scope actually states that bounded analysis (as in Alloy) should be performed on infinite traces made of at most 20 different states.

Executing the Liveness1 command (say, with Minisat as a backend) however yields a counterexample:

The Electrum Visualizer is an extended version of the Alloy one. As you can see in the picture (red rectangle), some specific information and exploration means were added:

• In the rightmost part, you can explore the instance trace being visualized. Here, the trace is in its initial state (Time0) and the next state is this very instant (this is what >0 tells you).
• Furthermore, the leftmost part tells you that the suffix starts in this very state and loops back to itself.

All in all, the counterexample is an infinite trace made of a single state. As in Alloy, you may iterate over counterexamples, in which case you may guess that the problem is that nothing prevents the processes from doing nothing endlessly.

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 Time 

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 Time 

Proving safety & liveness

Now that we feel our specification is correct, we can check our properties without taking the Time 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 Time scope and check the assertions over all possible traces of the specification. On the other hand, the scope on the state 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.

---

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 not 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 Time 

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 Time 

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

check Safety for 3 but 20 Time