Go to the first, previous, next, last section, table of contents.
NuSMV allows for Real Time CTL specifications
[EMSS90]. NuSMV assumes that each transition takes unit
time for execution. RTCTL extends the syntax of CTL path expressions
with the following bounded modalities:
rtctl_expr ::
ctl_expr
| "EBF" range rtctl_expr
| "ABF" range rtctl_expr
| "EBG" range rtctl_expr
| "ABG" range rtctl_expr
| "A" "[" rtctl_expr "BU" range rtctl_expr "]"
| "E" "[" rtctl_expr "BU" range rtctl_expr "]"
range :: number ".." number"
Intuitively, in the formula E [ a BU m..n b ]
m (n, resp.) represents the minimum (maximum) number of
permitted transition along a path of a structure before the eventuality
holds.
Real time CTL specifications can be defined with the following syntax, which extends the syntax for CTL specifications.
spec_declaration :: "SPEC" rtctl_expr
With the `COMPUTE' statement, it is also possible to compute quantitative information on the Kripke structure. In particular, it is possible to compute the exact bound on the delay between two specified events, expressed as CTL formulas. The syntax is the following:
compute_declaration :: "COMPUTE" compute_expr
where
compute_expr ::
"MIN" "[" rtctl_expr "," rtctl_expr "]"
| "MAX" "[" rtctl_expr "," rtctl_expr "]"
MIN [start , final] computes the set of
states reachable from start. If at any point, we encounter a state
satisfying final, we return the number of steps taken to reach the
state. If a fixed point is reached and no states intersect final
then infinity is returned.
MAX [start , final] returns the length of
the longest path from a state in start to a state in final. If
there exists an infinite path beginning in a state in start that
never reaches a state in final, then infinity is returned.