# New Electrum Release Candidate (towards Alloy 6) **URL:** \ **Category:** Alloy 6\ **Created:** [September 11, 2020, 1:51pm UTC](https://alloytools.discourse.group/t/new-electrum-release-candidate-towards-alloy-6/87 "2020-09-11T13:51:23Z")\ **Posts on this page:** 2\ **Page:** 1
**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\ **Post date:** [September 11, 2020, 1:51pm UTC](https://alloytools.discourse.group/t/new-electrum-release-candidate-towards-alloy-6/87/1 "2020-09-11T13:51:23Z")
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](https://github.com/haslab/Electrum2/releases/tag/v2.1rc2). We deeply thank our colleague Nuno Macedo for leading the development. The current specification draft is [there](https://github.com/haslab/Electrum2/wiki/Language), comments are welcome! # Issues Please use the [issue tracker](https://github.com/haslab/Electrum2/issues) 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"`. ---
**Author:** ![grayswandyr](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/grayswandyr/32/17_2.png) [@grayswandyr](https://alloytools.discourse.group/u/grayswandyr)\ **Post date:** [September 11, 2020, 2:43pm UTC](https://alloytools.discourse.group/t/new-electrum-release-candidate-towards-alloy-6/87/2 "2020-09-11T14:43:58Z")
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` .