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
be the set of initial states,
the
set of invariants,
the transition relation and
the set of fairness constraints. Then the
modifications act as follows:

where , are the added set of initial states and invariant states respectively. is the added transition relation and 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.

NuSMV <>