GENERATOR manual page
Table of Contents

Name

generator - BCG graph generation using reachability analysis

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] generator [generator_opt] result[.bcg]

or:

exp.open [exp_opt] spec[.exp] [cc_opt] generator [generator_opt] result[.bcg]

or:

fsp.open [fsp_opt] spec[.lts] [cc_opt] generator [generator_opt] result[.bcg]

or:

lnt.open [lnt_opt] spec[.lnt] [cc_opt] generator [generator_opt] result[.bcg]

or:

lotos.open [lotos_opt] spec[.lotos] [cc_opt] generator [generator_opt] result[.bcg]

or:

seq.open [seq_opt] spec[.seq] [cc_opt] generator [generator_opt] result[.bcg]

Description

This program performs exhaustive reachability analysis and generates the Labelled Transition System corresponding to the BCG graph spec.bcg, the composition expression spec.exp, the FSP program spec.lts, the LNT program spec.lnt, the LOTOS program spec.lotos, or the sequence file spec.seq.

The resulting Labelled Transition System is encoded in the BCG format and stored into file result.bcg.

Note: In its first form (i.e., when applied to the BCG graph spec.bcg), this program is not very useful, since the graph has already been generated.

Options

The options bcg_opt, if any, are passed to bcg_lib .

The options exp_opt, if any, are passed to exp.open .

The options fsp_opt, if any, are passed to fsp.open .

The options lnt_opt, if any, are passed to lnt.open .

The options lotos_opt, if any, are passed to caesar and to caesar.adt .

The options seq_opt, if any, are passed to seq.open .

The options cc_opt, if any, are passed to the C compiler.

The following options generator_opt are currently available:

-monitor
Open a window for monitoring in real-time the generation of result.bcg.

-depth n
Generate the fragment of the Labelled Transition System containing all states whose distance from the initial state (i.e., the number of transitions in the shortest sequence going from the initial state to a given state) is at most n. By convention, if n = 0 (default value), the resulting Labelled Transition System is not restricted to the initial state only, but is the entire Labelled Transition System, meaning that no constraint on maximal depth applies.

-hide [ -total | -partial | -gate ] hiding_filename
Use the hiding rules defined in hiding_filename to hide (on the fly) the labels of the Labelled Transition System being generated. See the caesar_hide_1 manual page for a detailed description of the appropriate format for hiding_filename.

The -total, -partial, and -gate options specify the "total matching", "partial matching", and "gate matching" semantics, respectively. See the caesar_hide_1 manual page for more details about these semantics. Option -total is the default.

-rename [-total|-single|-multiple|-gate] renaming_filename
Use the renaming rules defined in renaming_filename to rename (on the fly) the labels of the Labelled Transition System being generated. See the caesar_rename_1 manual page for a detailed description of the appropriate format for renaming_filename.

The -total, -single, -multiple, and -gate options specify the "total matching", "single partial matching", "multiple partial matching", and "gate matching" semantics, respectively. See the caesar_rename_1 manual page for more details about these semantics. Option -total is the default.

As for the bcg_labels tool, several hiding and/or renaming options can be present on the command line, in which case they are processed from left to right.

-uncompress, -compress, -register, -short, -medium, -size
These options control the form under which the BCG graph result.bcg is generated. See the bcg manual page for a description of these options.

-unparse, -parse
These options control label parsing when the BCG graph result.bcg is generated. Default option is -parse. See the bcg_write manual page for a description of label parsing.

-tmp
This option specifies the directory in which temporary files are to be stored. See the bcg manual page for a description of this option.

Exit Status

Exit status is 0 if everything is alright, 1 otherwise.

Diagnostics

When the source is erroneous, error messages are issued.

Author

Hubert Garavel (INRIA Rhone-Alpes)

Operands

spec.bcg
BCG graph (input)

spec.exp
network of communicating LTSs (input)

spec.lts
FSP specification (input)

spec.lnt
LNT specification (input)

spec.lotos
LOTOS specification (input)

spec.seq
sequence file (input)

Files

The source code of this tool is available in file $CADP/src/open_caesar/generator.c

See the caesar_hide_1 , caesar_rename_1 , bcg_labels manual pages for a description of hiding and renaming conventions.

See Also

OPEN/CAESAR Reference Manual, bcg , bcg_open , caesar , caesar.adt , exp , exp.open , fsp.open , lnt.open , lotos , lotos.open , seq , seq.open

Additional information is available from the CADP Web page located at http://cadp.inria.fr

Directives for installation are given in files $CADP/INSTALLATION_*.

Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.

Bugs

Please report new bugs to Hubert.Garavel@inria.fr

Table of Contents