User manual/Tool manual pages

From MCRL2

User manual

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

Contents

Release tools

Integrated tool environment
squadt	Interactive integration of software tools, including the tools mentioned below.
mCRL2 tools
grapemcl2	Graphical editing environment for mCRL2 process specifications.
grape	See grapemcrl2 for more information.
mcrl2i	Interpreter for the mCRL2 data language.
LPS tools
formulacheck	Check a boolean formula.
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	Translate a textual description of a linear process into an LPS.
PBES tools
lps2pbes	Generate a PBES from an LPS and a state formula.
pbes2bool	Determine whether a PBES is valid by translating it to a BES.
pbesconstelm	Remove constant parameters from a PBES.
pbesinfo	Display basic information about a PBES.
pbesparelm	Remove unused parameters from a PBES.
pbespp	Pretty print a PBES.
pbesrewr	Rewrite and simplify a PBES.
txt2pbes	Parse a textual description of a PBES.
LTS tools
diagraphica	Interactive visual analysis of an LTS.
lps2lts	Generate an LTS from 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.
tbf2lps	Convert a µCRL LPE to an mCRL2 LPS.

Experimental tools

lpsbisim2pbes	Compute a bisimulation relation between two LPSs.
lpsrealelm	Remove Real numbers from an LPS.
lts2lps	Converts an LTS to an LPS.
pbes2bes	Compute a BES out of a PBES.
pbespareqelm	Compute equivalence relations on parameters of a PBES.
pbespgsolve	Solve a PBES using a parity game solver.

Deprecated tools

ltsmin

Minimise an LTS.

---

Toolset overview

chi2mcrl2