Alloy with records Beta

records-beta

beta version of alloy with records

Electrum v2.1.5

• fixed a bug where visualizer was in trace mode for static models

Electrum v2.1.4

• re-enabled symbolic bounds (fixed bug on approximation)
• fixed bug on reporting configs (decomposed)
• better management of external processes (electrod)
• cleaned up modified annotations

Electrum v2.1.3

• changed enumeration operation labels
• changed "decomposed strategy" terminology to "decompose strategy"
• support for single quotes ‘ and ’ besides ' in primed expressions
• step parameters logged when solving

Electrum v2.1.2

• Support for trace visualisation other than graph (tree, text, table)
• Updated electrod to 1.0
• Added electrod windows binary
• Fixed importing of .md modules
• Fixed formula simplifier for temporal operators
• Fixed export instance to formula for static instances
• Fixed export instance to formula for empty universes
• Code cleaned up and documented in preparation of Alloy6 PR

Electrum 2.1

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 (#38)
• Updated Pardinus backend to v1.2.2 fixing several issues (#3,#6,#14,#15,#18,#20,#37,#43,#45,#48,#49)
• Instances can now be serialized into a runnable Electrum LTL formula (#1,#43,#45,#51)
• Reporting of solving process iterative, shows current state being solved
• Variables shown now accumulate all steps of the iterative temporal solving process (#6,#20)
• Variables shown accumulate all integrated problems of the decomposed solving process
• Fixed bug on painting temporal elements in vizualizer (#17)
• Fixed/updated the labels on navigation buttons (#19,#22,#42)
• Reinstated state identifiers on trace snapshot, denotes the identifier of the state in the prefix, not necessarily distinct (#15)
• Updated legacy Alloy models to avoid conflicts with Electrum (#27)
• Variable seqs are now supported after updating seq Alloy lib (#21)
• Fixed a couple of issues with precedences of temporal operators (#24,#31)
• Scope on the prefixed length changed from Time to steps (#26)
• Tweaked error reporting so that "execute all" can still terminate when incompatible solver selected (#25)
• Variable sigs as exact module parameters also throws an error (#28)
• Better error reporting for invalid temporal formulas (eg, total order) (#29)
• Scopes on variable sub-sigs forbidden, were not compatible with the semantics (#33)
• Updated the Kodkod to Java printer with Pardinus solving options (time scopes) (#34)
• Iteration operations updated to the API of Pardinus 1.2, only incremental SAT (#35,#36)
• Fixed imports when using extension .md (#40)
• Added pre-compiled amd64 electrod (#39)
• Fixed zooming in the two-state visualizer (#44)
• Added support for "new path" iteration, disabled after next init/state
• Disable "new config" iteration when no static elements (sigs/fields)

Electrum 2.1 RC6

Detailed:

• Disable new config when no static elements (sigs/fields).

Electrum 2.1 RC5

Detailed

• Fixed iteration when in purely static models

Electrum 2.1 RC4

Detailed

• Updated Pardinus to v1.2.3, changed semantics of next state (can now reduce prefix)
• Added support for "new path" iteration, disabled after next init/state
• Fixed export to LTL and prettier printing (#51)

Electrum 2.1 RC3

Detailed

• Updated Pardinus to v1.2.2, addressing several issues (#43,#45,#48,#49)
• Fixed zooming in the two-state visualizer (#44)
• Fixed and cleaned up the export to LTL feature (#43,#45)