NAME

       ltsconvert - convert and optionally minimise an LTS

SYNOPSIS

       ltsconvert [OPTION]... [INFILE [OUTFILE]]

DESCRIPTION

       Convert  the  labelled  transition  system  (LTS)  from INFILE to OUTFILE in the requested
       format after applying the selected minimisation method (default is none).  If  OUTFILE  is
       not supplied, stdout is used. If INFILE is not supplied, stdin is used.

       The  output  format is determined by the extension of OUTFILE, whereas the input format is
       determined by the content of INFILE. Options --in and --out can be used to force the input
       and output formats. 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 (default)

OPTIONS

       OPTION can be any of the following:

       -D, --determinise
              determinise LTS

       -eNAME, --equivalence=NAME
              generate   an   equivalent   LTS,  preserving  equivalence  NAME:  'none'  identity
              equivalence (default) 'bisim' strong bisimilarity 'bisim-sig'  strong  bisimilarity
              using  signature  refinement  'branching-bisim'  branching bisimilarity 'branching-
              bisim-sig' branching bisimilarity using  signature  refinement  'dpbranching-bisim'
              divergence  preserving  branching  bisimilarity  'dpbranching-bisim-sig' divergence
              preserving branching bisimilarity  using  signature  refinement  'weak-bisim'  weak
              bisimilarity 'weak-bisim-sig' weak bisimilarity using signature refinement 'dpweak-
              bisim'  divergence  preserving  weak  bisimilarity  'dpweak-bisim-sig'   divergence
              preserving  weak  bisimilarity  using  signature refinement 'sim' strong simulation
              equivalence 'trace' strong trace equivalence 'weak-trace'  weak  trace  equivalence
              'tau-star' tau star reduction

       -iFORMAT, --in=FORMAT
              use FORMAT as the input format

       -lFILE, --lps=FILE
              use FILE as the LPS from which the input LTS was generated; this might be needed to
              store the correct parameter names of states  when  saving  in  fsm  format  and  to
              convert non-mCRL2 LTSs to a mCRL2 LTS

       --no-reach
              do not perform a reachability check on the input LTS

       -n, --no-state
              leave out state information when saving in dot format

       -oFORMAT, --out=FORMAT
              use FORMAT as the output format

       --tau=ACTNAMES
              consider  actions  with  a name in the comma separated list ACTNAMES to be internal
              (tau) actions in addition to those defined as such by the input

       --timings[=FILE]
              append timing measurements to FILE. Measurements are written to standard  error  if
              no FILE is provided

       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, Jan Friso Groote.

REPORTING BUGS

       Report bugs at <http://www.mcrl2.org/issuetracker>.

COPYRIGHT

       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/ltsconvert.html>.