New Electrum Release Candidate (towards Alloy 6)

Dear All,

on July 21, the Electrum team presented a draft specification of Electrum to the Alloy Board. Considering the specification as well as the already-existing Electrum Analyzer, the consensus was to ultimately merge Electrum into the Alloy main branch to give Alloy 6. Before that, we will release some Electrum release candidates to gather your feedback and solve possible issues.

Release Candidate

This is my pleasure to introduce our first public release candidate. You can find it at on our Github repo. We deeply thank our colleague Nuno Macedo for leading the development.

The current specification draft is there, comments are welcome!


Please use the issue tracker for any bug report, comment, etc.


As of now, notice that:

  • we do not have a Windows 10 version yet
  • integers are not supported yet with the NuSMV and nuXmv backends

Electrum in a nutshell

Electrum is an extension of Alloy with a var keyword to specify that a signature or field is mutable , and with linear-time temporal logic with past (as well as a postfix prime ' operator to forward-translate the denotation of a relational expression by one state).

Interpretation structures are now infinite sequences of states (traces), where a state is a valuation for signatures and fields. The considered traces are represented as lasso traces: that is, finite sequences featuring a loop from the last state back to a former state. Because the last state can be looped back to itself, this is completely general.

The valuation of a mutable signature or field is likely to vary from state to state in a given trace, while static (that is, immutable) ones remain unchanged in a given trace. Due to the possible presence of toplevel mutable signatures, the keywords univ and iden no longer represent constants and should themselves be considered mutable values. On the other hand, the interpretation of a plain old Alloy model (provided it does not use any Electrum syntactic construct) collapses to the usual Alloy semantics.

Analyses proceed as in Alloy by bounding signatures. For the time horizon , however, the user may either decide to bound the possible number of distinct states in a trace (bounded model-checking), or to leave it unbounded (complete model-checking). We remark that, from a theoretical point of view, both techniques terminate. The former is in general faster but limited to a subset of infinite traces, while the latter is complete. In practice, the former is used on a normal basis and the second is used when checking temporal assertions that are thought to be true or that may be false for a bound that is hard to predict.

The language and analysis techniques are implemented in the Electrum Analyzer, a free-software extension of the Alloy Analyzer. The Electrum Analyzer also features a Visualizer enhanced to display traces in a user-friendly way, as well as a sophisticated way to explore alternative instances of a specification.

Plain Ol’Alloy?

If you do not use any Electrum keyword, models are interpreted as plain Alloy 4, except for one case: the prime symbol is interpreted as an Electrum symbol. To adapt your old Alloy models so that they are still interpreted in the old way, you must get rid of primes and replace them with another symbol or character. We suggest using double quotes " as they are already legit Alloy 4. E.g. you may replace t' by t".

1 Like

PS for users of previous versions of Electrum: in order to avoid clashes with Alloy 4, we now use the steps keyword in replacement of Time in the specification of the time horizon in commands:

  • If the time horizon takes the form for M .. N steps , only lasso traces with at least M transitions and at most N ones ( including the looping transition starting in the last state) will be explored.
  • If the time horizon takes the form for N steps , this is equivalent to for 1 .. N steps
  • If no time horizon is given, this is implicitly equivalent to for 10 steps .