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,
         '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  '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 © 2012 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>.

ltsconvert mCRL2 toolset 201210.1 (Release)       November 2012                                    LTSCONVERT(1)