LPS2LTS(1) User Commands LPS2LTS(1)
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 sup-
plied, the LTS is not stored.
If the 'jittyc' rewriter is used, then the MCRL2_COMPILEREWRITER environment variable (default value: 'mcrl2compilerewriter') determines
the script that compiles the rewriter, and MCRL2_COMPILEDIR (default value: '.') determines where temporary files are stored.
Note that lps2lts can deliver multiple transitions with the same label betweenany pair of states. If this is not desired, such transitions
can be removed byapplying a strong bisimulation reducton using for instance the tool ltsconvert.
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,
'lts' for the mCRL2 LTS format, or
'svc' for the SVC format If the jittyc rewriter is used, then the MCRL2_COMPILEREWRITER environment variable (default value: mcrl2compil-
erewriter) determines the script that compiles the rewriter, and MCRL2_COMPILEDIR (default value: '.') determines where temporary files are
stored. Note that lps2lts can deliver multiple transitions with the same label between any pair of states. If this is not desired, such
transitions can be removed by applying a strong bisimulation reducton using for instance the tool ltsconvert.
OPTIONS
OPTION can be any of the following:
-aNAMES, --action=NAMES
detect and report actions in the transitions system that have action names from NAMES, a comma-separated list. This is for instance
useful to find (or prove the absence) of an action error. A message is printed for every occurrence of one of these action names.
With the -t flag traces towards these actions are generated
-b[NUM], --bit-hash[=NUM]
use bit hashing to store states and store at most NUM states. This means that instead of keeping a full record of all states that
have been visited, a bit array is used that indicate whether or not a hash of a state has been seen before. Although this means that
this option may cause states to be mistaken for others (because they are mapped to the same hash), it can be useful to explore very
large LTSs that are otherwise not explorable. The default value for NUM is approximately 2*10^8 (this corresponds to about 25MB of
memory)
-c[NAME], --confluence[=NAME]
apply prioritization of transitions with the action label NAME.(when no NAME is supplied (i.e., '-c') priority is given to the
action 'ctau'. To give priority to to tau use the flag -ctau. Note that if the linear process is not tau-confluent, the generated
state space is necessarily branching bisimilar to the state space of the lps. The generation algorithm that is used does not require
the linear process to be tau convergent.
-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). The algorithm to detect the diver-
gences is linear for every state, so state space exploration becomes quadratic with this option on, causing a state space explo-
ration to become slow when this option is enabled.
-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 OUTFILEWithout this option lps2lts adds state vector to the LTS. This option causes this information
to be discarded and states are only indicated by a sequence number. Explicit state information is useful for visualisation purposes,
for instance, but can cause the OUTFILE to grow considerably. Note that this option is implicit when writing in the AUT format.
-oFORMAT, --out=FORMAT
save the output in the specified FORMAT
-rNAME, --rewriter=NAME
use rewrite strategy NAME:
'jitty' for jitty rewriting (default),
'jittyc' for compiled jitty rewriting,
'jittyp' for jitty rewriting with prover
-fNAME, --state-format=NAME
store state internally in format NAME:
'tree' for a tree (memory efficient, default), or
'vector' for a vector (slightly faster, often far less memory efficient)
-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. Out of all next states one is chosen at
random independently of whether this state has already been observed.
Consequently, random simultation only terminates when a deadlocked state is
encountered.
--suppress
in verbose mode, do not print progress messages indicating the number of visited states and transitionsFor large state spaces the
number of progress messages can be quite horrendous. This feature helps to suppress those. Other verbose messages, such as the total
number of states explored, just remain visible.
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
--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 maxi-
mum number of states per level, and for depth first, where NUM is the maximum depth
-t[NUM], --trace[=NUM]
Write a shortest trace to each state that is reached with an action from NAMES from option --action, is a deadlock detected with
--deadlock, or is a divergence detected with --divergence to a file. No more than NUM traces will be written. If NUM is not supplied
the number of traces is unbounded.For each trace that is to be written a unique file with extension .trc (trace) will be created
containing a shortest trace from the initial state to the deadlock state. The traces can be pretty printed and converted to other
formats using tracepp.
-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
--log-level=LEVEL
display intermediate messages up to and including level
-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 (C) 2012 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 201202.0 (Release) April 2012 LPS2LTS(1)