An overview of Electrum

In this chapter we will explain how Electrum can be used to explore the design of a very simple software component, namely the well-known trash bin. The aim is to give a brief, at times superficial, overview of how to specify and analyse a software design with Electrum. The full details of the Electrum specification language and analysing techniques will be given in the following chapters.

Trash bin

The goal of the trash bin is to enable deleted files to still be restored until an (undoable) decision of emptying the trash is made. More specifically, when a file is deleted it is stored in the trash bin. While still in the Trash, a file can be be restored. After emptying, the files contained in the Trash are permanently deleted.

More specifically, we will show how Electrum can be used to conduct the following tasks:

  1. Formally specify, at a very abstract level, the design of the structure and behavior (operations) of the Trash component.

  2. Validate this design specification by simulation, namely use the Electrum Analyzer to check that it allows some of the expected behaviours of the trash.

  3. Elicit and verify some of the expected properties of the trash bin component.

Specifying a software design

Transition systems are one of the most standard formalisms to reason about the behaviour of a system, and are a very convenient and abstract formalism to describe and reason about the design of a software system. A transition system contains the different states the system may be in while evolving over time, identifying which of these are possible initial states, and clearly depicting how the system can evolve by identifying the transitions that connect each state to every possible succeeding state.

The first step when specifying a transition system in Electrum is to describe the structure of its states. In Electrum, likewise Alloy, the structure of a system is described in terms of sets and relations. In Alloy parlance sets are usually called signatures, and are declared using the keyword sig followed by a mandatory signature name and an optional list of field declarations enclosed between brackets. Fields are relations that connect elements of the enclosing signature to other elements. We will not use fields in this chapter, so our signature declarations will always have a pair of empty brackets after the name.

In Alloy, signatures are inhabited by the so-called atoms, elements without any internal structure or any particular semantics attached, and whose names will be automatically generated by the Analyzer. In Alloy the value of all signatures and relations is immutable. In fact, there is no implicit notion of time or state, and to specify evolving systems it is usually necessary to explicitly specify the notion of time and of execution traces. This is often a rather time-consuming and error-prone task. The Electrum extension of Alloy was proposed precisely to address this shortcoming. Electrum has an implicit notion of time and allows the declaration of mutable signature and relations. To declare a mutable (or variable) signature just add the var keyword before the signature declaration.

Note

Is plain Alloy still useful?

The reader may wonder if plain Alloy, where all signatures and relations are immutable, is in anyway useful. In fact, in many software systems the main design problem concerns just the structural aspects, for example, to elicit requirements about the involved data structures. We will give an example of this in the Structural design with Alloy chapter. As pointed out by Daniel Jackson in the paper Alloy: A Language and Tool for Exploring Software Designs [CACM19], not committing in a particular model of time (as Electrum does) can sometimes be an asset, because it can allow the flow of time to be specified in away that is more convient for a particular problem.

At a very abstract level, we can describe the state of our trash bin component using two sets: the set of files existing in the file system at any time, and the subset of those that are currently in the trash bin. In our Electrum specification we will thus declare two variable signatures: File and Trash, respectively. To signal that the latter is a subset of the former, in the declaration of Trash we will use the keyword in followed the name of the including signature. The Electrum specification of the trash bin state is thus as follows.

var sig File {}
var sig Trash in File {}

In this example, the signature File is a top-level signature, one not contained in any other signature, while Trash is a sub-set signature. In Alloy all top-level signatures are disjoint. The same is true in Electrum for variable top-level signatures: they are always disjoint, even at different points in time, meaning that an atom cannot move from one top-level signature to another.

Having described the state of our system we can now proceed to specify its intended behavior, namely what are the initial states and transitions of the trash bin transition system. Unlike many formal specification languages, Electrum has no special syntax to declare this transition system. Instead it follows the idea, introduced by Leslie Lamport in the Temporal Logic of Actions [TLA], of specifying this transition systems implicitly by means of a temporal logic formula that recognises which are its valid execution traces. A trace is an infinite sequence of states, fully describing a possible behavior of the system.

