Section: User Commands (1)Updated: October 2010Local indexUp
NAME
mcrl22lps - translate an mCRL2 specification to an LPS
SYNOPSIS
mcrl22lps
[OPTION]... [INFILE [OUTFILE]]
DESCRIPTION
Linearises the mCRL2 specification in INFILE and writes the resulting LPS to
OUTFILE. If OUTFILE is not present, stdout is used. If INFILE is not present,
stdin is used.
OPTIONS
OPTION can be any of the following:
-b, --binary
when clustering use binary case functions instead of n-ary; in the presence of
-w/--newstate, state variables are encoded by a vector of boolean variables
-e, --check-only
check syntax and static semantics; do not linearise
-c, --cluster
all actions in the final LPS are clustered
-D, --delta
add a true->delta summands to each state in each process; these delta's subsume
all other conditional timed delta's, effectively reducing the number of delta
summands drastically in the resulting linear process; speeds up linearisation
-lNAME, --lin-method=NAME
use linearisation method NAME:
'regular' for generating an LPS in regular form
(specification should be regular, default),
'regular2' for a variant of 'regular' that uses more data variables
(useful when 'regular' does not work), or
'stack' for using stack data types
(useful when 'regular' and 'regular2' do not work)
--mcrl2-gui
outputs information about the visual representation of this option in the mCRL2
GUI
-w, --newstate
state variables are encoded using enumerated types (requires linearisation
method 'regular' or 'regular2'); without this option numbers are used
-z, --no-alpha
alphabet reductions are not applied
-n, --no-cluster
the actions in intermediate LPSs are not clustered (default behaviour is that
intermediate LPSs are clustered and the final LPS is not clustered)
-g, --no-deltaelm
avoid removing spurious delta summands
-f, --no-globvars
instantiate don't care values with arbitrary constants, instead of modelling
them by global variables. This has no effecton global variable that are
declared in the specification.
-o, --no-rewrite
do not rewrite data terms while linearising; useful when the rewrite system
does not terminate
-m, --no-sumelm
avoid applying sum elimination in parallel composition
-rNAME, --rewriter=NAME
use rewrite strategy NAME:
'jitty' for jitty rewriting (default),
'jittyp' for jitty rewriting with prover,
'jittyc' for compiled jitty rewriting,
'inner' for innermost rewriting,
'innerp' for innermost rewriting with prover, or
'innerc' for compiled innermost rewriting
-a, --statenames
the names of state variables are derived from the specification