throttler.tla

-------------------------------- MODULE throttler --------------------------------
EXTENDS TLC, Integers, Sequences

MaxEpoch == 20
RequestLimit == 5
TimeSpan == 1

Min(seq) == 
  LET 
    ix == 1..Len(seq)
    i == CHOOSE x \in ix: \A y \in ix: seq[x] <= seq[y]
  IN seq[i]

TooManyRequests(seq, epoch) ==
  /\ Len(seq) >= RequestLimit
  /\ Min(seq) >= epoch - TimeSpan


CircularBufferAppend(seq, newElement) ==
  IF Len(seq) < RequestLimit
    THEN Append(seq, newElement)
    ELSE Tail(seq) \o <<newElement>>

(* --algorithm throttler
variables
    epoch = 0;
    mem = <<>>;
    ready = TRUE;
    revived = FALSE;

define 
  TypeOk == 
    /\ epoch \in 0..MaxEpoch 
    /\ \A i \in 1..Len(mem): mem[i] <= epoch

  RequestsEventuallyUnblock == ~ready ~> ~[]ready
end define;

fair+ process time = 0
begin
  Tick:
    while epoch < MaxEpoch do
      epoch := epoch + 1;
    end while;
end process;

fair+ process requests = 1
begin
  Request:
    while epoch < MaxEpoch do
      if TooManyRequests(mem, epoch) then
        Wait:
          ready := FALSE;
      else
        Act:
          ready := TRUE;
          mem := CircularBufferAppend(mem, epoch);
      end if;
    end while;
end process;
end algorithm; *)