law fixed_rate_skip

bend-kit-scheduler@0.4.1.0 · recurrence_laws.bend:17

import bend-kit-scheduler@0.4.1.0/recurrence_laws.bend as RecurrenceLaws
import Base
import bend-kit-scheduler@0.4.1.0/recurrence.bend as R

17# These equations specify named policies, phase anchoring, and exact replay prefix.
18law fixed_rate_skip:
19  for +previous: Nat
20  for +completion: Nat
21  for +p: Nat
22  {R.plan(previous, completion, 1n+p, R.FixedRate{R.Skip{}}) ==
23    Some{R.Planned{Nil{}, Nat.add(previous,
24      Nat.mul(1n+Nat.div(Nat.sub(completion, previous), 1n+p), 1n+p))}}
25    : Maybe<&2, R.Plan>}

Uses (11)

Used by (0)

No other definition uses this definition.