Tool documentation

Below the main tools provided in the toolset are given. The common tools are suitable for all main tasks to be carried out with the toolset. The experimental tools are tools that are under development and provide additional but still experimental functionality.

List of the common tools

List of the experimental tools

In the source distribution there are more tools such as the deprecated and developer tools.

File formats

This page lists all file formats supported by the mCRL2 toolset.

File format

Extension

Type

Description

mCRL2

.mcrl2

textual

mCRL2 specification

MCF

.mcf

textual

µ-Calculus

LPS

.lps

binary

Linear Process Specifications

PBES

.pbes

binary

Parameterised Boolean Equation Systems

BES

.bes

binary

Boolean Equation Systems

GM

.gm

textual

parity game in the PGSolver format

LTS

.lts

binary

labelled transition system in the mCRL2 LTS format

AUT

.aut

textual

labelled transition system in the The aut format

FSM

.fsm

textual

labelled transition system in the The FSM file format

trace

.trc

binary

trace for simulation

DOT

.dot

textual

DOT file format (subgraphs as nodes are not supported)

External tools

The tools given below are not part of the toolset, but are standalone tools that have mCRL2-related functionalities.

  • A tool for generating LaTeX from a mu-calculus formula in the mCRL2 syntax: GitHub, Web app.