mCRL2 library documentation


PDF documentation


PDF documentation


PDF documentation


PDF documentation


PDF documentation


PDF documentation


PDF documentation


PDF documentation


PDF documentation



Source code reference

We generate the complete source code reference using Doxygen, which can be viewed here

Code generation

A substantial part of the mCRL2 code is generated using scripts. This section gives an overview of the scripts and their purpose.

  • build/code_generation/ Generates classes that derive from atermpp::aterm_appl. The class specifications that are used as input are located in build/code_generation/

  • build/code_generation/ Generates code for standard data types like bag, bool, int, etc.

  • build/code_generation/ Generates overloads for several template functions (pp, find, normalize_sorts, etc.). These overloads are added to header files to avoid the inclusion of heavy templated header files that are expensive to compile. The implementations of the functions are added to files in the source directory, while the declarations need to be added manually (since it is not always known where to put them).

  • build/code_generation/ Generates low level code for creating terms (soundness checks, constructors). The script requires command line arguments (see the help function for details). The description of the internal format in the file doc/specs/mcrl2.internal.txt is used as input for the script.

  • build/code_generation/ Generates functions that are implemented using the traverser framework (find/replace/rewrite etc).

  • build/code_generation/ Generates the contents of traverser.h and builder.h files. The class specifications that are used as input are located in build/code_generation/


Most of the scripts print a report of the files that have been updated, and the files that have stayed the same.