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 very 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 model is also available in the Electtrum 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 a identifier (it may for instance be a MAC address). Furthermore, each process holds a set of identifiers 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.

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

• its identifier;
• a "pointer" to its successor process;
• a set 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 }

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 {}

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 }

---

For a second reading: what is the upper bound of a toplevel variable signature?

In Electrum, as much as in Alloy, every variable signature should have an upper bound for commands to be executed. Now suppose we introduce a toplevel variable signature A as follows:

sig B {}

var sig A {}

check someCommand for 3 but 4 A

Morally, this is equivalent to introducing another static, parent signature for A, say Hull_A, and to execute the command on this new signature, i.e.:

sig B {}

sig Hull_A {} // introduce fresh, static signature

var sig A in Hull_A {} // 'A' is a subset of 'Hull_A'

check someCommand for 3 but 4 Hull_A // the scope is actually on 'Hull_A' 

This choice ensures that, at every instant, A is a subset of Hull_A and that the atoms that may belong to A are fixed.

---

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

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

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 (apart from the first), this set contains the processes that must send their own identifier while they did not have to at the previous one. Said otherwise: they were just sent their identifier, which means it passed through the whole ring and came back to them:

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