
NAME
     ktzio  - conversion tool for transition systems

     Part of Tina Toolbox for analysis of  Petri  nets  and  Time
     Petri nets (see also nd, tina, plan, struct, ndrio, selt).

SYNOPSIS
     ktzio [-help] [-i file]
     ktzio [-help] [-KTZ | -BCG | -AUT]
           [-ktz | -bcg |-aut | -mec | -l | -v | -q]
           [-sp n] [-tp n] [-wp n] [-g] [-tina] [-bf | -df]
           [infile] [outfile]

DESCRIPTION
     ktzio converts kripke  transition  systems  between  several
     formats.

     The formats manipulated are the following:

     name      file ext  description
     ------------------------------------------------------
     ktz       .ktz      tina compact binary format
     bcg       .bcg      CADP compact binary format
     aut       .aut      CADP aldebaran format
     mec       .mec      Mec4 model checker format
     textual   .txt      textual descriptions, explained below

     The conversions currently supported are the following:

     from      to
     ------------------------------------------------------
     ktz       ktz, aut, mec, bcg, textual
     bcg       ktz, textual
     aut       ktz, textual


OPTIONS
     -help Recalls options.

     Interactive mode:

     -i infile
          Reads  a  kts  from  infile  and  prints  its  contents
          interactively, as a list of state descriptions.

     Input format flags:

     -KTZ | -BCG | -AUT
          Specifies  the format  of the  input  transition   sys-
          tem.  This  flag is necessary when the input transition
          system is read on standard input, or read from  a  file
          that  does  not bear the expected extension. Default is
          -KTZ.

     Output format flags:

     -ktz | -bcg | -aut | -mec | -l | -v | -q
          Specifies the  format of  the output  transition   sys-
          tem.  This  flag is necessary  when the output  transi-
          tion system  is written  on standard output,   or    in
          a    file    that    does    not  bear   the   expected
          extension.  Flags -l, -v, -q produce  textual  descrip-
          tions, as follows. Default is -l.

          -l        ktzio -i style output (default)
          -v        tina -v style output (only from ktz)
          -q        tina -q style output (only from ktz)

     Transition system generation options (see the tina page):

     -sp n:
          For ktz to ktz/aut/mec/bcg conversions.   Encoding   of
          state    properties   in   output   transition   system
          (when information is present in the input system).
          -sp 0 : no state properties (default for .aut, .bcg)
          -sp 1 : boolean state properties (default for .mec)
          -sp 2 : weighted state properties (default for .ktz)
          -sp 3 : weighted state properties for all weights

     -tp n:
          For ktz to ktz/aut/mec/bcg  conversions.   Encoding  of
          transition  properties   in  output  transition  system
          (when information is present in the input system):
          -tp 0 : no transition properties
          -tp 1 : boolean transition properties (default for all formats)
          -tp 2 : weighted transition properties (default for .ktz)
          -tp 3 : weighted transition properties for all weights

     -wp n:
          For ktz to ktz/aut/mec/bcg  conversions.   Encoding  of
          wait  properties  in  output  transition   system (when
          information is present in the input system):
          -wp 0 : no wait properties (default for .aut, .bcg, .mec)
          -wp 1 : preserve wait properties (default for .ktz)

     -g   For ktz to ktz conversions. Removes  liveness  informa-
          tion if present.

     -tina
          For .aut or .bcg  input.  Decodes  properties  assuming
          they  were  encoded  by tina. E.g. if the .aut file was
          generated by tina with flag -sp 2, restores  the  state
          properties  encoded  in the file. If the input file was
          not generated by tina, then the behavior is undefined.

     -df | -bf
          Tune up flag for bcg to  ktz  conversions.  Default  is
          -df.

     Input source:

     infile
          Where the  kts is  read. The  input format  is   deter-
          mined  by  the file type, according to the table above.
          If absent or specified by "-",  the  kts  is   read  on
          standard   input in the  format specified by  the input
          flag. If  both an  infile and   some  input  flag   are
          present,   then  the format defined  by the  input flag
          supersedes  that determined  by the infile extension.

     Output destination:

     outfile
          Where results are written. The output format is  deter-
          mined by the file type, according  to the  table above.
          If  absent or specified  by "-", then results are writ-
          ten  on  standard output in the format specified by the
          output flag. If both an  outfile and some  output  flag
          are  present,  then  the  format defined by  the output
          flag supersedes that determined by the  outfile  exten-
          sion.


FILES
     Files  aut.txt,  bcg.txt,  mec.txt,   ktz.txt  in  directory
     doc/formats specify the syntax of .aut, .bcg,  .mec and .ktz
     transition system description files, respectively.


EXAMPLES
     ktzio -i abp.ktz
     ktzio -v abp.ktz
     ktzio abp.ktz abp.aut
     ktzio -AUT - abp.ktz < abp.aut
     ktzio -AUT -ktz < abp.aut > abp.ktz
     ktzio abp.bcg -ktz | ktzio -KTZ - abp.aut

     Note: not all targets support  binary data on standard input
     or output.


SEE ALSO
     nd, tina, plan, struct, ndrio, selt


AUTHORS
     Bernard       Berthomieu,       LAAS/CNRS,        2000-2005,
     Bernard.Berthomieu@laas.fr.


