4mktzio24m(n)                                                              4mktzio24m(n)

1mNAME0m
       ktzio  - conversion tool for transition systems

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


1mSYNOPSIS0m
       1mktzio 22m[-4mh24melp]

       1mktzio 22m[-sp n] [-tp n] [-wp n] [-g] [-tina] [-flat]
             [-kts | -lts | -ks | -rsf | -rsd | -rs] -i infile

       1mktzio 22m[-KTZ | -BCG | -AUT]
             [-4mk24mtz | -bcg |-4ma24mut | -mec | -cwb | -ktj | -txt]
             [-kts | -lts | -ks | -rsf | -rsd | -rs]
             [-sp n] [-tp n] [-wp n] [-g] [-tina] [-flat]
             [-fw] [-raw | -bf | -df]
             [infile] [outfile] [errorfile]


1mDESCRIPTION0m
       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
       json      .ktj           Json format
       textual   .txt           textual descriptions, explained below


       The conversions currently supported are the following:

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


1mOPTIONS0m
       -4mh24melp  Recalls options.


       1mInteractive mode:0m


       -i infile
              Reads  a  kts from infile and prints its contents interactively,
              as a list of state descriptions. Type ? at the prompt for avail-
              able commands.


       1mInput format flags:0m


       -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  ex-
              pected extension. Default is -KTZ.


       1mOutput format flags:0m


       -ktz | -bcg | -aut | -mec | -cwb | -ktj | -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.


       1mFor .ktz to .aut/.mec/.bcg conversions (see also the tina man page):0m


       -sp n  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  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  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     Removes  liveness information (scc properties) from .aut or .bcg
              input, if present.


       -flat  If converting to .aut or .bcg, expands all structured labels  to
              produce a lts with regular (flat) labels.



       1mFor conversions to .ktz:0m


       -raw | -df | -bf
              Tune  up flag for ktz: specifies encoding of targets. Default is
              -df.


       From .aut or .bcg input:


       -tina  Decodes properties in input assuming they were encoded by  tina.
              E.g. if the .aut file was generated by tina with flag -sp 2, re-
              stores the state properties encoded into the file .aut as struc-
              tured labels.  If the input file was not generated by tina, then
              the behavior is undefined.


       From .ktz input:


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


       Additionally, as of Version  4.0.0,   the  following  options   specify
       "profiles"   for  the output.   A  profile   makes  precise  the infor-
       mation  to be preserved from the input file.   The  available  profiles
       are described in the sift man page, these are:


       -kts   Kripke Transition  System (default).


       -lts   Labelled Transition System.


       -ks    Kripke Structure.


       -rsf   Reachability Set + Firable transitions.


       -rsd   Reachability Set + Deadlocks.


       -rs    Reachability Set.


       Profile options set output options -sp, -tp and -wp, hence these should
       be  avoided  when  specifying  a profile.  When producing a  .ktz file,
       whenever there is a  sequence of output options equivalent to   a  pro-
       file  option,  the profile  option should be prefered  as  the  profile
       option  will  be  recorded  into  the  ktz file. This may be useful for
       the tools processing ktz files.


       1mInput source:0m


       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  in-
              put  flag   are present,  then the format defined  by the  input
              flag supersedes  that determined  by the infile extension.


       1mOutput destination:0m


       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.


       1mErrors destination:0m


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



1mEXAMPLES0m
       ktzio -i abp.ktz
       ktzio 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

       ktzio abp.ktz -aut -flat
       ktzio abp.ktz -kts a.aut
       ktzio a.aut -tina

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


1mSEE ALSO0m
       nd(n),   tina(n),  plan(n),  struct(n),  ktzio(n),  ndrio(n),  tedd(n),
       selt(n), sift(n), muse(n), pathto(n), scan(n),  play(n),  walk(n),  re-
       duce(n), formats(n), stan(n)


1mAUTHORS0m
       Bernard Berthomieu, LAAS/CNRS, 2000-2026, Bernard.Berthomieu@laas.fr.


Tina Tools                       Version 4.0.0                        4mktzio24m(n)
