CONTROL(1) Local Manual CONTROL(1)

NAME

controlcontrol a system of communicating machines

SYNOPSIS

control [option ...] [scm-file]

DESCRIPTION

The control tool reads the model given in the specified scm-file, and performs a control algorithm during the execution (simulation) of the model. If scm-file is omitted, the model is read from the standard input.

The model contains the description of a system of communicating machines along with, optionally, the specification of a set of bad configurations. See scm(5) for a description of the scm input language.

At each step of the simulation, control displays the transitions that may be taken and asks the user to choose one. If the number provided by the user is not a possible transitions, the simulation ends. If the similation is automatic (see the options), it ends after a given number of execution steps.

OPTIONS

Main Options

-k param
Specifies the value of the extrapolation parameter. This parameter tunes the precision of the state estimates. A greater param gives more precision but the execution time exponentially increases as well. The param must be a nonnegative integer. The default is 1.
-limit limit
Limit the number of execution steps of the automatic simulation to limit. The limit must be a nonnegative integer. The default is 100.
-statistics
Upon succesful termination, control displays detailed statistics about execution time and memory consumption.

Supervisory Control Options

-simulation-mode mode
Specifies whether the simulation is automatic or not.
manual
At each step of the simulation, the user must choose one transition among the possible ones. This is the default.
auto
At each step of the simulation, one transition among the possible ones is randomly chosen.
-display-estimate
Displays the symbolic representation (QDDs) of the state estimates. By default, control does not display the state estimates, but give their size (number of QDD nodes).
-simulation-only
Simulates a run of the system and computes the state estimates, but does not control it.

Logging Options

-columns width
Use width columns for pretty-printing. In other words, set the value of the pretty-printer's right margin to width (in characters). The default is the value of the environment variable COLUMNS if set, or 78 otherwise.
-box-depth depth
Set the pretty-printer's box depth to depth. Boxes nested deeper than depth are printed as an ellipsis. OCaml's max_int is used by default.

SEE ALSO

verify(1), scm(5)

AUTHORS

The control tool is mainly written, maintained and tested by:

See the AUTHORS file in the source distribution for the full list of contributors.

Web site: ../../../projects/mcscm/wiki.html

CAVEATS

Numerical values held by messages or local variables are currently ignored by control.
  • Conditions in transitions and bad configurations are discarded and assumed to be true.
  • Assignments in transitions are ignored.

These rules guarantee that the reachability analyses performed by control are “correct”.

BUGS

Please visit the following page for bug reports and feature requests: ../../../projects/mcscm/issues

ACKNOWLEDGEMENTS

The control tool is programmed in Objective Caml and uses several 3rd-party libraries:
September 13, 2011 Linux 3.0.0-1-amd64