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!
Issues
Please use the issue tracker for any bug report, comment, etc.
Limitations
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".