The formula specifying the transition system is typically decomposed in two parts: one formula that specifies which are the valid initial states, and another that specifies which transitions are possible at each state. In the case of our example, in the initial state we have an empty trash bin. To test a set for emptiness we can use the keyword no followed by the set expression to be checked (to check that it is non-empty we can use the keyword some, and to check that it contains at most one element the keyword lone). To impose a constraint to restrict the valid traces of a system we can use the keyword fact followed by an optional identifier and a formula enclosed between brackets. If that formula contains no special temporal operators, namely if it a normal first-order formula that somehow constraints the values of the sets and relations in the state, then it is only required to hold in the initial state of every trace. In our example, the valid initial states can thus be specified by the following fact.

fact init {
  no Trash
}

To specify the valid transitions, it is easier to first think about the events (or operations) in the system. Each event will give origin to many transitions. In the case of the trash bin we have three events: delete a file, restore a file, and empty the trash. To specify an event, we will write a formula that holds in a particular state of a trace iff that event can occur in that state and the next state of the trace is a valid outcome of the event. These two conditions are usually called the guard and the effect of the event, respectively. To specify the effect we need to somehow evaluate the value of a formula in the next state or refer to the value of sets and relations in the next state. To evaluate a formula in the next state we precede it with the temporal operator after. To evaluate an expression in the next state we append it the operator '. For readability reasons, it is convenient to specify each event in separate predicates. A predicate is a named formula that will only hold when invoked (for example in a fact). To declare a predicate the keyword pred should be used, followed by the predicate name, an optional list of predicate parameters, and a formula enclosed between brackets. For example, the empty trash event can be specified by the conjunction of three formulas as follows.

pred empty {
  some Trash and       // guard
  after no Trash and   // effect on Trash
  File' = File - Trash // effect on File
}

