This repository contains a re-implementation of the core functionality of the mCRL2 toolset in the Rust programming language. Its name is an acronym for "mCRL2 except Reliable & Concurrent", which should not be taken literal. The main goal is demonstrate a correct implementation using (mostly) safe Rust, with a secondary goal to achieve similar performance to the C++ toolset.
Compilation requires at least rustc version 1.85.0 and we use 2024 edition rust. Then the toolset can be build using cargo build, by default this will build in dev or debug mode, and a release build can be obtained by passing --release. Several tools will be build that can be found in the target/{debug, release} directory. The GUI tools have to be build separatedly by running the build from the tools/gui directory.
- merc-lts implement various bisimulation reductions for labelled transition systems in the mCRL2
.ltsformat and the Aldebaran.autformat. - merc-rewrite allows rewriting of REC specifications.
- merc-vpg can be used to solve (variability) parity games.
- merc-pbes can identify symmetries in paramerised boolean equation systems (PBES).
- merc-ltsgraph is a GUI to visualize LTSs (located in the tools/GUI/ workspace).
This library is fully inspired by the work on mCRL2.