Man Linux: Main Page and Category List


       ltsconvert - convert and optionally minimise an LTS


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


       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,
         ’mcrl’ for the mCRL SVC format,
         ’mcrl2’ for the mCRL2 LTS format (default), or
         ’svc’ for the (generic) SVC format


       OPTION can be any of the following:

       -a, --add
              do  not  minimise  but  save a copy of the original LTS extended
              with a state parameter indicating the bisimulation class a state
              belongs to (only for mCRL2)

       -D, --determinise
              determinise LTS

       -eNAME, --equivalence=NAME
              generate an equivalent LTS, preserving equivalence NAME:
                ’bisim’ for strong bisimilarity,
                ’branching-bisim’ for branching bisimilarity,
                ’dpbranching-bisim’   for   divergence   preserving  branching
                ’sim’ for strong simulation equivalence,
                ’trace’ for strong trace equivalence, or
                ’weak-trace’ for weak trace equivalence

       -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
              mightbe  needed  to  store the correct parameter names of states
              when saving in fsm format and to convert  non-mCRL2  LTSs  to  a
              mCRL2 LTS

              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

              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

       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

ltsconvert mCRL2 toolset July 2010 Mayv2010ment)