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] [-sp n] [-tp n] [-wp n] [-g] [-tina | -fw] -i file]

ktzio [-help] [-KTZ | -BCG | -AUT]
[-ktz | -bcg |-aut | -mec | -cwb | -ktj | -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
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.

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 written 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 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 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 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 -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), tedd(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 ktzio (n) Version 3.5.0
Generated by manServer 1.07 from src/ktzio.n using man macros.