-
Notifications
You must be signed in to change notification settings - Fork 4
Tutorial
This brief tutorial to Electrum is aimed at users already fluent in Alloy and covers Electrum v2.1+.
We also suppose that Electrum Analyzer is already installed.
In a nutshell, Electrum is an extension of Alloy with:
- A keyword ("
var
") to declare some fields and signature as variable (i.e. their valuation may vary along time); - Connectives from Linear Temporal Logic with Past (PLTL) to express properties of traces;
- Primed expressions that represent the value of the said expressions in the next instant (so the prime sign is, contrary to Alloy v4/v5, not a valid character for identifiers);
- 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:
- Most of the relations that were indexed by
Time
will usually be just taggedvar
; - You need not join variable expressions with an expression denoting an instant;
- You must replace quantifications over time by the corresponding, classic LTL operators (e.g.
always
,eventually
...); - 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).
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.
In Electrum modelling terms, the above is summed up by introducing a Process
signature, with three fields:
- its identifier
id
of a totally-ordered typeId
(this is not strictly necessary, as we could have specified a total order onProcess
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, butnext
is already used in theutil/ordering
Alloy module, that we kept in Electrum, so we chose to call this operatorafter
to avoid name clashes.) - finally, the prime symbol (following
elected
) is a facility to talk about the value ofelected
at the next instant (soafter
applies to constraints while the prime symbol applies to expressions).
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]) } }
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 }
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 steps
. steps
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 transitions. If you don't specify anything, the default bound for steps
is 10.
As in Alloy, the scope on steps
can be declared exact using the exactly
keyword.
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, some specific information and exploration means were added:
- The split view presents two consecutive states. The states currently shown have a white background in the trace depiction just above. Here, we learn that the trace consists of a single state (of index
0
) that repeats forever (this is why the white part of the trace depiction contains twic e the same state0
). Furthermore, a looping edge from the last state to itself tells you that which part of the trace repeats itself indefinitely. Here the trace is just the made of the state0
forever. - Just above(
New ...
buttons), you can explore the instance trace being visualized. We will not address this more advanced topic in this tutorial.
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
Now that we feel our specification is correct, we can check our properties without bounding steps
. 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, change the scope for steps
to 1..
(which means "unbounded"):
check Safety for 3 but 1.. steps
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 !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
check Safety for 3 but 1.. steps