The goal of the MERC project is to provide a generic set of libraries and tools for (specification language-agnostic) model checking, written in the Rust language. The name is an acronym for "mCRL2 except Reliable & Concurrent", which should not be taken literally.
We aim to demonstrate efficient and correct implementations using Rust. The main focus is on clean interfaces to allow the libraries to be reused as well. The toolset supports and is tested on all major platforms: Linux, macOS and Windows.
The toolset is still in quite early stages, but contributions and ideas are more than welcome so feel free to contact the authors or open discussion. Compilation requires at least rustc version 1.85.0 and we use 2024 edition rust. 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 the --release flag. Several tools will be build that can be found in the target/debug (or release) directory. See CONTRIBUTING.md for more information on the testing and formatting of code. Copilot is used for reviewing and occasionally boiler plate code can be written by AI, but slop is strictly forbidden. Extensive (random) testing under various sanitizers and miri is used to gain confidence in the unsafe parts of the implementation.
Bugs and issues can be reported in the issue tracker.
Various tools have been implemented so far:
merc-ltsimplement various (signature-based) bisimulation algorithms for labelled transition systems in the mCRL2 binary.ltsformat and the AUTomaton (or ALDEBARAN).autformat.merc-rewriteallows rewriting of Rewrite Engine Competition specifications (REC) using Sabre (Set Automaton Based REwriting).merc-vpgcan be used to solve (variability) parity games in the PGSolver.pgformat, and a slightly extended variability parity game.vpgformat. Furthermore, it can generate variability parity games for model checking modal mu-calculus on LTSs.merc-pbescan identify symmetries in paramerised boolean equation systems PBES, located in thetools/mcrl2workspace.merc-ltsgraphis a GUI tool to visualize LTSs, located in thetools/GUIworkspace.
Various crates are also published on crates.io, see the crates directory for an overview.
The work is licensed under the Boost Software License, see the LICENSE for details. Third party dependencies have additional license terms, which are included in the 3rd-party directory. Furthermore, cargo deny is used to ensure that no crates.io dependencies with incompatible licenses are added.
This tool set is inspired by the work on the mCRL2 toolset, the work on a specification language agnostic toolset ltsmin and the work on CADP.
This project is developed at the department of Mathematics and Computer Science of the Technische Universiteit Eindhoven.