--------------------------- MODULE LifecycleModel ---------------------------
(***************************************************************************)
(* Standalone liveness model for DLV-0017 (DLV-0008): a message in play *)
(* always eventually reaches a terminal state -- acked or dead-lettered, *)
(* never redelivered forever (message_active leads_to message_terminal). *)
(* *)
(* The lifecycle machine is one of the composed subject model's (QrustyModel *)
(* 's) disjoint sub-machines. Its SAFETY half -- retry_count never exceeds *)
(* the cap (RetriesBounded) -- is checked by provreq over the composed Spec. *)
(* Its LIVENESS half lives here, 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 lifecycle variables are disjoint *)
(* from the other machines, so checking this standalone by direct TLC, over *)
(* this machine with its own weak fairness, is sound, fast, and reproducible.*)
(* *)
(* A message cycles available -> locked and, on nack/expiry under the cap, *)
(* back to available for redelivery; at or over the cap it dead-letters. *)
(* retry_count strictly increases on each consume and is capped, so *)
(* redelivery cannot recur forever. Weak fairness on the progress actions *)
(* forces the message off any non-terminal state, so it must reach acked or *)
(* dlq. *)
(***************************************************************************)
EXTENDS Integers
MaxRetries == 2 \* per-message retry cap (DLV-0006); small for TLC
VARIABLES lifestate, \* "available" | "locked" | "acked" | "dlq"
rc \* retry_count of the message
vars == <<lifestate, rc>>
Init == /\ lifestate = "available"
/\ rc = 0
\* consume (pop): available -> locked, retry_count += 1.
LifeConsume == /\ lifestate = "available"
/\ lifestate' = "locked"
/\ rc' = rc + 1
\* ack: the lock holder acks -> terminal.
LifeAck == /\ lifestate = "locked"
/\ lifestate' = "acked"
/\ rc' = rc
\* nack under the cap: locked -> available for redelivery (DLV-0007).
LifeNackRetry == /\ lifestate = "locked"
/\ rc < MaxRetries
/\ lifestate' = "available"
/\ rc' = rc
\* nack at or over the cap: locked -> DLQ (DLV-0008).
LifeNackDlq == /\ lifestate = "locked"
/\ rc >= MaxRetries
/\ lifestate' = "dlq"
/\ rc' = rc
\* lock expiry under the cap: locked -> available for redelivery (DLV-0005/0007).
LifeExpireRetry == /\ lifestate = "locked"
/\ rc < MaxRetries
/\ lifestate' = "available"
/\ rc' = rc
\* lock expiry at or over the cap: locked -> DLQ (DLV-0015).
LifeExpireDlq == /\ lifestate = "locked"
/\ rc >= MaxRetries
/\ lifestate' = "dlq"
/\ rc' = rc
\* terminal stutter so a terminated message's state has a successor.
LifeTerminating == lifestate \in {"acked", "dlq"} /\ UNCHANGED vars
\* progress actions (everything that advances the message; not ack, not the
\* terminal stutter). Weak fairness on these forces the message toward a
\* terminal state: retry_count strictly increases on each consume and is capped,
\* so redelivery cannot recur forever -- it must reach the DLQ (or be acked).
LifeStep == LifeConsume \/ LifeNackRetry \/ LifeNackDlq \/ LifeExpireRetry \/ LifeExpireDlq
Next == LifeStep \/ LifeAck \/ LifeTerminating
LifeSpec == Init /\ [][Next]_vars /\ WF_vars(LifeStep)
(***************************************************************************)
(* Grounded observables. *)
(***************************************************************************)
\* DLV-0008 safety (the composed Spec checks the same property as its own
\* RetriesBounded; named distinctly here to avoid a cross-module name clash).
\* retry_count never exceeds the configured cap.
LifeRetriesBounded == rc <= MaxRetries
MessageActive == lifestate \in {"available", "locked"}
MessageTerminal == lifestate \in {"acked", "dlq"}
\* DLV-0008 liveness: a message still in play always eventually terminates.
MessageTerminates == MessageActive ~> MessageTerminal
=============================================================================