Man Linux: Main Page and Category List


       lps2lts - generate an LTS from an LPS


       lps2lts [OPTION]... [INFILE [OUTFILE]]


       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


       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’

              if an error occurs during exploration, save a trace to the state
              that could not be explored

              set the initial size of the internally used hash tables (default
              is 10000)

       -lNUM, --max=NUM
              explore at most NUM states

              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
                with  more  than  one  action  are  always  chosen  (option is
                ’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

              in verbose mode, do not print progress messages  indicating  the
              number of visited states and transitions

              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

              display version information


       Written by Muck van Weerdenburg.


       Report bugs at <>.


       Copyright © 2010 Technische Universiteit Eindhoven.
       This  is  free  software.   You may redistribute copies of it under the
       terms        of        the        Boost        Software         License
       <>.   There  is NO WARRANTY, to the
       extent permitted by law.


       See             also             the             manual              at

lps2lts mCRL2 toolset July 2010 (deMayo2010t)