The Git repository for the mCRL2 toolset.
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.vim Added operator keywords Dec 18, 2009
3rd-party Updated the README in the 3rd-party folder. Jul 6, 2018
benchmarks Added proper labels to the benchmarks. Aug 15, 2018
build Replaced closed data expressions in an lps by variables to avoid that… Sep 30, 2018
doc Updated the documentation of the enumerator. Nov 6, 2018
examples Changed the run.py script for open-field-tictactoe. Aug 20, 2018
libraries Fixed typo in min rank attractor computation. Nov 14, 2018
tests Added the "fatal attractors" optimization to pbessolve. Nov 14, 2018
tools Added the "fatal attractors" optimization to pbessolve. Nov 14, 2018
.clang-format ltsgraph: use arcball, add exit button May 4, 2017
.clang-tidy ltsgraph: use arcball, add exit button May 4, 2017
.gitignore Added a git ignore file for intermediate files generated Jun 4, 2018
CHANGES Added a changelog for the 201808.0 release Aug 27, 2018
CMakeLists.txt The atermpp micro-benchmarks are now build by the prepare_benchmarks … Aug 14, 2018
COPYING Moved the README file to Markdown, added some more basic info Jul 23, 2018
CTestConfig.cmake -Update CTestConfig file. Results are now uploaded to our virtual mac… Apr 27, 2010
CTestCustom.cmake.in * Increased # of warnings to 2000 Dec 8, 2010
LICENSE_1_0.txt Changes: Jan 15, 2008
README Restored the README file. Aug 27, 2018
README.md Removed CWI from front page and README Aug 3, 2018
astylerc fix astylerc Apr 13, 2017
cppcheck_ignore.lst Merge all revisions up to r11353 from trunk. Nov 13, 2012
eclipse_coding_standard.xml - Add extension to eclipse coding standard Jul 1, 2010

README.md

mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols. It can be run on Windows, Linux and macOS.

The toolset supports a collection of tools for linearisation, simulation, state-space exploration and generation and tools to optimise and analyse specifications. Moreover, state spaces can be manipulated, visualised and analysed.

The mCRL2 toolset is developed at the department of Mathematics and Computer Science of the Technische Universiteit Eindhoven, in collaboration with the University of Twente.

See our website for extensive documentation on the usage of the toolset and downloads of the release and nightly versions.

Build instructions

mCRL2 has the following dependencies:

  • Qt (5.5.0 or higher, only for the GUI tools)
  • Boost (1.48 or higher)

Furthermore, sphinx and xsltproc are required to build the documentation. Makefiles can be generated using cmake. To build the toolset in Release mode using 4 threads, run the following commands (preferably in an empty directory):

git clone https://github.com/mCRL2org/mCRL2 src
mkdir build && cd build
cmake -DCMAKE_BUILD_TYPE=Release ../src
make -j4

When compilation is finished, the binaries can be found in stage/bin/. Convenient front-ends for cmake are ccmake (macOS/Linux) and cmake-gui. Under Windows and macOS, it is usually necessary to set the variables Boost_INCLUDE_DIR and Qt5_DIR manually. More build instructions can be found in the documentation.

Contributing

Report bugs in the issue tracker. Please include the version number from mcrl22lps --version, and a complete, self-contained test case in each bug report.

Contributions in the form of a pull request are welcome. For more details, see the documentation.

If you have questions about using the mCRL2 toolset which the documentation does not answer, send a mail to mcrl2-users@listserver.tue.nl or open an issue.

License

Copyright (C) 2005-2018 Eindhoven University of Technology
mCRL2 is licensed under the Boost license. See the file COPYING for detailed license information.