.TH ktzio n "Version 4.0.0" "Tina Tools"

.SH NAME
ktzio  \- conversion tool for transition systems

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

.SH SYNOPSIS

.B ktzio
[\-\f2h\f1elp]

.B ktzio
[\-sp n] [\-tp n] [\-wp n] [\-g] [\-tina] [\-flat]
      [\-kts | \-lts | \-ks | \-rsf | \-rsd | \-rs] \-i infile

.B ktzio
[\-KTZ | \-BCG | \-AUT]
      [\-\f2k\f1tz | \-bcg |\-\f2a\f1ut | \-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]

.SH DESCRIPTION

ktzio converts kripke transition systems between several formats. 

The formats manipulated are the following:

.nf
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
.fi


The conversions currently supported are the following:

.nf
from		to
------------------------------------------------------
ktz		ktz, aut, mec, cwb, bcg, ktj, textual
bcg		ktz, textual
aut		ktz, textual
.fi

.SH OPTIONS

.TP
\-\f2h\f1elp
Recalls options.

.TP
.B Interactive mode:

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

.TP
.B Input format flags:

.TP
\-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.

.TP
.B Output format flags:

.TP
\-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 written  on standard
output,   or   in  a   file   that   does   not  bear   the   expected
extension.
Flag -txt (default) produces a textual description.

.TP
.B For \&.ktz to \&.aut/\&.mec/\&.bcg conversions (see also the tina man page):

.TP
\-sp n
Encoding  of  state  properties  in  output  transition  system  (when
information is present in the input system).
.nf
-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
.fi

.TP
\-tp n
Encoding of  transition properties  in output transition  system (when
information is present in the input system):
.nf
-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
.fi

.TP
\-wp n
Encoding of wait properties in output transition  system (when
information is present in the input system):
.nf
-wp 0 : no wait properties (default for \&.aut, \&.bcg, \&.mec)
-wp 1 : preserve wait properties (default for \&.ktz)
.fi

.TP
\-g
Removes liveness information (scc properties) from \&.aut or \&.bcg input, if present.

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


.TP
.B For conversions to \&.ktz:

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

.PP
From \&.aut or \&.bcg input:

.TP
\-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,
restores the state properties encoded into the file \&.aut as structured labels.
If the input file was not generated by tina, then the behavior is undefined.

.PP
From \&.ktz input:

.TP
\-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.

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

.TP
\-kts
Kripke Transition  System (default).

.TP
\-lts
Labelled Transition System.

.TP
\-ks
Kripke Structure.

.TP
\-rsf
Reachability Set + Firable transitions.

.TP
\-rsd
Reachability Set + Deadlocks.

.TP
\-rs 
Reachability Set.

.PP
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 profile 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.

.TP
.B Input source:

.TP
infile
Where the  kts is  read. The  input format is  determined 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.

.TP
.B Output destination:

.TP
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 extension.

.TP
.B Errors destination:

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


.SH EXAMPLES

.nf
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
.fi

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

.SH SEE ALSO

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), reduce(n), formats(n), stan(n)

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

