On the fly modification of the model.

The user might want to try to modify the model (e.g to try to fix a bug) or add new fairness constraints without restarting the computation from scratch. In NUSMV this can be done using shell commands that allow the user to modify interactively the model. The user can impose a new constraint on the set of initial states, the set of invariant states or on the transition relation. Let $\ \mathcal{I}$ be the set of initial states, $\mathit{Inv}$ the set of invariants, $T(\cdot,\cdot)$ the transition relation and $\mathcal{H}$ the set of fairness constraints. Then the modifications act as follows:

$$\begin{array}{c@{\hspace{1cm}}c} \mathcal{I} := \mathcal{I} ... ... \mathcal{H} := \mathcal{H} \cup \{\mathit{h}_a\} \end{array}$$

where $\mathcal{I}_a$, $\mathit{Inv}_a$ are the added set of initial states and invariant states respectively. $T_a(\cdot, \cdot)$ is the added transition relation and $\mathit{h}_a$ is the new fairness constraint. Moreover, NUSMV allows the user to undo the modifications and restore the original status of the system. This is useful in case the user wants to try further modifications.