v1.0

[mlaveaux]

v1.0

The initial release of the MERC toolset. Although no where near feature complete we opted to produce a 1.0 release to mark the initial milestone of the toolset instead of staying in zero version forever. We generally expect to release a single major version per year, without focusing too much on avoiding breaking changes to libraries for foreseeable future.

This release comes with a set of five tools:

• merc-lts implement branching, strong and weak (signature-based) bisimulation reduction and comparison for labelled transition systems in the mCRL2 binary .lts format and the AUTomaton (or ALDEBARAN) .aut format.
• merc-rewrite allows rewriting of Rewrite Engine Competition specifications (REC) using Sabre (Set Automaton Based Rewrite Engine).
• merc-vpg can be used to solve (variability) parity games in the PGSolver .pg format, and a slightly extended variability parity game .vpg format. Furthermore, it can generate variability parity games for model checking modal mu-calculus on LTSs.
• merc-pbes can identify symmetries in paramerised boolean equation systems PBES.
• merc-ltsgraph is a GUI tool to visualize LTSs.

This release also comes with various crates that can be used, these are also published on crates.io:

• merc_aterm: A feature complete thread-safe re-implementation of the mCRL2 aterm library in Rust. Can read and write aterms in (streamable) binary and text formats.
• merc_data: Defines data expressions mimicking the mCRL2 data expressions, demonstrates the use of Rust macros (defined in merc_macros) to generate the required boiler plate code.
• merc_lts: library for manipulating labelled transition systems, including I/O for mCRL2's .lts files and Aldebaran .aut files. Can also generated random LTSs and (synchronous) products for testing purposes.
• merc_sharedmutex is a crate implementing the busy-forbidden protocol, a read-efficient readers-writer lock described in the preprint.
• merc_syntax defines a Pest grammar for the mCRL2 specification, modal formula and PBES languages, and defines an AST for these languages.
• merc_vpg defines functionality for manipulating (variability) parity games, including I/O for the PGSolver .pg format and a slightly extended variability parity game .vpg format.

Full Changelog: https://github.com/MERCorg/merc/commits/v1.0

---

This discussion was created from the release v1.0.