Rechercher une page de manuel
lps2lts
Langue: en
Version: May 2010 (ubuntu - 24/10/10)
Section: 1 (Commandes utilisateur)
NAME
lps2lts - generate an LTS from an LPSSYNOPSIS
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>.Contenus ©2006-2024 Benjamin Poulain
Design ©2006-2024 Maxime Vantorre