xenial (1) lps2lts.1.gz

Provided by: mcrl2_201409.0-1ubuntu1_amd64 bug

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.

       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 (no longer supported as input format),
         'fsm' for the Finite State Machine format, or
         'lts'  for  the  mCRL2  LTS  format  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 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)

       --cached
              use enumeration caching techniques to speed up state space generation.

       -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 divergences is linear for every state, so state space exploration becomes
              quadratic with this option on, causing a state space exploration 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

       -mNAMES, --multiaction=NAMES
              detect and report multiactions in the transitions system from NAMES, a comma-separated list. Works
              like -a, except that multi-actions are matched exactly, including data parameters.

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

       --prune
              use summand pruning to speed up state space generation.

       -QNUM, --qlimit=NUM
              limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for unlimited).

       -rNAME, --rewriter=NAME
              use  rewrite  strategy  NAME:  'jitty' jitty rewriting (default) 'jittyc' compiled jitty rewriting
              'jittyp' jitty rewriting with prover

       -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
              transitions. For 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,
              where NUM is the maximum number of states per level, and for depth first search, 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 © 2014 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/release/user_manual/tools/lps2lts.html>.