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
tosteps
(#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)