Skip to content

Instantly share code, notes, and snippets.

@ocadaruma

ocadaruma/DynamicPropertyReload.cfg

Last active July 16, 2023 22:51
Show Gist options
  • Save ocadaruma/70eb325080bcb0dc13fdba08900d9529 to your computer and use it in GitHub Desktop.
Save ocadaruma/70eb325080bcb0dc13fdba08900d9529 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
DynamicPropertyReload.cfg
(**********************************************)
(* Initial predicate and next-state relation. *)
(* Alternatively, you can comment out these *)
(* and use SPECIFICATION. *)
(**********************************************)
SPECIFICATION Spec
(**********************************************)
(* Specify the values of declared constants. *)
(**********************************************)
\* CONSTANT MyConstant = {0, 1}
CONSTANTS
Partitions = {1}
MaxMaxpendingTasks = 3
MaxPollRecords = 1
INVARIANT NoOffsetOverflow
\*PROPERTY EventuallyReload
(**********************************************)
(* Formulas true in every reachable state. *)
(**********************************************)
\* INVARIANT MyInvariant
(**********************************************)
(* Disable checking deadlock. *)
(**********************************************)
\* CHECK_DEADLOCK FALSE
Raw
DynamicPropertyReload.tla
---- MODULE DynamicPropertyReload ----
EXTENDS FiniteSets, Integers, Sequences, TLC
CONSTANTS
Partitions,
MaxMaxpendingTasks,
MaxPollRecords
(* --algorithm dynamic_property_reload
variables
currentValue = 1;
partitionStates = [p \in Partitions |-> [paused |-> FALSE]];
partitionContexts = [p \in Partitions |-> [
paused |-> FALSE,
pendingTasks |-> 1,
oooccCapacity |-> currentValue + MaxPollRecords,
reloadRequested |-> FALSE
]];
process subscription = "s"
variables
i = 1;
retval = {};
flag = FALSE;
begin
s_add_records:
with p \in 1..Cardinality(Partitions), records \in 0..MaxPollRecords do
if ~partitionStates[p].paused then
partitionContexts[p] := [partitionContexts[p] EXCEPT!.pendingTasks = @ + records];
end if;
end with;
s_update_hw:
i := 1;
s_update_hw_loop:
while i <= Cardinality(Partitions) do
with tasks \in 0..partitionContexts[i].pendingTasks do
partitionContexts[i] := [partitionContexts[i] EXCEPT!.pendingTasks = @ - tasks];
end with;
i := i + 1
end while;
s_pause_partitions:
i := 1;
retval := {};
s_pause_partitions_loop:
while i <= Cardinality(Partitions) do
s_pause_partitions_loop_1:
flag := ~partitionContexts[i].paused /\ partitionContexts[i].reloadRequested;
s_pause_partitions_loop_2:
flag := flag \/ (~partitionContexts[i].paused /\ partitionContexts[i].pendingTasks >= currentValue);
s_pause_partitions_loop_3:
if flag then
retval := retval \cup {i};
end if;
i := i + 1
end while;
s_pause_partitions_update:
partitionContexts := [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = TRUE] ELSE partitionContexts[p]];
partitionStates := [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = TRUE] ELSE partitionStates[p]];
s_resume_partitions:
i := 1;
retval := {};
s_resume_partitions_loop:
while i <= Cardinality(Partitions) do
s_resume_partitions_loop_1:
flag := partitionContexts[i].paused /\ ~partitionContexts[i].reloadRequested;
s_resume_partitions_loop_2:
flag := flag /\ (partitionContexts[i].paused /\ partitionContexts[i].pendingTasks < currentValue);
s_resume_partitions_loop_3:
if flag then
retval := retval \cup {i}
end if;
i := i + 1
end while;
s_resume_partitions_update:
partitionContexts := [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = FALSE] ELSE partitionContexts[p]];
partitionStates := [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = FALSE] ELSE partitionStates[p]];
s_property_reload:
partitionContexts := [p \in Partitions |-> IF /\ partitionContexts[p].pendingTasks = 0
/\ partitionContexts[p].reloadRequested
THEN [partitionContexts[p] EXCEPT
!.oooccCapacity = currentValue + MaxPollRecords,
!.reloadRequested = FALSE]
ELSE partitionContexts[p]];
goto s_add_records
end process
process property_watcher = "w"
begin
w:
if currentValue < MaxMaxpendingTasks then
currentValue := currentValue + 1;
partitionContexts := [p \in Partitions |-> [partitionContexts[p] EXCEPT!.reloadRequested = TRUE]]
end if;
goto w
end process
end algorithm
*)
\* BEGIN TRANSLATION (chksum(pcal) = "251d1cc" /\ chksum(tla) = "879700d6")
VARIABLES currentValue, partitionStates, partitionContexts, pc, i, retval,
flag
vars == << currentValue, partitionStates, partitionContexts, pc, i, retval,
flag >>
ProcSet == {"s"} \cup {"w"}
Init == (* Global variables *)
/\ currentValue = 1
/\ partitionStates = [p \in Partitions |-> [paused |-> FALSE]]
/\ partitionContexts = [p \in Partitions |-> [
paused |-> FALSE,
pendingTasks |-> 1,
oooccCapacity |-> currentValue + MaxPollRecords,
reloadRequested |-> FALSE
]]
(* Process subscription *)
/\ i = 1
/\ retval = {}
/\ flag = FALSE
/\ pc = [self \in ProcSet |-> CASE self = "s" -> "s_add_records"
[] self = "w" -> "w"]
s_add_records == /\ pc["s"] = "s_add_records"
/\ \E p \in 1..Cardinality(Partitions):
\E records \in 0..MaxPollRecords:
IF ~partitionStates[p].paused
THEN /\ partitionContexts' = [partitionContexts EXCEPT ![p] = [partitionContexts[p] EXCEPT!.pendingTasks = @ + records]]
ELSE /\ TRUE
/\ UNCHANGED partitionContexts
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw"]
/\ UNCHANGED << currentValue, partitionStates, i, retval,
flag >>
s_update_hw == /\ pc["s"] = "s_update_hw"
/\ i' = 1
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, retval, flag >>
s_update_hw_loop == /\ pc["s"] = "s_update_hw_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ \E tasks \in 0..partitionContexts[i].pendingTasks:
partitionContexts' = [partitionContexts EXCEPT ![i] = [partitionContexts[i] EXCEPT!.pendingTasks = @ - tasks]]
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw_loop"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions"]
/\ UNCHANGED << partitionContexts, i >>
/\ UNCHANGED << currentValue, partitionStates, retval,
flag >>
s_pause_partitions == /\ pc["s"] = "s_pause_partitions"
/\ i' = 1
/\ retval' = {}
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_pause_partitions_loop == /\ pc["s"] = "s_pause_partitions_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop_1"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_update"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval, flag >>
s_pause_partitions_loop_1 == /\ pc["s"] = "s_pause_partitions_loop_1"
/\ flag' = (~partitionContexts[i].paused /\ partitionContexts[i].reloadRequested)
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop_2"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_pause_partitions_loop_2 == /\ pc["s"] = "s_pause_partitions_loop_2"
/\ flag' = (flag \/ (~partitionContexts[i].paused /\ partitionContexts[i].pendingTasks >= currentValue))
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop_3"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_pause_partitions_loop_3 == /\ pc["s"] = "s_pause_partitions_loop_3"
/\ IF flag
THEN /\ retval' = (retval \cup {i})
ELSE /\ TRUE
/\ UNCHANGED retval
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_pause_partitions_update == /\ pc["s"] = "s_pause_partitions_update"
/\ partitionContexts' = [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = TRUE] ELSE partitionContexts[p]]
/\ partitionStates' = [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = TRUE] ELSE partitionStates[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions"]
/\ UNCHANGED << currentValue, i, retval, flag >>
s_resume_partitions == /\ pc["s"] = "s_resume_partitions"
/\ i' = 1
/\ retval' = {}
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_resume_partitions_loop == /\ pc["s"] = "s_resume_partitions_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop_1"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_update"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval, flag >>
s_resume_partitions_loop_1 == /\ pc["s"] = "s_resume_partitions_loop_1"
/\ flag' = (partitionContexts[i].paused /\ ~partitionContexts[i].reloadRequested)
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop_2"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_resume_partitions_loop_2 == /\ pc["s"] = "s_resume_partitions_loop_2"
/\ flag' = (flag /\ (partitionContexts[i].paused /\ partitionContexts[i].pendingTasks < currentValue))
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop_3"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_resume_partitions_loop_3 == /\ pc["s"] = "s_resume_partitions_loop_3"
/\ IF flag
THEN /\ retval' = (retval \cup {i})
ELSE /\ TRUE
/\ UNCHANGED retval
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_resume_partitions_update == /\ pc["s"] = "s_resume_partitions_update"
/\ partitionContexts' = [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = FALSE] ELSE partitionContexts[p]]
/\ partitionStates' = [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = FALSE] ELSE partitionStates[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_property_reload"]
/\ UNCHANGED << currentValue, i, retval, flag >>
s_property_reload == /\ pc["s"] = "s_property_reload"
/\ partitionContexts' = [p \in Partitions |-> IF /\ partitionContexts[p].pendingTasks = 0
/\ partitionContexts[p].reloadRequested
THEN [partitionContexts[p] EXCEPT
!.oooccCapacity = currentValue + MaxPollRecords,
!.reloadRequested = FALSE]
ELSE partitionContexts[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_add_records"]
/\ UNCHANGED << currentValue, partitionStates, i, retval,
flag >>
subscription == s_add_records \/ s_update_hw \/ s_update_hw_loop
\/ s_pause_partitions \/ s_pause_partitions_loop
\/ s_pause_partitions_loop_1
\/ s_pause_partitions_loop_2
\/ s_pause_partitions_loop_3
\/ s_pause_partitions_update \/ s_resume_partitions
\/ s_resume_partitions_loop
\/ s_resume_partitions_loop_1
\/ s_resume_partitions_loop_2
\/ s_resume_partitions_loop_3
\/ s_resume_partitions_update \/ s_property_reload
w == /\ pc["w"] = "w"
/\ IF currentValue < MaxMaxpendingTasks
THEN /\ currentValue' = currentValue + 1
/\ partitionContexts' = [p \in Partitions |-> [partitionContexts[p] EXCEPT!.reloadRequested = TRUE]]
ELSE /\ TRUE
/\ UNCHANGED << currentValue, partitionContexts >>
/\ pc' = [pc EXCEPT !["w"] = "w"]
/\ UNCHANGED << partitionStates, i, retval, flag >>
property_watcher == w
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == subscription \/ property_watcher
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
NoOffsetOverflow ==
\A p \in Partitions: partitionContexts[p].pendingTasks <= partitionContexts[p].oooccCapacity
\*EventuallyReload ==
\* <>[](\A p \in Partitions: partitionContexts[p].oooccCapacity = currentValue + MaxPollRecords)
====
Raw
DynamicPropertyReload_fix.tla
---- MODULE DynamicPropertyReload_fix ----
EXTENDS FiniteSets, Integers, Sequences, TLC
CONSTANTS
Partitions,
MaxMaxpendingTasks,
MaxPollRecords
(* --algorithm dynamic_property_reload_fix
variables
currentValue = 1;
partitionStates = [p \in Partitions |-> [paused |-> FALSE]];
partitionContexts = [p \in Partitions |-> [
paused |-> FALSE,
pendingTasks |-> 0,
oooccCapacity |-> currentValue + MaxPollRecords,
reloadRequested |-> FALSE,
maxPendingTasks |-> currentValue
]];
process subscription = "s"
variables
i = 1;
retval = {};
flag = FALSE;
begin
s_add_records:
with p \in 1..Cardinality(Partitions), records \in 0..MaxPollRecords do
if ~partitionStates[p].paused then
partitionContexts[p] := [partitionContexts[p] EXCEPT!.pendingTasks = @ + records];
end if;
end with;
s_update_hw:
i := 1;
s_update_hw_loop:
while i <= Cardinality(Partitions) do
with tasks \in 0..partitionContexts[i].pendingTasks do
partitionContexts[i] := [partitionContexts[i] EXCEPT!.pendingTasks = @ - tasks];
end with;
i := i + 1
end while;
s_pause_partitions:
i := 1;
retval := {};
s_pause_partitions_loop:
while i <= Cardinality(Partitions) do
s_pause_partitions_loop_1:
flag := ~partitionContexts[i].paused /\ partitionContexts[i].reloadRequested;
s_pause_partitions_loop_2:
flag := flag \/ (~partitionContexts[i].paused /\ partitionContexts[i].pendingTasks >= partitionContexts[i].maxPendingTasks);
s_pause_partitions_loop_3:
if flag then
retval := retval \cup {i};
end if;
i := i + 1
end while;
s_pause_partitions_update:
partitionContexts := [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = TRUE] ELSE partitionContexts[p]];
partitionStates := [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = TRUE] ELSE partitionStates[p]];
s_resume_partitions:
i := 1;
retval := {};
s_resume_partitions_loop:
while i <= Cardinality(Partitions) do
s_resume_partitions_loop_1:
flag := partitionContexts[i].paused /\ ~partitionContexts[i].reloadRequested;
s_resume_partitions_loop_2:
flag := flag /\ (partitionContexts[i].paused /\ partitionContexts[i].pendingTasks < partitionContexts[i].maxPendingTasks);
s_resume_partitions_loop_3:
if flag then
retval := retval \cup {i}
end if;
i := i + 1
end while;
s_resume_partitions_update:
partitionContexts := [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = FALSE] ELSE partitionContexts[p]];
partitionStates := [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = FALSE] ELSE partitionStates[p]];
s_property_reload:
partitionContexts := [p \in Partitions |-> IF /\ partitionContexts[p].pendingTasks = 0
/\ partitionContexts[p].reloadRequested
THEN [partitionContexts[p] EXCEPT
!.oooccCapacity = currentValue + MaxPollRecords,
!.reloadRequested = FALSE,
!.maxPendingTasks = currentValue]
ELSE partitionContexts[p]];
goto s_add_records
end process
process property_watcher = "w"
begin
w:
if currentValue < MaxMaxpendingTasks then
currentValue := currentValue + 1;
partitionContexts := [p \in Partitions |-> [partitionContexts[p] EXCEPT!.reloadRequested = TRUE]]
end if;
goto w
end process
end algorithm
*)
\* BEGIN TRANSLATION (chksum(pcal) = "cc980600" /\ chksum(tla) = "517fa07d")
VARIABLES currentValue, partitionStates, partitionContexts, pc, i, retval,
flag
vars == << currentValue, partitionStates, partitionContexts, pc, i, retval,
flag >>
ProcSet == {"s"} \cup {"w"}
Init == (* Global variables *)
/\ currentValue = 1
/\ partitionStates = [p \in Partitions |-> [paused |-> FALSE]]
/\ partitionContexts = [p \in Partitions |-> [
paused |-> FALSE,
pendingTasks |-> 0,
oooccCapacity |-> currentValue + MaxPollRecords,
reloadRequested |-> FALSE,
maxPendingTasks |-> currentValue
]]
(* Process subscription *)
/\ i = 1
/\ retval = {}
/\ flag = FALSE
/\ pc = [self \in ProcSet |-> CASE self = "s" -> "s_add_records"
[] self = "w" -> "w"]
s_add_records == /\ pc["s"] = "s_add_records"
/\ \E p \in 1..Cardinality(Partitions):
\E records \in 0..MaxPollRecords:
IF ~partitionStates[p].paused
THEN /\ partitionContexts' = [partitionContexts EXCEPT ![p] = [partitionContexts[p] EXCEPT!.pendingTasks = @ + records]]
ELSE /\ TRUE
/\ UNCHANGED partitionContexts
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw"]
/\ UNCHANGED << currentValue, partitionStates, i, retval,
flag >>
s_update_hw == /\ pc["s"] = "s_update_hw"
/\ i' = 1
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, retval, flag >>
s_update_hw_loop == /\ pc["s"] = "s_update_hw_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ \E tasks \in 0..partitionContexts[i].pendingTasks:
partitionContexts' = [partitionContexts EXCEPT ![i] = [partitionContexts[i] EXCEPT!.pendingTasks = @ - tasks]]
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw_loop"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions"]
/\ UNCHANGED << partitionContexts, i >>
/\ UNCHANGED << currentValue, partitionStates, retval,
flag >>
s_pause_partitions == /\ pc["s"] = "s_pause_partitions"
/\ i' = 1
/\ retval' = {}
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_pause_partitions_loop == /\ pc["s"] = "s_pause_partitions_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop_1"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_update"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval, flag >>
s_pause_partitions_loop_1 == /\ pc["s"] = "s_pause_partitions_loop_1"
/\ flag' = (~partitionContexts[i].paused /\ partitionContexts[i].reloadRequested)
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop_2"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_pause_partitions_loop_2 == /\ pc["s"] = "s_pause_partitions_loop_2"
/\ flag' = (flag \/ (~partitionContexts[i].paused /\ partitionContexts[i].pendingTasks >= partitionContexts[i].maxPendingTasks))
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop_3"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_pause_partitions_loop_3 == /\ pc["s"] = "s_pause_partitions_loop_3"
/\ IF flag
THEN /\ retval' = (retval \cup {i})
ELSE /\ TRUE
/\ UNCHANGED retval
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_pause_partitions_update == /\ pc["s"] = "s_pause_partitions_update"
/\ partitionContexts' = [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = TRUE] ELSE partitionContexts[p]]
/\ partitionStates' = [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = TRUE] ELSE partitionStates[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions"]
/\ UNCHANGED << currentValue, i, retval, flag >>
s_resume_partitions == /\ pc["s"] = "s_resume_partitions"
/\ i' = 1
/\ retval' = {}
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_resume_partitions_loop == /\ pc["s"] = "s_resume_partitions_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop_1"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_update"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval, flag >>
s_resume_partitions_loop_1 == /\ pc["s"] = "s_resume_partitions_loop_1"
/\ flag' = (partitionContexts[i].paused /\ ~partitionContexts[i].reloadRequested)
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop_2"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_resume_partitions_loop_2 == /\ pc["s"] = "s_resume_partitions_loop_2"
/\ flag' = (flag /\ (partitionContexts[i].paused /\ partitionContexts[i].pendingTasks < partitionContexts[i].maxPendingTasks))
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop_3"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, i, retval >>
s_resume_partitions_loop_3 == /\ pc["s"] = "s_resume_partitions_loop_3"
/\ IF flag
THEN /\ retval' = (retval \cup {i})
ELSE /\ TRUE
/\ UNCHANGED retval
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, flag >>
s_resume_partitions_update == /\ pc["s"] = "s_resume_partitions_update"
/\ partitionContexts' = [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = FALSE] ELSE partitionContexts[p]]
/\ partitionStates' = [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = FALSE] ELSE partitionStates[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_property_reload"]
/\ UNCHANGED << currentValue, i, retval, flag >>
s_property_reload == /\ pc["s"] = "s_property_reload"
/\ partitionContexts' = [p \in Partitions |-> IF /\ partitionContexts[p].pendingTasks = 0
/\ partitionContexts[p].reloadRequested
THEN [partitionContexts[p] EXCEPT
!.oooccCapacity = currentValue + MaxPollRecords,
!.reloadRequested = FALSE,
!.maxPendingTasks = currentValue]
ELSE partitionContexts[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_add_records"]
/\ UNCHANGED << currentValue, partitionStates, i, retval,
flag >>
subscription == s_add_records \/ s_update_hw \/ s_update_hw_loop
\/ s_pause_partitions \/ s_pause_partitions_loop
\/ s_pause_partitions_loop_1
\/ s_pause_partitions_loop_2
\/ s_pause_partitions_loop_3
\/ s_pause_partitions_update \/ s_resume_partitions
\/ s_resume_partitions_loop
\/ s_resume_partitions_loop_1
\/ s_resume_partitions_loop_2
\/ s_resume_partitions_loop_3
\/ s_resume_partitions_update \/ s_property_reload
w == /\ pc["w"] = "w"
/\ IF currentValue < MaxMaxpendingTasks
THEN /\ currentValue' = currentValue + 1
/\ partitionContexts' = [p \in Partitions |-> [partitionContexts[p] EXCEPT!.reloadRequested = TRUE]]
ELSE /\ TRUE
/\ UNCHANGED << currentValue, partitionContexts >>
/\ pc' = [pc EXCEPT !["w"] = "w"]
/\ UNCHANGED << partitionStates, i, retval, flag >>
property_watcher == w
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == subscription \/ property_watcher
\/ Terminating
Spec == Init /\ [][Next]_vars
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
NoOffsetOverflow ==
\A p \in Partitions: partitionContexts[p].pendingTasks <= partitionContexts[p].oooccCapacity
\*EventuallyReload ==
\* <>[](\A p \in Partitions: partitionContexts[p].oooccCapacity = currentValue + MaxPollRecords)
====
Raw
result.log
Invariant NoOffsetOverflow is violated.
Raw
trace.log
1. Initial predicate
flag FALSE
retval {}
i 1
pc [w |-> "w", s |-> "s_add_records"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 1, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
2. DynamicPropertyReload:s_add_records
flag FALSE
retval {}
i 1
pc [w |-> "w", s |-> "s_update_hw"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
3. DynamicPropertyReload:s_update_hw
flag FALSE
retval {}
i 1
pc [w |-> "w", s |-> "s_update_hw_loop"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
[1] [paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]
partitionStates <<[paused |-> FALSE]>>
4. DynamicPropertyReload:s_update_hw_loop
flag FALSE
retval {}
i 2
pc [w |-> "w", s |-> "s_update_hw_loop"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
5. DynamicPropertyReload:s_update_hw_loop
flag FALSE
retval {}
i 2
pc [w |-> "w", s |-> "s_pause_partitions"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
6. DynamicPropertyReload:s_pause_partitions
flag FALSE
retval {}
i 1
pc [w |-> "w", s |-> "s_pause_partitions_loop"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
7. DynamicPropertyReload:s_pause_partitions_loop
flag FALSE
retval {}
i 1
pc [w |-> "w", s |-> "s_pause_partitions_loop_1"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
8. DynamicPropertyReload:s_pause_partitions_loop_1
flag FALSE
retval {}
i 1
pc [w |-> "w", s |-> "s_pause_partitions_loop_2"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
9. DynamicPropertyReload:s_pause_partitions_loop_2
flag TRUE
retval {}
i 1
pc [w |-> "w", s |-> "s_pause_partitions_loop_3"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
10. DynamicPropertyReload:s_pause_partitions_loop_3
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_pause_partitions_loop"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
11. DynamicPropertyReload:s_pause_partitions_loop
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_pause_partitions_update"]
currentValue 1
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> FALSE]>>
12. DynamicPropertyReload:s_pause_partitions_update
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_resume_partitions"]
currentValue 1
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
[1] [paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]
paused TRUE
pendingTasks 2
oooccCapacity 2
reloadRequested FALSE
partitionStates <<[paused |-> TRUE]>>
13. DynamicPropertyReload:s_resume_partitions
flag TRUE
retval {}
i 1
pc [w |-> "w", s |-> "s_resume_partitions_loop"]
currentValue 1
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> TRUE]>>
14. DynamicPropertyReload:s_resume_partitions_loop
flag TRUE
retval {}
i 1
pc [w |-> "w", s |-> "s_resume_partitions_loop_1"]
currentValue 1
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> TRUE]>>
15. DynamicPropertyReload:s_resume_partitions_loop_1
flag TRUE
retval {}
i 1
pc [w |-> "w", s |-> "s_resume_partitions_loop_2"]
currentValue 1
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> FALSE]>>
partitionStates <<[paused |-> TRUE]>>
16. DynamicPropertyReload:w
flag TRUE
retval {}
i 1
pc [w |-> "w", s |-> "s_resume_partitions_loop_2"]
currentValue 2
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
partitionStates <<[paused |-> TRUE]>>
17. DynamicPropertyReload:w
flag TRUE
retval {}
i 1
pc [w |-> "w", s |-> "s_resume_partitions_loop_2"]
currentValue 3
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
partitionStates <<[paused |-> TRUE]>>
18. DynamicPropertyReload:s_resume_partitions_loop_2
flag TRUE
retval {}
i 1
pc [w |-> "w", s |-> "s_resume_partitions_loop_3"]
currentValue 3
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
partitionStates <<[paused |-> TRUE]>>
19. DynamicPropertyReload:s_resume_partitions_loop_3
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_resume_partitions_loop"]
currentValue 3
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
partitionStates <<[paused |-> TRUE]>>
20. DynamicPropertyReload:s_resume_partitions_loop
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_resume_partitions_update"]
currentValue 3
partitionContexts <<[paused |-> TRUE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
partitionStates <<[paused |-> TRUE]>>
21. DynamicPropertyReload:s_resume_partitions_update
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_property_reload"]
currentValue 3
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
[1] [paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]
paused FALSE
pendingTasks 2
oooccCapacity 2
reloadRequested TRUE
partitionStates <<[paused |-> FALSE]>>
22. DynamicPropertyReload:s_property_reload
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_add_records"]
currentValue 3
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 2, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
partitionStates <<[paused |-> FALSE]>>
23. DynamicPropertyReload:s_add_records
flag TRUE
retval {1}
i 2
pc [w |-> "w", s |-> "s_update_hw"]
currentValue 3
partitionContexts <<[paused |-> FALSE, pendingTasks |-> 3, oooccCapacity |-> 2, reloadRequested |-> TRUE]>>
partitionStates <<[paused |-> FALSE]>>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment