39Verification
Repeat an FSM action four times
Goal and observed defect
repeatIncrement should perform one register increment per iteration and
complete after exactly four iterations. The body is already correct, but the
starter's control count stops after three executions. Starting from zero, the
current trace is 0 -> 1 -> 2 -> 3, so the public run exposes an off-by-one
control error rather than a bad arithmetic expression.
Before editing, predict the terminal count and explain why adding another assignment would repair only this particular sample, not the repetition contract.
Navigate the starter
Start in repeatIncrement and identify three nested pieces: the outer returned
seq, the repeat controller, and the inner seq containing the register
assignment. Then follow the Stmt into mkFSM in mkTop. The supplied start
and finish rules launch the process once and display state only after the
controller is done.
Keep the function signature, nested sequence structure, increment expression,
and supplied mkTop unchanged. The defect is in the declaration that controls
how often the valid body executes.
Make the smallest justified repair
Do not duplicate the body or change count <= count + 1. One firing of that
action already describes one unit of work. Adjust only the repetition control
so the same action receives the required number of FSM opportunities.
Predict the repaired transition sequence before Run. It must begin at zero, commit four increments in order, and reach four before completion. If the controller reaches the right number through fewer writes, an extra assignment, or a direct constant, it has not implemented the requested repeated process.
Observable completion contract
Completion means all four state transitions have committed and count is 4
when the finish rule observes the controller. The process must neither stop at
3 nor continue to 5, and it must make forward progress to done. These
conditions distinguish the intended loop from a hard-coded terminal value.
Progressive hints
Hint 1: separate body behavior from loop behavior
The body adds one exactly once each time it executes. Compare the number of required transitions with the number of body executions selected by the controller.
Hint 2: locate the off-by-one value
Inspect the expression attached to repeat; no declaration inside the nested
body needs another action.
Hint 3: preserve the control structure
repeat expresses a fixed amount of work. Change its iteration specification,
not the assignment or the surrounding FSM lifecycle.
Transfer experiment
After the required repair passes, compare fixed work with target-based work.
In a disposable edit, initialize count to 2 and predict the result of the
fixed repetition. Then consider a while (count < 4) process from the same
initial state. One performs four increments; the other stops at a target.
Restore the starter structure before grading. This experiment tests which loop
matches a specification rather than merely changing a number.