Electrum V2.1

[nmacedo]

Major

• Support for decomposed solving
• Small language changes
• Updated Pardinus backend
• New iteration operations and improvements to existing
• Several interface/reporting improvements
• Sample Alloy models and util libraries compatible with Electrum

Detailed

• Support for decomposed solving re-introduced after being dropped after 2.0 transition (Support decomposed solving #38)
• Updated Pardinus backend to v1.2.2 fixing several issues (Possible problem with symmetry breaking #3,Number of vars displayed #6,Fatal error on examples #14,State numbers not displayed in 2.0.1 #15,Allow integers with electrod backend #18,Fix vars displayed for Pardinus backend #20,Missing unsat cores #37,Invalid int identifiers in export instance as LTL #43,Export instance as LTL does not consider the mutable universe #45,The fork button misses some traces #48,New config when no static sigs gives new solution #49)
• Instances can now be serialized into a runnable Electrum LTL formula (Serialize a simulation result as a scenario #1,Invalid int identifiers in export instance as LTL #43,Export instance as LTL does not consider the mutable universe #45,Implement export to LTL at the Alloy level  #51)
• Reporting of solving process iterative, shows current state being solved
• Variables shown now accumulate all steps of the iterative temporal solving process (Number of vars displayed #6,Fix vars displayed for Pardinus backend #20)
• Variables shown accumulate all integrated problems of the decomposed solving process
• Fixed bug on painting temporal elements in vizualizer (Identification of var sig in themes overrides user #17)
• Fixed/updated the labels on navigation buttons (Better navigation ops labels #19,Trace navigation issues #22,Bad labels when hovering over navigation buttons (next state, previous state, etc.) #42)
• Reinstated state identifiers on trace snapshot, denotes the identifier of the state in the prefix, not necessarily distinct (State numbers not displayed in 2.0.1 #15)
• Updated legacy Alloy models to avoid conflicts with Electrum (Update legacy models to avoid conflicts #27)
• Variable seqs are now supported after updating seq Alloy lib (Are seq supported? #21)
• Fixed a couple of issues with precedences of temporal operators (Parsing issue on formulas #24,Precedence of ; vs quantifiers ok? #31)
• Scope on the prefixed length changed from Time to steps (Change Time scope by step #26)
• Tweaked error reporting so that "execute all" can still terminate when incompatible solver selected (Execute All crashes when using a SAT solver and there are 1.. commands #25)
• Variable sigs as exact module parameters also throws an error (Address "exactly" annotation in module parameters for var sigs #28)
• Better error reporting for invalid temporal formulas (eg, total order) (Orderings on var sigs throw fatal error #29)
• Scopes on variable sub-sigs forbidden, were not compatible with the semantics (Scopes on variable subsigs are not consistent with the semantics #33)
• Updated the Kodkod to Java printer with Pardinus solving options (time scopes) (Update the translate kodkod to java printer #34)
• Iteration operations updated to the API of Pardinus 1.2, only incremental SAT (Update iteration to new pardinus api #35,Properly handle backends without iteration support #36)
• Fixed imports when using extension .md (module imports from .md files search for mangled filenames #40)
• Added pre-compiled amd64 electrod (Pre-package electrod binaries #39)
• Fixed zooming in the two-state visualizer (Zoom only works on one of the step windows #44)
• Added support for "new path" iteration, disabled after next init/state
• Disable "new config" iteration when no static elements (sigs/fields)