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

4.4 Traces Inspection Commands

A trace is a sequence of states corresponding to a possible execution of the model. Traces are created by NuSMV when a formula is found to be false; they are also generated by the simulation feature (section 4.3 Simulation Commands). Each trace has a number, and the states are numbered within the trace. Trace n has states n.1, n.2, n.3, "...".

The trace inspection commands of NuSMV allow to navigate along the traces produced by NuSMV. During the navigation, there is a current state, and the current trace is the trace the current state belongs to. The commands are the following:

Command: goto_state [-h] state

Makes state the current state.

Command: print_current_state [-h] [-v]

Prints the name of the current state if defined.

-v

Prints the value of all the state variables of the current state.

Command: step [-h] [-v]

Moves to the next state in the current trace. If the current state is the last in the trace, then an error message is printed out.

-v

Prints the value of all state variables, otherwise it prints only the values of the state variables that have changed their value from previous state.

Command: assign [-h] variable := expression

Assigns the value of expression, as evaluated in the current state, to variable.

variable := expression

Assigns the value of expression, as evaluated in the current state, to variable. This command changes the current state. The value of all other variables in the new current state remains the same as it was in the old current state.

Command: eval [-h] ctl-expression

Evaluates ctl-expression in the current state. Since we deal with CTL formulas, the evaluation activates the model checking algorithms, and can produce a new trace starting from current state, to be used by later commands. If additional traces are created from state n.i, they are numbered t+1, t+2, t+3, ..., where t is the number corresponding to the last trace generated. Within these traces, the states are numbered (t+i).1, (t+i).2, (t+i).3, ...