Download NuSMV 2.4 User Manual

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.
It is important to remark here that if the FSM is not total (i.e. it contains deadlock states)
COMPUTE may produce wrong results. It is possible to check the FSM against deadlock
states by calling the command check fsm.
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
-p "compute-expr
context]"
-n number
Writes the output generated by the command in processing
COMPUTEs to the file output-file.
[IN
A COMPUTE formula to be checked.
context
is the module instance name which the variables in
compute-expr must be evaluated in.
Computes only the property with index number.
check property - Checks a property into the current list of properties, or a newly specified property
Command
check property [-h] [-n number] | [(-c | -l | -i | -s | -q )
[-p "formula [IN context]"]]
Checks the specified property taken from the property list, or adds the new specified property and checks it. It is possible to check LTL, CTL, INVAR, PSL and quantitative
(COMPUTE) properties. Every newly inserted property is inserted and checked.
Command Options:
-c
Checks all the CTL properties not already checked. If -p is
used, the given formula is expected to be a CTL formula.
-l
Checks all the LTL properties not already checked. If -p is
used, the given formula is expected to be a LTL formula.
-i
Checks all the INVAR properties not already checked. If
-p is used, the given formula is expected to be a INVAR
formula.
-s
Checks all the PSL properties not already checked. If -p is
used, the given formula is expected to be a PSL formula.
-q
Checks all the COMPUTE properties not already checked. If
-p is used, the given formula is expected to be a COMPUTE
formula.
-p "formula [IN
context]"
Checks the formula specified on the command-line.
context is the module instance name which the variables
in formula must be evaluated in.
add property - Adds a property to the list of properties
Command
add property [-h] [(-c | -l | -i | -q | -s) -p "formula
[IN context]"]
Adds a property in the list of properties. It is possible to insert LTL, CTL, INVAR,
PSL and quantitative (COMPUTE) properties. Every newly inserted property is initialized
to unchecked. A type option must be given to properly execute the command.
53