Liveness: finding starvation

The last line of the spec is "every call is eventually served". That is a liveness property: pending[f] |-> s_eventually (door_open && floor == f). Run it on the first version of the design (ANTI_STARVE = 0) and the tool reports a failure with a loop:

The trace is legal: nothing in the spec stops a passenger from pressing the button at the floor where the lift is standing. Whether this is a bug is a specification decision — exactly the kind of question exploration should raise early. The team decides that a call ahead of the lift must take priority once the current floor has been served. That is what served_here does in the final design (ANTI_STARVE = 1).

Re-proving and quantifying

1. With ANTI_STARVE = 1, a_served should be proven for all four floors.
2. Liveness says "eventually" but not "how soon". Use covers to find the worst-case wait, for example cover property (pending[3] && !door_open [*K]) for increasing K. The largest coverable K tells you the bound.
3. Turn the bound into a safety assertion, e.g. pending[3] |-> ##[0:K] (door_open && floor == 3). It is easier to prove, easier to debug, and it documents a real performance guarantee.

Exit: sharing the results

Design exploration ends with a short summary for the team: covers hit (with trace lengths), assertions proven, open questions, and spec changes (here: the anti-starvation rule). The wrapper becomes the seed of the verification FPV environment — minus the temporary assumptions.

Chapter takeaways