EXECUTOR manual page
Table of Contents

Name

executor - random execution

Synopsis

bcg_open [bcg_opt] spec[.bcg] [cc_opt] executor [executor_opt] executor_param

or:

exp.open [exp_opt] spec[.exp] [cc_opt] executor [executor_opt] executor_param

or:

fsp.open [fsp_opt] spec[.lts] [cc_opt] executor [executor_opt] executor_param

or:

lnt.open [lnt_opt] spec[.lnt] [cc_opt] executor [executor_opt] executor_param

or:

lotos.open [lotos_opt] spec[.lotos] [cc_opt] executor [executor_opt] executor_param

or:

seq.open [seq_opt] spec[.seq] [cc_opt] executor [executor_opt] executor_param

Description

This program explores 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, and produces a random execution sequence.

Visible labels in the execution sequence are displayed as the corresponding transitions are fired. Invisible labels (noted ``i'') are not displayed.

The execution sequence is displayed using the full SEQ format (see the seq man page for a description of this format).

Various strategies are currently available to solve non-determinism:

(1):
Non-determinism is not allowed. The program will stop if the current state has more than one successor.

(2):
Non-determinism is allowed. If the current state has several successors, one of them is selected using a pseudo-random number generator. The seed of the generator is initialized using the system clock.

(3):
Same as strategy (2), except that the seed of the generator is provided by the user, in order to obtain reproducible execution sequences.

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 executor_opt are currently available:

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

The parameters executor_param have the following formats, where depth is an integer denoting the maximal number of transitions to be fired (if depth = 0, no upper bound is fixed) and where seed is an integer denoting the value of the chosen seed:

Exit Status

When the source is erroneous, error messages are issued. Exit status is 0 if everything is alright, 1 otherwise.

Author

Hubert Garavel (INRIA Rhone-Alpes)

Files

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)

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

See Also

OPEN/CAESAR Reference Manual, bcg_open , bcg , 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