#

Manual Reference Pages - ktzio (n)

### NAME

> ktzio - conversion tool for transition systems

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

### CONTENTS

> Synopsis
> Description
> Options
> Examples
> See Also
> Authors

### SYNOPSIS

> ktzio [-help]

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

> ktzio [-KTZ | -BCG | -AUT]
> [-ktz | -bcg |-aut | -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]

### 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
>     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

### OPTIONS

> -help | Recalls options.
> Interactive mode:
> -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.
> 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 | -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.
> For .ktz to .aut/.mec/.bcg conversions (see also the tina man page):
> -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.
> For conversions to .ktz:
> -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, 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.
> 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 3.8.5, 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:
> -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 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.
> 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 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 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.
> Errors destination:
> errorfile
> | Where error messages are written. By default, errors are printed on standard error.

### EXAMPLES

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

### 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)

### AUTHORS

> Bernard Berthomieu, LAAS/CNRS, 2000-2024, Bernard.Berthomieu@laas.fr.

Tina Tools | ktzio (n) | Version 3.8.5

Generated by manServer 1.07 from src/ktzio.n using man macros.