Next: Invariant checking.
Up: Advanced Functionalities
Previous: Advanced Functionalities
NUSMV allows expressing specifications in real-time CTL (RTCTL) .
For example, it is possible to express that
always leads to
in 0 to 4 time units with the RTCTL
It is assumed that a time unit corresponds to a step.
This functionality is the same as in CMU SMV.