-------------------------- MODULE ScanLivenessModel -------------------------
(***************************************************************************)
(* Standalone liveness model for PER-0022: the bounded queue-scan loop *)
(* always terminates (scan_active leads_to scan_done). *)
(* *)
(* The scan machine is one of the composed subject model's (QrustyModel's) *)
(* disjoint sub-machines. Its SAFETY half -- the scan returns only in-range *)
(* keys (ScanYieldsOnlyInRange) -- is checked by provreq over the composed *)
(* Spec. Its LIVENESS half lives here instead, because liveness over the *)
(* composed Spec is intractable at the current machine count (re-verify *)
(* times out, so the verdict could not be reproduced). The scan's variables *)
(* are disjoint from the other machines, which can neither enable nor *)
(* disable a scan step, so composing them in would only multiply the state *)
(* space without changing this property's truth -- checking it standalone by *)
(* direct TLC, over this machine with its own weak fairness, is sound, fast, *)
(* and reproducible. *)
(* *)
(* RocksDB keys are a total order 0..MaxKey; a scan for one queue is bounded *)
(* to [Lo, Hi). Weak fairness on the productive steps makes the loop run to *)
(* completion: it cannot stall mid-scan, so it always reaches `done`. *)
(***************************************************************************)
EXTENDS Integers, FiniteSets
MaxKey == 6
Lo == 2
Hi == 5
VARIABLES store, \* stored keys at scan time (fixed once opened)
pos, \* iterator cursor: least key still to consider
yielded, \* keys the scan has returned so far
done \* the loop has finished
vars == <<store, pos, yielded, done>>
Init == /\ store \in SUBSET (0..MaxKey)
/\ pos = Lo
/\ yielded = {}
/\ done = FALSE
\* stored keys at or after the cursor that the bounded iterator can still see.
Remaining(p) == { k \in store : (k >= p) /\ (k < Hi) }
\* advance to the next in-range stored key (ascending) and return it.
ScanStep == /\ ~done
/\ Remaining(pos) # {}
/\ LET k == CHOOSE k \in Remaining(pos) : \A j \in Remaining(pos) : k =< j
IN /\ yielded' = yielded \cup {k}
/\ pos' = k + 1
/\ UNCHANGED <<store, done>>
\* no stored key in [pos, Hi): the upper bound is reached, the scan stops.
ScanFinish == /\ ~done
/\ Remaining(pos) = {}
/\ done' = TRUE
/\ UNCHANGED <<store, pos, yielded>>
\* once finished, the scan stutters.
ScanTerminating == done /\ UNCHANGED vars
Next == ScanStep \/ ScanFinish \/ ScanTerminating
\* Weak fairness on the productive steps forces the loop to run to completion
\* (in isolation the vars tuple is the whole state, so no cross-machine framing
\* is needed -- the gymnastics the composed model required are gone).
ScanSpec == Init /\ [][Next]_vars /\ WF_vars(ScanStep) /\ WF_vars(ScanFinish)
(***************************************************************************)
(* Grounded observables. *)
(***************************************************************************)
ScanActive == ~done
ScanDone == done
\* PER-0022 liveness: a running scan always eventually finishes.
ScanTerminates == ScanActive ~> ScanDone
=============================================================================