NAME
lps2lts - generate an LTS from an LPS
SYNOPSIS
lps2lts [OPTION]... [INFILE [OUTFILE]]
DESCRIPTION
Generate an LTS from the LPS in INFILE and save the result to OUTFILE.
If INFILE is not supplied, stdin is used. If OUTFILE is not supplied,
the LTS is not stored.
The format of OUTFILE is determined by its extension (unless it is
specified by an option). The supported formats are:
’aut’ for the Aldebaran format (CADP),
’dot’ for the GraphViz format,
’fsm’ for the Finite State Machine format,
’mcrl’ for the mCRL SVC format,
’mcrl2’ for the mCRL2 LTS format, or
’svc’ for the (generic) SVC format
OPTIONS
OPTION can be any of the following:
-aNAMES, --action=NAMES
detect actions from NAMES, a comma-separated list of action
names; a message is printed for every occurrence of one of these
action names
-b[NUM], --bit-hash[=NUM]
use bit hashing to store states and store at most NUM states;
note that this option may cause states to be mistaken for others
(default value for NUM is approximately 2*10^8)
-c[NAME], --confluence[=NAME]
apply on-the-fly confluence reduction with NAME the confluent
tau action (when no NAME is supplied, ’ctau’ is used)
-D, --deadlock
detect deadlocks (i.e. for every deadlock a message is printed)
-F, --divergence
detect divergences (i.e. for every state with a divergence (=tau
loop) a message is printed).
-yBOOL, --dummy=BOOL
replace free variables in the LPS with dummy values based on the
value of BOOL: ’yes’ (default) or ’no’
--error-trace
if an error occurs during exploration, save a trace to the state
that could not be explored
--init-tsize=NUM
set the initial size of the internally used hash tables (default
is 10000)
-lNUM, --max=NUM
explore at most NUM states
--no-info
do not add state information to OUTFILE
-oFORMAT, --out=FORMAT
save the output in the specified FORMAT
-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
-fNAME, --state-format=NAME
store state internally in format NAME:
’vector’ for a vector (fastest, default), or
’tree’ for a tree (for memory efficiency)
-sNAME, --strategy=NAME
explore the state space using strategy NAME:
’b’, ’breadth’ breadth-first search (default)
’d’, ’depth’ depth-first search
’p’, ’prioritized’ prioritize single actions on its first
argument being of
sort Nat where only those actions with the lowest value for
this parameter
are selected. E.g. if there are actions a(3) and b(4), a(3)
remains and b(4)
is skipped. Actions without a first parameter of sort Nat and
multactions
with more than one action are always chosen (option is
experimental).
’q’, ’rprioritized’ prioritize actions on its first argument
being of sort
Nat (see option --prioritized), and randomly select one of
these to obtain a
prioritized random simulation (option is experimental).
’r’, ’random’ random simulation
--suppress
in verbose mode, do not print progress messages indicating the
number of visited states and transitions
--todo-max=NUM
keep at most NUM states in todo lists; this option is only
relevant for breadth-first search with bithashing, where NUM is
the maximum number of states per level, and for depth first,
where NUM is the maximum depth
-t[NUM], --trace[=NUM]
write at most NUM traces to states detected with the --deadlock,
--divergence or --action options (default is unlimited)
-u, --unused-data
do not remove unused parts of the data 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 Muck van Weerdenburg.
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/lps2lts>.
lps2lts mCRL2 toolset July 2010 (deMayo2010t)