lps2lts

Langue: en

Version: May 2010 (ubuntu - 24/10/10)

Section: 1 (Commandes utilisateur)

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 © 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>.