EXECUTOR manual page
Table of Contents

Name

executor - random execution

Synopsis

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

or:

caesar.open [caesar_opt] spec[.lotos] [cc_opt] executor executor_param

or:

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

or:

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

or:

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

or:

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

Description

This program explores the labelled transition system corresponding to the BCG graph spec.bcg, the LOTOS program spec.lotos, the composition expression spec.exp, the FSP program spec.lts, the LOTOS NT program spec.lnt, 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 SEQUENCE format (see the exhibitor 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 caesar_opt, if any, are passed to caesar and to caesar.adt .

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 seq_opt, if any, are passed to seq.open .

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

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.lotos
LOTOS specification (input)

spec.lts
FSP specification (input)

spec.lnt
LOTOS NT 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

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

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

Directives for installation are given in file $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