33Verification

Return the current ticket

Problem

issueTicket is an ActionValue expression with two simultaneous obligations: return the ticket visible at entry to the action and schedule the following ticket for the next call. The register update is already correct, but the return expression predicts that update too early. The starter therefore prints 41 and 42 where the contract requires 40 and 41.

Repair only the editable function. Keep its ActionValue#(UInt#(8)) type, its actionvalue block, the single state advance, and the supplied mkTop.

Read and trace before editing

Start at issueTicket, not at the display rule. Mark the register read in the scheduled write, the value used by return, and the <- binding in issueTwo. Both expressions in the action observe the register's entry value; the <= write becomes visible only in the next state.

Trace the starter before Run:

1. Entry state 40 schedules 41, while the current return expression computes the first visible ticket.
2. The next firing enters with 41 and schedules 42.
3. The issued register follows the same entry-state/next-state rule, so the public run performs exactly two issue operations.

Run once to confirm your predicted incorrect sequence. Then make the smallest possible change to the returned value. Do not remove or duplicate the write: the action side of the ActionValue contract is not defective. Run again and explain why the first result and the first committed next state differ by one.

Observable completion contract

• Starting at 40, consecutive calls return 40 and 41 in that order.
• Each execution advances next exactly once, so the states after those calls are 41 and 42.
• For any entry value n, the result denotes n while the following call observes the advanced state.
• The function remains an executable ActionValue; replacing it with a pure value or an Action does not satisfy the interface.

Progressive hints

Transfer experiment

In a scratch copy after completion, change the state step from one to two while preserving “return current, then advance.” Predict the first two results and states before running. This separates the entry-state rule from the particular increment amount. Restore the original step before submitting.