From b3a6bc6a3966b1aaca407ac4a452ae1f21d06021 Mon Sep 17 00:00:00 2001 From: Piotr Kazmierczak <470696+pkazmierczak@users.noreply.github.com> Date: Fri, 21 Nov 2025 13:31:10 +0100 Subject: [PATCH 1/4] scheduler: TLA+ spec of the system scheduler --- scheduler/spec/.gitignore | 2 + scheduler/spec/system/SystemScheduler.cfg | 34 +++++ scheduler/spec/system/SystemScheduler.tla | 152 ++++++++++++++++++++++ 3 files changed, 188 insertions(+) create mode 100644 scheduler/spec/.gitignore create mode 100644 scheduler/spec/system/SystemScheduler.cfg create mode 100644 scheduler/spec/system/SystemScheduler.tla diff --git a/scheduler/spec/.gitignore b/scheduler/spec/.gitignore new file mode 100644 index 00000000000..2b9579fa498 --- /dev/null +++ b/scheduler/spec/.gitignore @@ -0,0 +1,2 @@ +states +*.out \ No newline at end of file diff --git a/scheduler/spec/system/SystemScheduler.cfg b/scheduler/spec/system/SystemScheduler.cfg new file mode 100644 index 00000000000..53f08fecd3e --- /dev/null +++ b/scheduler/spec/system/SystemScheduler.cfg @@ -0,0 +1,34 @@ +\* TLC Model Configuration for SystemScheduler +\* Includes safety invariants and liveness (SystemCoverage) temporal property + +\* ---------- Constants ---------- +CONSTANT Nodes = {n1, n2} +CONSTANT Jobs = {j1, j2} + +CONSTANT Attrs = [ n1 |-> [zone |-> "us", cores |-> 2], + n2 |-> [zone |-> "eu", cores |-> 1] ] + +CONSTANT Capacity = [ c1 |-> 2, + c2 |-> 1 ] + +CONSTANT Demand = [ j1 |-> 1, + j2 |-> 1 ] + +CONSTANT ConstraintFn = "lambda j, a: a.zone = 'us'" +CONSTANT ScoreFn = "lambda j, a: IF j = j1 THEN a.cores ELSE a.cores - 1" + +\* ---------- Safety Invariants ---------- +Inv +CapacitySafety +AllocRange + +\* ---------- Temporal Properties ---------- +SystemCoverage + +\* ---------- Fairness ---------- +WF_vars(Next) + +\* ---------- Notes ---------- +\* - SystemCoverage checks that every eligible client eventually receives allocations for all jobs. +\* - Weak fairness ensures the placement action is eventually executed. +\* - Adjust Clients, Jobs, Capacity, Demand, Attrs for larger tests. diff --git a/scheduler/spec/system/SystemScheduler.tla b/scheduler/spec/system/SystemScheduler.tla new file mode 100644 index 00000000000..8fb7451c2ea --- /dev/null +++ b/scheduler/spec/system/SystemScheduler.tla @@ -0,0 +1,152 @@ +------------------------- MODULE SystemScheduler ------------------------- +EXTENDS Naturals, Sequences, FiniteSets, TLC + +\* ---------- Constants (to be set in TLC) ---------- +CONSTANT + Nodes, \* finite set of nodes + Jobs, \* finite set of job identifiers + Attrs, \* Attrs is a function Nodes -> attribute record (abstract) + Capacity, \* Capacity is a function Nodes -> Nat + Demand, \* Demand is a function Jobs -> Nat + ConstraintFn, \* ConstraintFn(job, attr) -> BOOLEAN + ScoreFn \* ScoreFn(job, attr) -> Nat + +\* ---------- Helper sets ---------- +NodeSet == Nodes +JobSet == Jobs + +VARIABLE + eligibleNodes, \* subset of Nodes that are currently eligible + allocs, \* allocs[j][n] = 0/1 indicating allocation of job j on node n + currentJobs \* subset of Jobs that exist (allows job add/remove) + +\* Initialize variables +Init == + /\ eligibleNodes = Nodes + /\ currentJobs = Jobs + /\ allocs = [j \in Jobs |-> [n \in Nodes |-> 0]] + +\* Used capacity on client c +RECURSIVE Sum(_) +Sum(S) == IF S = {} THEN 0 ELSE + LET x == CHOOSE y \in S: TRUE IN x + Sum(S \ { x }) + +UsedCap(c) == Sum({ allocs[j][c] * Demand[j] : j \in currentJobs }) + +\* Whether job j can run on node n (constraints + capacity + presence) +Eligible(j,n) == + /\ n \in eligibleNodes + /\ j \in currentJobs + /\ ConstraintFn[j][Attrs[n]] + /\ allocs[j][n] = 0 + /\ UsedCap(n) + Demand[j] <= Capacity[n] + +\* Safety: no node exceeds capacity +CapacitySafety == + \A n \in Nodes: UsedCap(n) <= Capacity[n] + +\* Safety: allocs are only 0 or 1 +AllocRange == + \A j \in Jobs: \A n \in Nodes: allocs[j][n] \in {0, 1} + +\* Desired coverage (for system jobs): for every job, every eligible client should have alloc=1 +\* SystemCoverage == +\* \A j \in currentJobs: \A c \in eligibleNodes: +\* (ConstraintFn[j][Attrs[c]] /\ (UsedCap(c) + Demand[j] <= Capacity[c])) +\* => allocs[j][c] = 1 + +SystemCoverage == + <> (\A j \in curentJobs: \A c \in eligibleNodes: + Eligible(j,c) => allocs[j][c] = 1) + +\* Choose the best eligible (job,client) pair. +\* To be deterministic for TLC, we break ties by lexicographic order (smallest job then smallest client). +BestPairExists == + \E j \in currentJobs, c \in eligibleNodes: Eligible(j,c) + +BestPair(j,c) == + /\ Eligible(j,c) + /\ \A jb \in currentJobs, cb \in eligibleNodes: + Eligible(jb,cb) => + ( ScoreFn[j][Attrs[c]] > ScoreFn[jb][Attrs[cb]] + \/ (ScoreFn[j][Attrs[c]] = ScoreFn[jb][Attrs[cb]] + /\ (j < jb \/ (j = jb /\ c <= cb))) + ) + +\* ---------- PlusCal algorithm (inside comment block) ---------- +(* +--algorithm MultiJobScheduler +variables + eligibleNodes = Nodes; + currentJobs = Jobs; + allocs = [j \in Jobs |-> [n \in Nodes |-> 0]]; + +define + UsedCap(c) == \sum_{j \in currentJobs} (allocs[j][c] * Demand[j]); + Eligible(j,c) == (c \in eligibleNodes) /\ (j \in currentJobs) + /\ ConstraintFn(j, Attrs[c]) + /\ (allocs[j][c] = 0) + /\ (UsedCap(c) + Demand[j] <= Capacity[c]); + + Score(j,c) == ScoreFn(j, Attrs[c]); +end define; + +begin +MainLoop: + while TRUE do + either \* Place allocation on best eligible (job, node) pair + if (\E j \in currentJobs, c \in eligibleNodes: Eligible(j,c)) then + \* choose lexicographically smallest best pair to be deterministic in TLC + with jb \in currentJobs do + with nb \in eligibleNodes do + if BestPair(jb,nb) then + allocs[jb][nb] := 1; + end if; + end with; + end with; + end if; + + or \* Client joins + with n \in Nodes do + if n \notin eligibleNodes then + eligibleNodes := eligibleNodes \cup {n}; + end if; + end with; + + or \* Client leaves (evict all allocs on that client) + with n \in eligibleNodes do + eligibleNodes := eligibleNodes \ {n}; + \* free all allocations on that node + with j \in Jobs do + allocs[j][n] := 0; + end with; + end with; + + or \* Job added + with j \in Jobs do + if j \notin currentJobs then + currentJobs := currentJobs \cup {j}; + end if; + end with; + + or \* Job removed (evict all allocations of that job) + with j \in currentJobs do + currentJobs := currentJobs \ {j}; + with n \in Nodes do + allocs[j][n] := 0; + end with; + end with; + end either; + end while; +end algorithm; +*) + +\* ---------- Helpful invariants to check with TLC ---------- +Inv == + /\ AllocRange + /\ CapacitySafety + /\ \A j \in currentJobs, c \in eligibleNodes: + allocs[j][n] = 1 => ConstraintFn[j][Attrs[n]] + /\ \A j \in currentJobs, n \in Nodes: allocs[j][n] = 1 => n \in eligibleNodes + +============================================================================= From 033c985bfd42a9dc129a01d69cf7be593fabb5f9 Mon Sep 17 00:00:00 2001 From: Piotr Kazmierczak <470696+pkazmierczak@users.noreply.github.com> Date: Fri, 28 Nov 2025 17:37:31 +0100 Subject: [PATCH 2/4] pluscal sucks --- scheduler/spec/system/SystemScheduler.tla | 110 ++++++++-------------- 1 file changed, 41 insertions(+), 69 deletions(-) diff --git a/scheduler/spec/system/SystemScheduler.tla b/scheduler/spec/system/SystemScheduler.tla index 8fb7451c2ea..bf729e8c67a 100644 --- a/scheduler/spec/system/SystemScheduler.tla +++ b/scheduler/spec/system/SystemScheduler.tla @@ -56,7 +56,7 @@ AllocRange == \* => allocs[j][c] = 1 SystemCoverage == - <> (\A j \in curentJobs: \A c \in eligibleNodes: + <> (\A j \in currentJobs: \A c \in eligibleNodes: Eligible(j,c) => allocs[j][c] = 1) \* Choose the best eligible (job,client) pair. @@ -73,79 +73,51 @@ BestPair(j,c) == /\ (j < jb \/ (j = jb /\ c <= cb))) ) -\* ---------- PlusCal algorithm (inside comment block) ---------- -(* ---algorithm MultiJobScheduler -variables - eligibleNodes = Nodes; - currentJobs = Jobs; - allocs = [j \in Jobs |-> [n \in Nodes |-> 0]]; - -define - UsedCap(c) == \sum_{j \in currentJobs} (allocs[j][c] * Demand[j]); - Eligible(j,c) == (c \in eligibleNodes) /\ (j \in currentJobs) - /\ ConstraintFn(j, Attrs[c]) - /\ (allocs[j][c] = 0) - /\ (UsedCap(c) + Demand[j] <= Capacity[c]); - - Score(j,c) == ScoreFn(j, Attrs[c]); -end define; - -begin -MainLoop: - while TRUE do - either \* Place allocation on best eligible (job, node) pair - if (\E j \in currentJobs, c \in eligibleNodes: Eligible(j,c)) then - \* choose lexicographically smallest best pair to be deterministic in TLC - with jb \in currentJobs do - with nb \in eligibleNodes do - if BestPair(jb,nb) then - allocs[jb][nb] := 1; - end if; - end with; - end with; - end if; - - or \* Client joins - with n \in Nodes do - if n \notin eligibleNodes then - eligibleNodes := eligibleNodes \cup {n}; - end if; - end with; - - or \* Client leaves (evict all allocs on that client) - with n \in eligibleNodes do - eligibleNodes := eligibleNodes \ {n}; - \* free all allocations on that node - with j \in Jobs do - allocs[j][n] := 0; - end with; - end with; - - or \* Job added - with j \in Jobs do - if j \notin currentJobs then - currentJobs := currentJobs \cup {j}; - end if; - end with; - - or \* Job removed (evict all allocations of that job) - with j \in currentJobs do - currentJobs := currentJobs \ {j}; - with n \in Nodes do - allocs[j][n] := 0; - end with; - end with; - end either; - end while; -end algorithm; -*) +\* Actual scheduling algorithm model +vars == << eligibleNodes, currentJobs, allocs >> + +Next == \/ /\ IF (\E j \in currentJobs, c \in eligibleNodes: Eligible(j,c)) + THEN /\ \E jb \in currentJobs: + \E nb \in eligibleNodes: + IF BestPair(jb,nb) + THEN /\ allocs' = [allocs EXCEPT ![jb][nb] = 1] + ELSE /\ TRUE + /\ UNCHANGED allocs + ELSE /\ TRUE + /\ UNCHANGED allocs + /\ UNCHANGED <> + \/ /\ \E n \in Nodes: + IF n \notin eligibleNodes + THEN /\ eligibleNodes' = (eligibleNodes \cup {n}) + ELSE /\ TRUE + /\ UNCHANGED eligibleNodes + /\ UNCHANGED <> + \/ /\ \E n \in eligibleNodes: + /\ eligibleNodes' = eligibleNodes \ {n} + /\ \E j \in Jobs: + allocs' = [allocs EXCEPT ![j][n] = 0] + /\ UNCHANGED currentJobs + \/ /\ \E j \in Jobs: + IF j \notin currentJobs + THEN /\ currentJobs' = (currentJobs \cup {j}) + ELSE /\ TRUE + /\ UNCHANGED currentJobs + /\ UNCHANGED <> + \/ /\ \E j \in currentJobs: + /\ currentJobs' = currentJobs \ {j} + /\ \E n \in Nodes: + allocs' = [allocs EXCEPT ![j][n] = 0] + /\ UNCHANGED eligibleNodes + +Spec == Init /\ [][Next]_vars + +\* END TRANSLATION \* ---------- Helpful invariants to check with TLC ---------- Inv == /\ AllocRange /\ CapacitySafety - /\ \A j \in currentJobs, c \in eligibleNodes: + /\ \A j \in currentJobs, n \in eligibleNodes: allocs[j][n] = 1 => ConstraintFn[j][Attrs[n]] /\ \A j \in currentJobs, n \in Nodes: allocs[j][n] = 1 => n \in eligibleNodes From 9a3bd1d3fd49f68b978060b827943a5cbcd8ed15 Mon Sep 17 00:00:00 2001 From: Piotr Kazmierczak <470696+pkazmierczak@users.noreply.github.com> Date: Mon, 1 Dec 2025 08:51:58 +0100 Subject: [PATCH 3/4] reorg of cfg files --- scheduler/spec/system/SystemCoverageWF.cfg | 26 +++++++++++++++++ scheduler/spec/system/SystemCoverageWF.tla | 20 +++++++++++++ scheduler/spec/system/SystemScheduler.cfg | 34 ---------------------- scheduler/spec/system/SystemScheduler.tla | 12 ++++---- 4 files changed, 51 insertions(+), 41 deletions(-) create mode 100644 scheduler/spec/system/SystemCoverageWF.cfg create mode 100644 scheduler/spec/system/SystemCoverageWF.tla delete mode 100644 scheduler/spec/system/SystemScheduler.cfg diff --git a/scheduler/spec/system/SystemCoverageWF.cfg b/scheduler/spec/system/SystemCoverageWF.cfg new file mode 100644 index 00000000000..396b2659571 --- /dev/null +++ b/scheduler/spec/system/SystemCoverageWF.cfg @@ -0,0 +1,26 @@ +\* TLC Model Configuration for SystemScheduler +\* Includes safety invariants and liveness (SystemCoverage) temporal property + +\* ---------- Constants ---------- + +CONSTANT + Nodes <- NodesValue + Jobs <- JobsValue + Attrs <- AttrsValue + Capacity <- CapacityValue + Demand <- DemandValue + ConstraintFn <- ConstraintFnValue + ScoreFn <- ScoreFnValue + + +\* ---------- Safety Invariants ---------- +INVARIANT + Inv + CapacitySafety + AllocRange + +\* ---------- Temporal Properties ---------- +PROPERTY SystemCoverage + +\* ---------- Fairness ---------- +PROPERTY WF_vars(Next) diff --git a/scheduler/spec/system/SystemCoverageWF.tla b/scheduler/spec/system/SystemCoverageWF.tla new file mode 100644 index 00000000000..6fa86cbb13f --- /dev/null +++ b/scheduler/spec/system/SystemCoverageWF.tla @@ -0,0 +1,20 @@ +---- MODULE SystemCoverageWF ---- +EXTENDS SystemScheduler + +NodesValue == { "n1", "n2" } +JobsValue == { "j1", "j2" } + +AttrsValue == [ + n1 |-> [ dc |-> "us", cores |-> 2 ], + n2 |-> [ dc |-> "eu", cores |-> 1 ] +] + +CapacityValue == [ c1 |-> 2, c2 |-> 1 ] + +DemandValue == [ j1 |-> 1, j2 |-> 1 ] + +ConstraintFnValue(a) == a.dc = "us" + +ScoreFnValue(j, a) == IF j = "j1" THEN a.cores ELSE a.cores - 1 + +==== \ No newline at end of file diff --git a/scheduler/spec/system/SystemScheduler.cfg b/scheduler/spec/system/SystemScheduler.cfg deleted file mode 100644 index 53f08fecd3e..00000000000 --- a/scheduler/spec/system/SystemScheduler.cfg +++ /dev/null @@ -1,34 +0,0 @@ -\* TLC Model Configuration for SystemScheduler -\* Includes safety invariants and liveness (SystemCoverage) temporal property - -\* ---------- Constants ---------- -CONSTANT Nodes = {n1, n2} -CONSTANT Jobs = {j1, j2} - -CONSTANT Attrs = [ n1 |-> [zone |-> "us", cores |-> 2], - n2 |-> [zone |-> "eu", cores |-> 1] ] - -CONSTANT Capacity = [ c1 |-> 2, - c2 |-> 1 ] - -CONSTANT Demand = [ j1 |-> 1, - j2 |-> 1 ] - -CONSTANT ConstraintFn = "lambda j, a: a.zone = 'us'" -CONSTANT ScoreFn = "lambda j, a: IF j = j1 THEN a.cores ELSE a.cores - 1" - -\* ---------- Safety Invariants ---------- -Inv -CapacitySafety -AllocRange - -\* ---------- Temporal Properties ---------- -SystemCoverage - -\* ---------- Fairness ---------- -WF_vars(Next) - -\* ---------- Notes ---------- -\* - SystemCoverage checks that every eligible client eventually receives allocations for all jobs. -\* - Weak fairness ensures the placement action is eventually executed. -\* - Adjust Clients, Jobs, Capacity, Demand, Attrs for larger tests. diff --git a/scheduler/spec/system/SystemScheduler.tla b/scheduler/spec/system/SystemScheduler.tla index bf729e8c67a..6f974eb27ba 100644 --- a/scheduler/spec/system/SystemScheduler.tla +++ b/scheduler/spec/system/SystemScheduler.tla @@ -1,17 +1,15 @@ -------------------------- MODULE SystemScheduler ------------------------- +---- MODULE SystemScheduler ---- EXTENDS Naturals, Sequences, FiniteSets, TLC -\* ---------- Constants (to be set in TLC) ---------- CONSTANT Nodes, \* finite set of nodes Jobs, \* finite set of job identifiers Attrs, \* Attrs is a function Nodes -> attribute record (abstract) Capacity, \* Capacity is a function Nodes -> Nat Demand, \* Demand is a function Jobs -> Nat - ConstraintFn, \* ConstraintFn(job, attr) -> BOOLEAN + ConstraintFn, \* ConstraintFn(attr) -> BOOLEAN ScoreFn \* ScoreFn(job, attr) -> Nat -\* ---------- Helper sets ---------- NodeSet == Nodes JobSet == Jobs @@ -37,7 +35,7 @@ UsedCap(c) == Sum({ allocs[j][c] * Demand[j] : j \in currentJobs }) Eligible(j,n) == /\ n \in eligibleNodes /\ j \in currentJobs - /\ ConstraintFn[j][Attrs[n]] + /\ ConstraintFn[Attrs[n]] /\ allocs[j][n] = 0 /\ UsedCap(n) + Demand[j] <= Capacity[n] @@ -118,7 +116,7 @@ Inv == /\ AllocRange /\ CapacitySafety /\ \A j \in currentJobs, n \in eligibleNodes: - allocs[j][n] = 1 => ConstraintFn[j][Attrs[n]] + allocs[j][n] = 1 => ConstraintFn[Attrs[n]] /\ \A j \in currentJobs, n \in Nodes: allocs[j][n] = 1 => n \in eligibleNodes -============================================================================= +==== From a2b974f514f0861b2e41082045a713ba4e91c849 Mon Sep 17 00:00:00 2001 From: Piotr Kazmierczak <470696+pkazmierczak@users.noreply.github.com> Date: Wed, 3 Dec 2025 10:47:45 +0100 Subject: [PATCH 4/4] corrections (like the Jonathan Franzen novel) --- scheduler/spec/system/SystemCoverageWF.cfg | 4 ++-- scheduler/spec/system/SystemCoverageWF.tla | 4 ++-- scheduler/spec/system/SystemScheduler.tla | 27 +++++++++++----------- 3 files changed, 17 insertions(+), 18 deletions(-) diff --git a/scheduler/spec/system/SystemCoverageWF.cfg b/scheduler/spec/system/SystemCoverageWF.cfg index 396b2659571..d138415da78 100644 --- a/scheduler/spec/system/SystemCoverageWF.cfg +++ b/scheduler/spec/system/SystemCoverageWF.cfg @@ -22,5 +22,5 @@ INVARIANT \* ---------- Temporal Properties ---------- PROPERTY SystemCoverage -\* ---------- Fairness ---------- -PROPERTY WF_vars(Next) +INIT Init +NEXT Next \ No newline at end of file diff --git a/scheduler/spec/system/SystemCoverageWF.tla b/scheduler/spec/system/SystemCoverageWF.tla index 6fa86cbb13f..afc0fd9739b 100644 --- a/scheduler/spec/system/SystemCoverageWF.tla +++ b/scheduler/spec/system/SystemCoverageWF.tla @@ -9,12 +9,12 @@ AttrsValue == [ n2 |-> [ dc |-> "eu", cores |-> 1 ] ] -CapacityValue == [ c1 |-> 2, c2 |-> 1 ] +CapacityValue == [ n1 |-> 2, n2 |-> 1 ] DemandValue == [ j1 |-> 1, j2 |-> 1 ] ConstraintFnValue(a) == a.dc = "us" -ScoreFnValue(j, a) == IF j = "j1" THEN a.cores ELSE a.cores - 1 +ScoreFnValue(j,a) == IF j = "j1" THEN a.cores ELSE a.cores - 1 ==== \ No newline at end of file diff --git a/scheduler/spec/system/SystemScheduler.tla b/scheduler/spec/system/SystemScheduler.tla index 6f974eb27ba..f484f499095 100644 --- a/scheduler/spec/system/SystemScheduler.tla +++ b/scheduler/spec/system/SystemScheduler.tla @@ -2,13 +2,13 @@ EXTENDS Naturals, Sequences, FiniteSets, TLC CONSTANT - Nodes, \* finite set of nodes - Jobs, \* finite set of job identifiers - Attrs, \* Attrs is a function Nodes -> attribute record (abstract) - Capacity, \* Capacity is a function Nodes -> Nat - Demand, \* Demand is a function Jobs -> Nat - ConstraintFn, \* ConstraintFn(attr) -> BOOLEAN - ScoreFn \* ScoreFn(job, attr) -> Nat + Nodes, \* finite set of nodes + Jobs, \* finite set of job identifiers + Attrs, \* Attrs is a function Nodes -> attribute record (abstract) + Capacity, \* Capacity is a function Nodes -> Nat + Demand, \* Demand is a function Jobs -> Nat + ConstraintFn(_), \* ConstraintFn(attr) -> BOOLEAN + ScoreFn(_,_) \* ScoreFn(job, attr) -> Nat NodeSet == Nodes JobSet == Jobs @@ -35,7 +35,7 @@ UsedCap(c) == Sum({ allocs[j][c] * Demand[j] : j \in currentJobs }) Eligible(j,n) == /\ n \in eligibleNodes /\ j \in currentJobs - /\ ConstraintFn[Attrs[n]] + /\ ConstraintFn(Attrs[n]) /\ allocs[j][n] = 0 /\ UsedCap(n) + Demand[j] <= Capacity[n] @@ -58,7 +58,8 @@ SystemCoverage == Eligible(j,c) => allocs[j][c] = 1) \* Choose the best eligible (job,client) pair. -\* To be deterministic for TLC, we break ties by lexicographic order (smallest job then smallest client). +\* To be deterministic for TLC, we break ties by lexicographic order (smallest +\* job then smallest client). BestPairExists == \E j \in currentJobs, c \in eligibleNodes: Eligible(j,c) @@ -66,8 +67,8 @@ BestPair(j,c) == /\ Eligible(j,c) /\ \A jb \in currentJobs, cb \in eligibleNodes: Eligible(jb,cb) => - ( ScoreFn[j][Attrs[c]] > ScoreFn[jb][Attrs[cb]] - \/ (ScoreFn[j][Attrs[c]] = ScoreFn[jb][Attrs[cb]] + ( ScoreFn(j, Attrs[c]) > ScoreFn(jb, Attrs[cb]) + \/ (ScoreFn(j, Attrs[c]) = ScoreFn(jb, Attrs[cb]) /\ (j < jb \/ (j = jb /\ c <= cb))) ) @@ -109,14 +110,12 @@ Next == \/ /\ IF (\E j \in currentJobs, c \in eligibleNodes: Eligible(j,c)) Spec == Init /\ [][Next]_vars -\* END TRANSLATION - \* ---------- Helpful invariants to check with TLC ---------- Inv == /\ AllocRange /\ CapacitySafety /\ \A j \in currentJobs, n \in eligibleNodes: - allocs[j][n] = 1 => ConstraintFn[Attrs[n]] + allocs[j][n] = 1 => ConstraintFn(Attrs[n]) /\ \A j \in currentJobs, n \in Nodes: allocs[j][n] = 1 => n \in eligibleNodes ====