v1.1

Added support for reading and writing LTSs in the .bcg format used by the CADP toolset, this is gated behind the cadp feature flag.

Made the AUT format compliant with the original specification. In particular, the internal action is now represented by i instead of tau. This means that merc-lts now requires the --tau=tau flag to read AUT files that use tau as the internal action, as is the case for mCRL2.

See the README.md of the individual crates for their own changelogs.

Full Changelog: v1.0...v1.1

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