Nondeterminism in NuSMV Verification
The verification provided by NuSMV does not support the non-determinism in case at the same time the guards of more transitions are true. For example, we consider one state with three outgoing transitions: if the conditions for two transitions are either fireble, the third transition will be never considered as fireable. Nevertheless, the third transition may be executed in a non-deterministic scenario.
(from redmine: issue id 768, created on 2012-04-16, closed on 2012-05-19)
- Relations:
- parent #849 (closed)