User manual/Tool manual pages

From MCRL2

User manual

Introduction Installation instructions Toolset overview Tool manual pages chi2mcrl2 diagraphica formcheck grapemcrl2 lps2lts lps2pbes lps2torx lpsactionrename lpsbinary lpsbisim2pbes lpsconfcheck lpsconstelm lpsinfo lpsinvelm lpsparelm lpsparunfold lpspp lpsrealelm lpsrewr lpssim lpssumelm lpssuminst lpsuntime lpsxsim lts2lps ltscompare ltsconvert ltsgraph ltsinfo ltsmin ltsview lysa2mcrl2 mcrl22lps mcrl2-gui mcrl2i pbesinst pbes2bool pbesconstelm pbesinfo pbesparelm pbespareqelm pbespgsolve pbespp pbesrewr pnml2mcrl2 squadt tbf2lps tracepp txt2lps txt2pbes FAQ

Contents

Release tools

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.

Experimental tools

besconvert	Simplify a BES using equivalences.
bessolve	Solve a BES.
lpsbisim2pbes	Compute a bisimulation relation between two LPSs.
lpsrealelm	Remove Real numbers from an LPS.
lts2pbes	Generate a PBES from an LTS and a state formula.
pbesabsinthe	A form of abstract interpretation for PBESs.
pbesabstract	A form of abstract interpretation for PBESs.
pbesinst	Compute a (P)BES out of a PBES.
pbespareqelm	Compute equivalence relations on parameters of a PBES.
txt2bes	Parse a textual description of a BES.

Deprecated tools

squadt	Interactive integration of software tools, including the tools mentioned above.
ltsmin	Minimise an LTS.

---

Toolset overview

chi2mcrl2