Model checking (experimental)
This release features a re-engineered implementation of model checking analyses which is still in experimental phase. It supports the models with following restrictions:
- only integer, boolean and enums types are supported (arrays and structures are not supported)
- only for atomic components are supported (hierarchical components are not supported)
- only strongly causal components are supported
- only state automaton is supported as component specification (operator panels, code specification, mode automatons are not supported)
It can be triggered by selecting the option "NuSMV/nuXmv (re-engineered and experimental)" from the dropdown menu "Prover to be used" in the "AG, contracts, patterns" window.