| Integrated tool environment
|
| mcrl2-gui | A graphical front-end for mCRL2-tools.
|
| mCRL2 tools
|
| grapemcrl2 | Graphical editing environment for mCRL2 process specifications.
|
| mcrl2i | Interpreter for the mCRL2 data language.
|
| LPS tools
|
| formulacheck | Check a boolean formula.
|
| lps2lts | Generate an LTS from an LPS.
|
| lpsactionrename | Rename actions of an LPS.
|
| lpsbinary | Replace finite sort variables by vectors of boolean variables in an LPS.
|
| lpsconfcheck | Mark confluent tau-summands of an LPS.
|
| lpsconstelm | Remove constant parameters from an LPS.
|
| lpsinfo | Display basic information about an LPS.
|
| lpsinvelm | Check invariants and use these to simplify or eliminate summands of an LPS.
|
| lpsparelm | Remove unused parameters from an LPS.
|
| lpsparunfold | Unfold process parameters in an LPS.
|
| lpspp | Pretty print an LPS.
|
| lpsrewr | Rewrite data expressions in an LPS.
|
| lpssim | Command-line simulation of an LPS.
|
| lpssumelm | Remove superfluous summations from an LPS.
|
| lpssuminst | Instantiate summation variables of an LPS.
|
| lpsuntime | Remove time from an LPS.
|
| lpsxsim | Graphical simulation of an LPS.
|
| mcrl22lps | Translate an mCRL2 specification to an LPS.
|
| txt2lps | Parse a textual description of a linear process specification.
|
| PBES tools
|
| lps2pbes | Generate a PBES from an LPS and a state formula.
|
| pbes2bool | Solve a (P)BES.
|
| pbes2bes | Instantiate a PBES into a BES.
|
| pbesconstelm | Remove constant parameters from a PBES.
|
| pbesinfo | Display basic information about a PBES.
|
| pbesparelm | Remove unused parameters from a PBES.
|
| pbespgsolve | Solve a (P)BES using a parity game solver.
|
| pbespp | Pretty print a PBES.
|
| pbesrewr | Rewrite and simplify a PBES.
|
| txt2pbes | Parse a textual description of a PBES.
|
| BES tools
|
| besinfo | Provide information of a BES.
|
| bespp | Pretty print a BES.
|
| pbes2bool | Solve a (P)BES.
|
| pbespgsolve | Solve a (P)BES using a parity game solver.
|
| LTS tools
|
| diagraphica | Interactive visual analysis of an LTS.
|
| lts2lps | Convert an LTS to an LPS.
|
| ltscompare | Compare two LTSs.
|
| ltsconvert | Convert and optionally minimise an LTS.
|
| ltsgraph | Visualise an LTS as a graph and manipulate its layout.
|
| ltsinfo | Display basic information about an LTS.
|
| ltsview | 3D interactive visualisation of an LTS.
|
| tracepp | Convert and pretty print traces.
|
| Import/Export
|
| chi2mcrl2 | Convert a Chi specification to a matching mCRL2 process specification.
|
| lps2torx | Provide TorX explorer interface to an LPS.
|
| lysa2mcrl2 | Convert a Typed LySa specification to an mCRL2 process specification.
|
| pnml2mcrl2 | Convert a Petri net to an mCRL2 process specification (removed from release March 2011).
|
| tbf2lps | Convert a µCRL LPE to an mCRL2 LPS.
|
Toolset overview
