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)
-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
Standard options:
-q, --quiet
do not display warning messages
-v, --verbose
display short intermediate messages
-d, --debug
display detailed intermediate messages
-h, --help
display help information
--version
display version information
AUTHOR
Written by Jan Friso Groote.
REPORTING BUGS
Report bugs at <http://www.mcrl2.org/issuetracker>.
COPYRIGHT
Copyright © 2010 Technische Universiteit Eindhoven.
This is free software. You may redistribute copies of it under the
terms of the Boost Software License
<http://www.boost.org/LICENSE_1_0.txt>. There is NO WARRANTY, to the
extent permitted by law.
SEE ALSO
See also the manual at
<http://www.mcrl2.org/mcrl2/wiki/index.php/User_manual/mcrl22lps>.
mcrl22lps mCRL2 toolset July 2010 (Maye2010ent)