The first condition is the guard of our event, and it states that the trash can only be emptied in a state if the set Trash contains some files. After the guard we have two conditions to specify its effect. When specifying an event we should consider what is its effect on all variable sets and relations that comprise the state. If nothing is specified about a particular variable set or relation, then there will be no constraints restricting how that set or relation can evolve, meaning that it can change freely when the event occurs. If the intention was for that set or relation to remain unchanged when the event occurs, then an explicit formula stating that the value in the next state is the same as the present value must be added. Such “no change” effect conditions are usually called frame conditions. In the case of the empty trash event, the first effect condition states that in the next state the Trash set will be empty (this effect could alternatively be specified by no Trash'), and the second effect condition states that the value of the File set in the next state is the result of subtracting the set of files in the Trash from its current value (operator - denotes set difference, & set intersection, and + set union).

Tip

Increasing the readability of your specification

Alloy has a dual syntax for boolean operators: they can be both written with the typical programming language style operators, but also using the respective english words. We have ! and not for negation, && and and for conjunction, || and or for disjunction, => and implies for implication, <=> and iff for equivalence. Alloy syntax was designed to be very clean and readable. The use of the english version of the operators further increases the readability of the specifications, and will be the preferred style in this book. In a fact or predicate, formulas written in different lines are implicitly conjoined, so the and keywords at the end of the first two lines in the empty predicate are not needed, and omitting them further increases the readability of the event specification.

The delete file event occurs when a file (not currently in the trash) is moved to the trash bin. This event can be specified by the following predicate, parametrised by the file to be deleted. Notice the frame condition on File: moving a file to the trash bin does not permanently delete it, and so the set of files in the file system remains unchanged.

pred delete [f : File] {
  not (f in Trash)   // guard
  Trash' = Trash + f // effect on Trash
  File' = File       // frame condition on File
}

Important

Everything is a set!

The attentive reader might wonder how the expression Trash + f in this predicate type checks, since the union operator is being applied to the set Trash and the file atom f. In Alloy every expression denotes a set, and in particular the value of a variable is a singleton set containing just the value of that variable. So the f in Trash + f is a set of files, just like Trash, and the union of both can be done without any problem. This may seem rather strange at first, but it is one of the nice details of Alloy, that further contributes to simplify its semantics and syntax, by substantially reduce the number of operators in the language. Another example is the in operator which in fact tests for set inclusion and not set membership, as one might expect. Again, since f denotes a singleton set, expression f in Trash is indirectly checking that f is a member of Trash, so the same in opertor can easily be used for both purposes.

The restore file event specification is very similar to the one of delete file.

pred restore [f : File] {
  f in Trash         // guard
  Trash' = Trash - f // effect on Trash
  File' = File       // frame condition on File
}

Having specified our three events, we now need to constraint the valid transitions of the system. This can be done by imposing that at each possible state during the system evolution one of the three event must hold. To impose a constraint on all the states of a trace we can use the temporal operator always followed by the desired formula. With this operator we can easily specify the valid transitions of our trash bin example as follows.

fact trans {
  always (empty or (some f : File | delete[f] or restore[f]))
}

Note the usage of the existential quantifier some to “pick” at each state the file to be deleted or restored.

Validating a design specification

Now that we have a first specification of the intend behavior of the trash bin, and before proceeding with the verification of its expected properties, it is advisable to validate it to check if indeed it behaves as expected. A typical way to perform such validation is by using some sort of user-guided simulation. The Electrum Analyzer has several mechanisms to allow the user to explore and validate a design, including an interactive exploration mode akin so simulation [FIDE19].

A distinguishing feature of Alloy is that analysis commands can be included together with the declarations and facts in a specification. There are two analysis commands, both accepting wither a predicate or a formula enclosed in brackets (and in this case an optional command name): run commands instruct the Analyzer to check the satisfiability of the formula (and the declared facts), yielding a satisfying instance if that is the case; check commands instruct the Analyzer to check the validity of the formula (assuming the declared facts to be true), yielding a counter-example instance if that is not the case. In the case of Electrum, an instance is a valid execution trace, an infinite sequence of states, each a valuation of the declared sets and fields.

Note

Instances or models?!

When presenting the semantics of a logic, instances of formulas are usually known as models: a model of a formula is a valuation of its free variables that makes the formula true. In Alloy the term model is frequently used to denote the specification of a system, and the term instance is used to denote a satisfying valuation. This use of the term model in Alloy parlance is consistent with other techniques and languages for software design, namely the Unified Modeling Language, where a software model is precisely the kind of artefact we have been denoting by a specification.

Another distinguishing feature of Alloy is that the instances returned by the analysis commands are depicted graphically as graph like structures: atoms belonging to the different sets are nodes (depicted as boxes) and relations are edges (depicted as arrows). Moreover, this graphical depiction can be customised using themes, namely it is possible to customise the colors and shapes of nodes and edges according to the sets and relations they belong to.

The usual way to start validating a specification is to define an empty run command: an empty formula is equivalent to true, and this command basically asks for an instance that satisfies all the declared facts. If none is returned then the facts are inconsistent and most likely our specification of the system is buggy and needs to be corrected. To kick-start the simulation process we will add an empty command (named example) to our specification.

run example {}

To execute the single command of a specification, or to re-execute the last command, just press cmd-e or the Execute button in the top of the Analyzer window. If you have multiple commands, to choose which one to execute go to the Execute menu and select the desired command. If the commands are named you will see the names there, otherwise you will see an automatically generated name composed by the type of command (run or check) followed by a $ and a sequential numeric identifier. After executing the example command we get the following instance.

../_images/instance1.png

Here we see a depiction of an execution trace that satisfies our specification. Bellow the first row of buttons, the Electrum visualiser shows a depiction of the instance trace, which in this case consists of two states, with the second behing followed by a loop back to the initial one. This trace is thus an infinite alternating sequence of the two states. All traces returned by the Electrum Analyzer will be of this kind: a finite sequence of states followed by a loop back to one of the previous states. All the execution traces are infinite but the tool only returns and depicts traces that can be represented finitely. In the lower part of the window the visualizer focus on a particular transition of the trace, depicting the pre- and post-state in the typical Alloy style: the atoms are named sequentially according the signature they belong to, and atoms belonging to a sub-set signature (such as Trash) are labeled with that signature name. The two states being depicted are the ones shown in white in the trace, all will be kept centered in the trace depiction. When the visualizer window pops up the transition being the depicted is always the first one, with the state on the left hand side being the initial state of the trace. In this example, we can infer that the first transition was due to a file deletion: initially we have three files, none of them in the trash, and in the second state File2 is in the trash: the only event that could have caused this transition is a deletion.

To navigate in the trace, namely to move forwards and backwards to focus on a different transition, just press the or button, respectively. For example, by moving forward to focus on the second transition we get the following.

../_images/instance2.png

The second transition was caused by a restore event: in the pre-state File2 is in the trash and in the post-state it is no longer there. As such we can conclude that our first instance is an infinite alternation between deleting and immediately restoring File2, which is a valid execution of the system.

Note

Displaying the event corresponding to a transition

The Electrum instance visualiser does not show the event that corresponds to a transition. Actually, there is no notion of event in Electrum: our events where modeled by three normal logic predicates, so there is no way for the visualiser to know these are events that should be treated specially. Another problem is that a transition may not correspond to just one event: many times two different events can yield the same transition, and at this abstract level of specification there is no way (nor interest) in distinguishing which one actually occurred. In most examples, namely simple ones like our running example, it is kind of trivial to infer which event occurred. However, in some more complex designs that is not the case. In the chapter Methodology and tips we will present an Electrum idiom that allows the visualisation of the name (or names) of the events that could have caused each transition.

In the top of the Electrum instance visualiser window we can find three buttons, that can be used to ask the Analyzer for alternative instances:

Next Config

This button asks for a new trace that differs in the values of immutable sets and relations. Usually, immutable elements constitute the configuration of a system (for example, describing a specific network topology where a protocol is to be executed), and by pressing this button we will get an execution trace on a different configuration. In this example, all our sets are variable, so this button is of no interest.

Next Init

This button asks for a new trace with a different initial value for mutable sets and relations, allowing us to quickly explore a scenario starting with different initial conditions.

Fork

Finally, this button asks for a different trace with the same behavior up to the (left-hand) pre-state we are currently focused, but a different transition at this point. If that is possible, the pre-state will remain the same and we will see a different post-state. The latter could be a different result for the same (non-deterministic) event, or the outcome of a different event.

For example, if at this point we press Fork we could get the following instance.

../_images/instance3.png

In this (different) trace, the second transition is another deletion (of file File1) instead of a restore (of File2). Our trace now starts with a deletion of File2 followed by an infinite alternation of these two events. The Fork button is the main tool used while validating a design specification, since it allows us to explore alternative behaviours in a very similar way to simulation modes in other formal verification or model checking tools.

Before proceeding with the validation of our design, let’s customise our visualisation, for example by setting a different color for files in the trash. To do so just press the Theme button. On the left-hand side you will see many theme customisation options. Just select the set Trash, and in the first drop-down menu on the top left-hand select the color red, as follows.

../_images/theme.png

After selecting Apply and than Close our trace will now be displayed as follows.

../_images/instance4.png

There are many options in the theme customisation, and when dealing with larger more complex systems this will become an extremely useful feature to help better understand execution traces. We will further discuss themes and give some tips about how to use them in the Methodology and tips chapter.

If we now press Next Init, to ask for a different initial valuation of our sets, we get the following trace, where initially we have two files in the file system instead of three.

../_images/instance5.png

By pressing Next Init one more time we get a trace where initially we have just one file, and if we press again we get the following message.

../_images/nomore.png

This may seem rather surprising at first. First, why isn’t the Analyzer returning instances where, for example, initially we have more than three files!? Second, why isn’t the Analyzer returning instances where, for example, initially there are two files named File1 and File2 instead of File0 and File1 as above!? The former is due to scopes. To enable automatic analysis, Alloy imposes a bound on the size of all signatures. This bound is defined by a scope on commands. By default the scope is 3 for all top-level signatures, meaning that instances will only be built using at most three atoms for each top-level signature. This scope can be changed by using the keyword for after a command, followed by the desired global scope for all top-level signatures. It is possible to set a different scope for specific signatures, by following this global scope by the keyword but and a list of comma separated scopes for different signatures. For example, if our run command was instead

run example {} for 5

we could get the following instance.

../_images/instance6.png

The second omission is due to symmetry breaking. As mentioned before, atoms have no semantics attached. In particular, the names the Analyzer creates for them are meaningless: File0 isn’t the name of a particular file existing in a real-world file-system, but just a random name to help us distinguish it from other files. As such, two instances that only differ in the names of the atoms are in fact the same instance (they are isomorphic up to atom renaming), and showing both to the user would just encumber the understanding of the specification. To avoid this, and also to speed up analysis, the Analyzer implements a powerful symmetry breaking mechanism that excludes from the search most isomorphic (symmetric) instances.

To conclude our validation let’s try to find a concrete trace example using the Analyzer, namely one where initially we have a single file, which is than deleted, and finally the trash is emptied. To do so we re-execute our example run command, and press Next Init until we get the desired initial state.

../_images/instance7.png

The first transition is the desired one, corresponding to the deletion of the single file File0. We press to move to the second transition, which in this trace corresponds to the recovery of the previously deleted file.

../_images/instance8.png

To ask for a different transition, namely one corresponding to a trash emptying event, we press Fork. Surprisingly, instead of different next state with no files, we get the no more satisfying instances window!

../_images/nomore.png

This means that this execution trace, which for sure we want to allow in our system, is not currently considered valid according to our specification. In fact, the current specification does not allow all files in the file system to be permanently deleted, as we can confirm by defining the following run command, now with a formula, which asks for a trace where we reach a point where there are no files. Executing this command yields no instances, which clearly indicates that our specification is wrong.

run no_files { eventually no File } for 5

In this command’s formula we used the temporal operator eventually: a trace satisfies this operator if the ensuing formula is true at least on one of the states of the trace.

So what is the problem with our specification? The issue is that fact trans imposes that at any point in time one of the three events (delete, restore, or empty) must occur. Since empty has a guard requiring the trash to have some files, in fact none of these three events can occur when there are no more files. To fix our specification there are many options. We could, for example, specify an event allowing the creation of new files. Or, to keep the focus of our specification just in the operations concerning the trash, we could add an event that accounts for the (very real) possibility that the user of our system is doing something else that does not affect the trash bin. When considering only the sets in our abstraction of the trash bin, this event will have no effect at all, so its specification is just composed of frame conditions.

pred do_something_else {
  File' = File
  Trash' = Trash
}

We can now fix our specification of the valid transitions as follows.

fact trans {
  always (empty or (some f : File | delete[f] or restore[f]) or do_something_else)
}

If we now re-execute the no_files command we get the following instance, where we basically never have any files, which, although a bit surprising, should be considered as a valid instance of our design.

../_images/instance9.png

Note

A quicker way to detect our problem

The attentive reader could notice that actually the problem with our specification could have been detected much earlier in this validation process. In our first execution of the example command, when pressing Next Init to get instances with a different number of files in the initial state, after getting an instance with just one file the no more satisfying instances poped up. At this point we could have noticed that the Analyzer was not yielding an instance with no files at all in the initial state, something that should have been possible.

To search for a more interesting instance we could either do a “simulation” starting with command example and using and Fork until we get to a point where the thrash is empty, or just change the no_file command to search directly for a more interesting example, where initially we have some files but eventually they are all permanently deleted.

run no_files {
  some File
  eventually no File
} for 5

Executing this command yields an instance with a single file that is immediately deleted. By pressing we get to the following transition corresponding to the emptying of the trash.

../_images/instance10.png

Verifying expected properties

After validating our design we now proceed with the specification and verification of some of its expected properties. To exemplify, we will consider the following (rather trivial) properties, but many more could be specified about this example.

  1. Every restored file must have been previously deleted.

  2. If all files are in the trash and we empty it then no more files will ever exist.

A nice thing about Alloy and Electrum is that the same logic is used to both specify the system and its expected properties. In many formal specification languages and verification tools (namely, most model checkers), a different language is used for each. In Electrum we use temporal logic, of which we already saw some of the key operators, namely always and eventually. So far our formulas consisted of exactly one of these operators followed by some constraint, so the meaning of the formula was easy to grasp: in the case of always, the ensuing formula must be true in all states of a trace for it to be considered a valid instance, and in the case of eventually the formula must be true at least in one state. However, formulas can contain several of these operators, potentially nested, which further complicates their understanding. As detailed in the A temporal logic primer chapter, a temporal formula is in fact evaluated in a particular state of a trace. The outermost formula is evaluated in the initial state, but nested temporal formulas may be evaluated in different states of the trace depending on the enclosing temporal operator. So, the (informal) semantics of the temporal operators is the following:

always

When evaluated in a particular state, the ensuing formula must be true in that state and all the following states.

eventually

When evaluated in a particular state, the ensuing formula must be true in that state or in at least one of the following states.

after

When evaluated in a particular state, the ensuing formula must be true in the next state (which always exists, since traces are infinite).

We will now introduce a couple more temporal operators that may come in handy. These temporal operators are of a different nature of the above, because they constrain the past behavior, while those we have seen so far constrain the future behavior.

historically

When evaluated in a particular state, the ensuing formula must be true in that state and all the previous states.

once

When evaluated in a particular state, the ensuing formula must be true in that state or in at least one of the previous states.

Properties to be verified by check commands should be written in assertions. An assertion is declared with the keyword assert, followed an identifier, and a formula enclosed between brackets. For example, the first property above could be specified as follows.

assert restore_after_delete {
  always (all f : File | restore[f] implies once delete[f])
}

Here we have an example of a nested temporal operator. The outermost always imposes that the formula all f : File | restore[f] implies once delete[f] is true in all states of the execution traces. The all in this formula is an universal quantifier, meaning that in all states restore[f] implies once delete[f] must be true for every file f in the file-system. This formula imposes that whenever the restore event for a particular file is observed in a state, the delete event for that very same file must have been observed before. To verify this assertion we can use a check command followed by the assertion name to be checked.

check restore_after_delete

This command yields no counter-example instances, meaning that the assertion is most likely valid. Note that the command has an implicit scope on top-level signatures, so this result means that the assertion is valid for file-systems with up to 3 files. In Electrum commands also have a scope on the size of the finite prefix of traces that precedes the mandatory loop-back. By default this scope is 10, meaning that the verification only checks for counter-example traces with at most 10 different states (and transitions). This is a verification technique known as bounded model checking. The Electrum Analyzer searches for counter-examples of increasing length, and is guaranteed to return the shortest one, if some exists. To change this bound just set the scope of the special signature Time. For example, to verify the above property for file systems with up to 5 Files and traces with at most 20 different states the scope could be set as follows.

check restore_after_delete for 5 but 20 Time

This command also yields no counter-examples. With such a large scope it is thus very likely that our property is indeed valid. Although the analysis is always bounded in respect to the signatures, in Electrum we can perform unbounded model checking in respect to the size of the traces, essentially verifying properties for traces composed by an arbitrary number of states. To do so we must first choose a solver in the Options menu that supports unbounded model checking. At the moment only the nuXmv solver supports that feature. The solver is the analysis tool that the Analyzer uses in the backend to perform the actual search for instances and counter-examples. For bounded model checking, many different solvers can be used: some of them may be considerably faster than others in particular examples, so it is always worthwhile to try them out if your analysis commands are very slow. To verify our property for file systems with up to 3 Files and traces of any length the scope could be set as follows.

check restore_after_delete for 3 but 1.. Time

Again, no counter-examples are found!

The second property can be specified as follows.

assert delete_all {
  always ((Trash = File and empty) implies always no File)
}

Basically, in every state where the formula Trash = File and empty holds (all files are in the trash bin and the empty event occurs) the formula no File (no files exist) must forever hold. To verify this property (with bounded model checking) we could issue the following command.

check delete_all

Surprisingly, this command yields the following counter-example with three different states, of which we show the first two transitions.

../_images/instance11.png ../_images/instance10.png

On first sight, this trace does not look like a valid counter-example, since after deleting the only existing file and emptying the trash the file system remains forever empty. The problem in this case is that our specification of the property is buggy (and not the specification of the system, which hopefully is still correct). The semantics of the temporal operator always requires the ensuing formula to also hold at the state where the formula is evaluated, so in the above specification we where actually demanding that the file system is empty also in the same state where the empty event occurred. This is not what we wanted: instead we should have required that the file system remains forever empty, but starting only in the (post-)state after the occurrence of the empty event. We could fix our specification of the property by adding an after operator before the innermost always.

assert delete_all {
  always ((Trash = File and empty) implies after always no File)
}

Now the check command no longer yields a counter-example, and we can conclude that our trash bin design most likely satisfies these two properties!