02Verification

Stop a rule at its limit

Problem

Intended behavior. mkGuardedCounter counts up to the value in limit and then stops there. With the default limit of five the counter must reach five, report atLimit, and never move again until setLimit restarts it.

Current behavior. The counter runs one step too far. It passes five, and because atLimit compares against a value the counter has already gone by, the flag turns on for a single cycle and then goes off for good.

Fix. Correct the condition that decides when the counting rule is allowed to fire. Leave atLimit, setLimit, and the rule body as they are.

Read the starter

Trace count, limit, and the step condition inside mkGuardedCounter. setLimit resets the count, while value and atLimit expose the resulting state. The defect is in the readiness condition, not those methods.

mkTop is the fixed public demonstration harness. It leaves the default limit in place long enough for a correct counter to reach and hold it. At cycle nine it calls setLimit(2) without printing a row. The next observation restarts at zero, advances through one to two, and holds at two. Keep this server-owned suffix unchanged; edit only mkGuardedCounter.

Predict before editing

Before running, predict the corrected public trace:

Cycle	0	1	2	3	4	5	6	7	8	9	10	11	12	13
`value`	0	1	2	3	4	5	5	5	5	—	0	1	2	2
`atLimit`	0	0	0	0	0	1	1	1	1	—	0	0	1	1

For the starter, revisit each count == limit line and predict the extra transition. Cycle nine is the unprinted reset cycle. Register writes become visible on the next line, so its reset appears at cycle ten.

Make the smallest change

Stop the counter exactly at the limit it was given.
Keep reporting atLimit for every cycle after the limit is reached.
Restart correctly when setLimit supplies a smaller limit, including zero.

Change only the comparison that decides readiness. Keep the increment, reset behavior, and methods unchanged.

Run and explain

Run the repaired design and compare its output with your prediction. Cycle eight prints the final default-phase observation, cycle nine calls setLimit(2) without an output row, and cycle ten exposes the reset to zero. Explain why each equality now disables step, so both five and two remain visible instead of being followed by an overshoot. Stopping one cycle earlier would miss the target, while stopping one cycle later passes it.

Completion check

The counter reaches every configured limit exactly.
atLimit becomes true and stays true until setLimit is called.
setLimit still resets count to zero.
Different limits use the same readiness rule.

Progressive hints and concept

Hint 1

Work out the last value of count for which the rule is still allowed to fire, then compare it with the last value you want the counter to hold.

Hint 2

The rule fires once more than it should. The comparison operator in its condition is the part that is one step too generous.

Concept

A rule condition decides the cycles on which the body may fire. Because the body writes the value the condition tests, an off-by-one in that condition lets one extra transition through, and every later reading of the state is taken past the point the design was supposed to settle at.

Extension experiment

Treat the fixed mkTop suffix as part of the submission contract and do not edit it. As a prediction-only variation, imagine its restart used a limit of three. Write the resulting suffix of the trace and identify the last cycle on which step would be enabled.