21Implementation

Order two rule transitions

Problem

A request must preserve its seed for one entry cycle, add the stored increment in one atomic transition, expose the intermediate result while busy, then double that stored result in a second transition and return to Idle.

The starter enables both addFirst and doubleSecond in AddReady. Both write valueReg and phase, so they conflict. bsc must choose one, warn about the suppressed rule, and return the request to Idle after only one operation.

Edit only the two marked phase decisions: the next phase written by addFirst, and the guard on doubleSecond. Keep the arithmetic, interface, start method, and two separate rule bodies unchanged.

Navigate and predict

Read Phase first and note that it already has three protocol states. Then trace start: it stores the request and enters AddReady. Compare both rule guards and both write sets before reading the stage and busy methods that make phase progress observable.

Before editing, predict the compile and runtime symptoms separately. Compilation must report competing rules. At runtime, only the chosen rule updates the value, phase immediately returns to Idle, and the missing intermediate DoubleReady state proves that the two-step operation did not complete.

Restore the state machine

Use the unused phase to make the rule guards mutually exclusive. The first rule must leave work pending for the second; the second must be enabled only by that pending phase. This is a control-state correction, not an arithmetic rewrite or a priority choice.

For a request with seed 10 and increment 3, Run should agree with this trace:

Completion requires the entry state, intermediate state, and final state to be observable in that order on every request. Repeated requests must begin only from Idle. Both addition and doubling use eight-bit arithmetic, so overflow wraps at each transition. A wider combined expression truncated once can produce the same final eight-bit value, but it does not by itself preserve the separate observable DoubleReady state and its eight-bit intermediate value.

Progressive hints

Transfer experiment

After the required fix, try seed 8'hfa with increment 8'h0a. Predict the wrapped intermediate value before predicting the doubled final value. Observe that busy remains true between those calculations. This ungraded experiment checks per-transition width semantics as well as ordering.