17Verification

Issue the current ticket

Problem

Ticket.take must perform two inseparable parts of one transaction: return the ticket currently stored in next, and schedule the following ticket number as the next state. The starter gets the update right but derives the result from the following number. The public run therefore issues decimal 2, 3, and 4 instead of beginning with 1.

Repair only the faulty behavior inside mkTicket. Keep take as an ActionValue method, preserve its state update, and do not modify the supplied top module. The result and the next state are related but are not the same cycle's value.

Read, predict, and repair

Read starter/Main.bsv in this order:

Read interface Ticket; distinguish the ActionValue result of take from the value-method observation nextValue.
Find the initial state of next.
Within take, separately label the scheduled write and the returned expression.
Follow issue, noting that <- binds the issued value from each call.
Predict the pair (issued value, next stored state) for each cycle before changing code.

For the first transaction, both reads of next see the pre-update state 1. The <= write schedules 2 for the next cycle; source-code order does not make that new state visible to the later return. The same trace should continue as the pairs (1, 2), (2, 3), and (3, 4). The minimal repair leaves the already-correct transition alone and changes only the expression that selects the transaction result.

Run after the edit. Completion is observable when the public issued sequence starts at decimal 1 and advances without gaps. Also explain why the stored next number is one greater after every call; checking only the printed result would miss a repair that accidentally removed the state update.

Progressive hints

Hint 1 — split the contract

Write down two obligations: what the caller receives now, and what the register contains next cycle. Check each line of take against only one obligation.

Hint 2 — apply atomic register semantics

A nonblocking <= assignment schedules a future register value. Every read of that register in the same atomic action still denotes the pre-update value.

Hint 3 — narrow the edit

The next-state assignment already advances by one. The return expression should select the state being issued in this transaction, without applying the next-state arithmetic a second time.

Transfer experiment

After the required repair works, initialize next to 8'hfe and predict three issued values before running. Then account for the stored next state after each call, including wraparound. The experiment tests the same ActionValue contract at a width boundary rather than only near one.