The output has been slightly edited in order to make it more readable.
This model (short.smv) is taken from the
NuSMV distribution.
It is supposed that every NuSMV command is followed by a
RET keystroke. NuSMV commands are written in a bold face to
distinguish them from system output messages.
Note that the simulate argument
steps refers to the number of states that the system will generate
starting from the current state which is always stored as the first state
of a new trace (except when it is the last one in an existent trace). For this
reason the resulting trace contains 4 states (three state have been appended
to a trace containing current state at the beginning).
current state also changes executing the step command
(see section 4.4 Traces Inspection Commands) and reset command
(see section 4.7 Administration Commands) but in this last case current state is deleted.