Go to the first, previous, next, last section, table of contents.

4.5 Model Modification Commands

NuSMV allows for interactively modifying the Kripke structure. This can be done by changing the transition relation, the initial states, or adding new fairness constraints. To activate the modification mode, it is necessary to save the model with the command dump_model. The saved model can be restored after the modifications with the command restore_model.

Command: dump_model [-h]

Initializes the system to allow interactive model modification. This command is currently available only with the `Monolithic' partition method.

Command: add_init [-h] simple-expression

Modifies the initial states. simple-expression is evaluated and conjoined with the set of initial states to form the new set of initial states. This command has the same effect of an INIT declaration in the original input file. Before executing this command, the dump_model command must have been executed.

Command: add_trans [-h] trans-expression

Modifies the transition relation. trans-expression is evaluated and then conjoined with the current transition relation. This command has the same effect of a TRANS statement in the original input file. Before executing this command, the dump_model command must have been executed.

Command: add_fairness [-h] ctl-expression

Add a new fairness constraint to the existing list of fairness constraints. ctl-expression is evaluated and added to the current list of fairness constraints. This command has the same effect of a FAIRNESS statement in the original input file. Before executing this command, the dump_model command must have been executed.

Command: restore_model [-h]

This command cancels the effect of all add_fairness, add_init and add_trans commands issued inside the model inspection session, i.e. after the dump_model command.