20Verification

Remove an arbitrary rule conflict

Problem

Each accepted request stores an eight-bit amount and a Boolean operation choice. A boosted request must double the amount; a plain request must add five. Exactly one rule serves the request, increments its own counter, and clears busy.

The starter guards both applyBoost and applyOffset with pending alone. Whenever work arrives, both rules are enabled and both write resultReg and pending. bsc must choose a winner, warn that the other rule is suppressed, and apply that same winner's transformation regardless of boostReg.

Edit only the two rule conditions. Keep both action bodies, the request method, counters, widths, and interface unchanged. The corrected conditions must encode the stored request choice and must never be true together.

Navigate and predict

Read request before the rules. It records amount, records boost, and sets pending; because register writes commit at the edge, neither worker serves a request in its arrival cycle. Next, compare the worker write sets. Finish with result, both counters, and busy, which expose which rule actually fired.

Before editing, predict two symptoms. Compilation reports a scheduling conflict and a rule that cannot win under the chosen priority. At runtime, the visible plain request can still receive the boosted transformation if applyBoost has priority, or every request can receive the offset transformation under the opposite priority. A deterministic visible result does not make either schedule correct.

Make the choice part of enablement

The stored Boolean already distinguishes the operations. Combine that choice with the existing pending-work condition so one worker is enabled for each request. This removes the conflict at its source; an if inside one action or a priority annotation would still leave the other worker unselected.

Use Run and reason across request and service cycles:

Observation point	Plain request	Boosted request
Before request	`busy` is false; prior result and counters are stable.	Same contract.
After request edge	Amount and choice are stored, `busy` is true, and neither counter has advanced.	Same contract.
Service edge	Only the offset rule adds five and increments `offsetCount`.	Only the boost rule doubles and increments `boostCount`.
Following state	Wrapped eight-bit result is visible and `busy` is false.	Wrapped eight-bit result is visible and `busy` is false.

Completion requires alternating and repeated requests to update only the matching counter, preserve the previous result during the arrival cycle, and wrap each transformation to eight bits. Compilation must no longer report a suppressed or dead worker rule.

Progressive hints

Hint 1 — find the missing information

List the state read by each rule guard. One register written by request records the operation but is absent from both lists.

Hint 2 — narrow the edit

Keep pending in both guards. Add the stored operation choice at the two rule headers; do not move the choice into either body.

Hint 3 — prove exclusivity

One guard needs the Boolean case for boosting and the other needs its logical complement. For either stored Boolean value, write a two-row truth table and verify that exactly one complete guard is true while pending.

Transfer experiment

After the fix, run once with the visible request marked boosted, then run with a plain amount near 8'hff. Predict the selected counter and wrapped result each time. Changing only the request fields should select behavior without changing rule order or introducing a warning. This experiment is not part of grading.