ktzio(n)                                                              ktzio(n)



NAME
       ktzio  - conversion tool for transition systems

       Part of Tina Toolbox for analysis of Petri nets and Time Petri nets.


SYNOPSIS
       ktzio [-help] [-sp n] [-tp n] [-wp n] [-g] [-tina | -fw] -i file]

       ktzio [-help] [-KTZ | -BCG | -AUT]
             [-ktz | -bcg |-aut | -mec | -cwb | -txt]
             [-sp n] [-tp n] [-wp n] [-g] [-tina | -fw] [-bf | -df]
             [infile] [outfile] [errorfile]


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
       cwb       .cwb      Concurrency Workbench agent format
       textual   .txt      textual descriptions, explained below

       The conversions currently supported are the following:

       from      to
       ------------------------------------------------------
       ktz       ktz, aut, mec, cwb, 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   system.  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 | -cwb | -txt
              Specifies  the   format  of  the output transition  system. This
              flag is necessary  when the output  transition system  is  writ-
              ten  on standard output,   or   in  a   file   that   does   not
              bear   the   expected extension.  Flag -txt (default) produces a
              textual description.


       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 prop-
              erties 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 information 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.


       -fw    This flag is necessary to  convert  older  ktz  files  capturing
              unbounded property values (such as those resulting from tina -C)
              into crrent ktz.  If omitted  and  the  file  actually  contains
              unbounded values, then the conversion will fail.


       -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  determined by
              the file type, according to the table above. If absent or speci-
              fied  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  determined  by
              the  file  type,  according   to the  table above. If  absent or
              specified  by "-", then results are written 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.


       Errors destination:


       errorfile
              Where error messages are written. By default, errors are printed
              on standard error.



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(n),   tina(n),   sift(n),  rsdd(n),  plan(n),  struct(n),  ndrio(n),
       selt(n), muse(n), pathto(n), play(n)


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




Tina Tools                       Version 3.0.0                        ktzio(n)
