compute - Performs computation of quantitative characteristics


compute [-h] [-m | -o output-file] [-n number | -p "compute-expr [IN context]"]

This command deals with the computation of quantitative characteristics of real time systems. It is able to compute the length of the shortest (longest) path from two given set of states.

MAX [ alpha , beta ]

MIN [ alpha , beta ]

Properties of the above form can be specified in the input file via the keyword COMPUTE or directly at command line, using option -p.

Option -n can be used for computing a particular expression in the model. If neither -n nor -p are used, all the COMPUTE specifications are computed.

Command options:

-m
Pipes the output generated by the command in processing COMPUTEs to the program specified by the PAGER shell variable if defined, else through the UNIX command "more".
-o output-file
Writes the output generated by the command in processing COMPUTEs to the file output-file.
-p "compute-expr [IN context]"
A COMPUTE formula to be checked. context is the module instance name which the variables in compute-expr must be evaluated in.
-n number
Computes only the property with index number

Last updated on 2009/01/30 14h:53