Notebook 25: SMV Step Simulator

Step through three SMV models from the lecture notes one transition at a time: the flip-flop, the modulo-4 counter, and the five-digit mechanical counter with carry and reset.

SMV Step Simulator

Chapter 7 introduces SMV by simulating small models one next() step at a time. This notebook is a hands-on version of that same simulation loop for the three running examples of the chapter: the flip-flop, the modulo-4 counter, and the five-digit mechanical counter with carry propagation and a reset input.

Each click computes next(v) from the current valuation of every variable, exactly as the ASSIGN block specifies—there is no lookahead and no hidden state beyond what’s shown.

Current state

Trace

What to try

  1. Flip-flop and modulo-4 counter are both fully deterministic—every click has exactly one possible outcome, matching ex:flipflop and sec:smv-mod4 in the chapter.
  2. Mechanical counter, no reset. Click Step nine times and watch d0 climb from 0 to 9; on the tenth click, d0 wraps to 0 and carry_out becomes true for one step, which is exactly what pushes d1 from 0 to 1. This is the carry-propagation logic from sec:mech-counter made visible one digit at a time.
  3. Push reset mid-count. Tick “push reset on next step” after a few increments, then click Step—every digit snaps back to 0 in a single transition, exactly as IVAR reset is modelled: an environment input, unconstrained until the moment you choose its value.

[!TIP] Read the full chapter in the PDF

For the ASSIGN/case semantics behind every step here, see Chapter 7, §“The SMV Modelling Language” and §“Modules: Hierarchical Modelling”.

Download the Full Lecture Notes (PDF)