mCRL2 library documentation

Atermpp

• Introduction to the atermpp library
• What is an aterm?
• Programming with aterms

PDF documentation

• mCRL2 Term Library

BES

PDF documentation

• Some notes on a BES library

Core

• Introduction
• Concepts
• Structure
• Tutorial
• Common functionality

PDF documentation

• mCRL2 syntax definition

Data

• Introduction
• Data specifications
• Expressions
• Sort aliases and sort normalisation
• Data rewriters
• Data enumerator

PDF documentation

• An algorithm to find a representant for sorts in the context of sort aliases and recursive sorts

• Rewriter Implementation Notes

• Enumerator

• substitutions.tex

• Data types for mCRL2

• Some basic notions concerning the mCRL2 data library

GUI

• The GUI library

PDF documentation

• Architecture of mcrl2ide

LPS

• Linear process specifications
• Classes in the LPS library

PDF documentation

• State Space Exploration

• lpsparelm

• mcrl2lps.tex

• Next-state computation templates in state space exploration

• lps-implementation-notes.tex

• lps-implementation-communication-operator.tex

• A rewriting-strategies-based tool for transforming process-algebraic equations

• lpsconstelm

• Confluence Detection

LTS

• Introduction
• Structure
• Creating and accessing an LTS
• The standard labelled transition systems
• Reducing and comparing labelled transition systems
• Some utility functions
• Traces

PDF documentation

• Implementation of LTSGraph3D

• Notes on the bisimulation partitioner

Modal formula

• Modal formulas

PBES

• Parameterised Boolean Equation Systems
• Algorithms

PDF documentation

• Symbolic Reachability using LDDs

• PBES Generation

• PBES Implementation Notes

• PBES Instantiation and Solving

• PBES rewriters

• kant-pbes-greybox-notes.tex

• PBES Abstraction

Process

• Introduction

PDF documentation

• On free variables in process specifications, LPSs and PBESs

• Process Library Implementation Notes

SMT

• SMT Interface library

Utilities

• Introduction
• Structure
• CLI Library
• Tool classes
• Logging Library

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/generate_classes.py Generates classes that derive from atermpp::aterm_appl. The class specifications that are used as input are located in build/code_generation/mcrl2_classes.py.

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

• build/code_generation/generate_template_overloads.py 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/generate_term_functions.py 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/generate_traverser_functions.py Generates functions that are implemented using the traverser framework (find/replace/rewrite etc).

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

Note

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