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

• besinfo
• bespp
• bessolve
• diagraphica
• lps2lts
• lps2pbes
• lpsactionrename
• lpsbinary
• lpsbisim2pbes
• lpsconfcheck
• lpsconstelm
• lpsfununfold
• lpsinfo
• lpsinvelm
• lpsparelm
• lpsparunfold
• lpspp
• lpsreach
• lpsrewr
• lpssim
• lpsstategraph
• lpssumelm
• lpssuminst
• lpsuntime
• lpsxsim
• lts2lps
• lts2pbes
• ltscompare
• ltsconvert
• ltsgraph
• ltsinfo
• ltspbisim
• ltspcompare
• ltsview
• mcrl2-gui
• mcrl22lps
• mcrl2i
• mcrl2ide
• mcrl2xi
• pbes2bes
• pbes2bool
• pbes2booldeprecated
• pbesconstelm
• pbesinfo
• pbesinst
• pbesparelm
• pbespgsolve
• pbespp
• pbesrewr
• pbessolve
• pbessolvesymbolic
• pbesstategraph
• tracepp
• txt2bes
• txt2lps
• txt2pbes

List of the experimental tools

• besconvert
• lps2pres
• lps2torx
• lpscleave
• lpscombine
• lpsrealelm
• lpssymbolicbisim
• lts2pres
• ltscombine
• pbes2cvc4
• pbes2yices
• pbesabsinthe
• pbesabstract
• pbespareqelm
• pbespor
• pbessymbolicbisim
• presconstelm
• presinfo
• presinst
• presparelm
• prespp
• presrewr
• pressolve
• resinfo
• respp
• symbolic_exploration
• txt2pres
• txt2res

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)

• Formats for Labelled Transition Systems

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.