law pop_respects_limit

bend-kube-runtime@0.2.0.0 · LAWS.bend:154

import Base
import bend-kube-runtime@0.2.0.0/src/queue.bend as Q

154# No key starts while every worker slot is taken.
155law pop_respects_limit:
156  for f: List<&2, String>
157  for b: List<&2, String>
158  for inq: Map<&2, U32>
159  for run: Map<&2, U32>
160  for d: Map<&2, U32>
161  for g: Map<&2, U32>
162  for fl: Map<&2, U32>
163  for n: U32
164  for mx: U32
165  for full: {U32.is_lt(n, mx) == False{} : Bool}
166  {Q.Queue.pop(Q.Queue{f, b, inq, run, d, g, fl, n, mx})
167    == (Q.Queue{f, b, inq, run, d, g, fl, n, mx}, None{}) : Q.Queue & Maybe<&2, String>}