CONTROL(1) | Local Manual | CONTROL(1) |
NAME
control — control a system of communicating machinesSYNOPSIS
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.
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/issuesACKNOWLEDGEMENTS
The control tool is programmed in Objective Caml and uses several 3rd-party libraries:- Camllib, Fixpoint, LatticeAutomata, and Scm. By and . Licensed under the LGPL. Web site: http://gforge.inria.fr/projects/bjeannet/.
September 13, 2011 | Linux 3.0.0-1-amd64 |