Next: LTL model checking.
Up: Advanced Functionalities
Previous: Invariant checking.
In NUSMV it is possible to compute quantitative information on the
Kripke structure [14,15]. In particular, it is possible
to compute the exact bound on the delay between two specified events,
expressed as CTL formulas:
computes the set of
states reachable from .
When a state satisfying
encountered, we return the number of steps taken so far. If a fixed
point is reached and no state satisfying
is found, then
infinity is returned.
has the dual interpretation, and
returns the length of the longest path from a state in
state in .
If there exists an infinite path beginning in a
that never reaches a state in ,
infinity is returned. This functionality is the same as in