26 lines
1.5 KiB
Text
26 lines
1.5 KiB
Text
------------------------------- MODULE Queue -------------------------------
|
|
EXTENDS Keep
|
|
|
|
QueueInit ==
|
|
/\ late = "none"
|
|
/\ inputs = <<"paused", "active">>
|
|
/\ attached = TRUE
|
|
/\ live = [edits |-> 2, gen |-> 1,
|
|
goal |-> [id |-> 1, stamp |-> 0,
|
|
status |-> "active"],
|
|
turn |-> [id |-> 1, status |-> "inProgress", api |-> FALSE]]
|
|
/\ sample = live.goal
|
|
/\ w = [cut |-> 0, cursor |-> 0, fence |-> 0, goal |-> live.goal, turn |-> live.turn,
|
|
armed |-> TRUE, fails |-> 0, due |-> "none", hold |-> "none", pending |-> FALSE, known |-> TRUE, echo |-> EmptyGoal, seed |-> EmptyGoal]
|
|
/\ wire = <<Message("goal", [live EXCEPT !.goal.status = "paused", !.edits = 1], TRUE), Message("goal", live, TRUE)>> /\ online = TRUE /\ phase = "idle" /\ req = "none"
|
|
/\ invalid = FALSE
|
|
/\ ticket = [expired |-> FALSE, status |-> "active", quota |-> FALSE]
|
|
/\ lastAct = [sent |-> FALSE, view |-> [goal |-> w.goal.id, turn |-> w.turn.id], expected |-> ticket,
|
|
origin |-> "automatic", evidence |-> TRUE, recover |-> TRUE, usage |-> FALSE]
|
|
/\ known = {1} /\ need = {} /\ resumed = {} /\ cancelled = {}
|
|
/\ stopWant = [id |-> 0, status |-> "paused", epoch |-> 0] /\ stopNeed = FALSE
|
|
|
|
QueueNext == Next /\ ~FinishTurn("interrupted")
|
|
QueueSpec == QueueInit /\ [][QueueNext]_vars /\ Fairness
|
|
QueueProgress == (<>[]online) => (<>[](live.goal.status # "paused"))
|
|
=============================================================================
|