BatchingProcessor.tla

---- MODULE BatchingProcessor ----
EXTENDS Sequences, Integers

CONSTANT BatchSize

(*--algorithm BatchingProcessor
variables
    batch = <<>>;
    flushTasks = <<>>;
    flushedBatchSizeHistory = {};
define
    BatchSizeBound == Len(batch) <= BatchSize
    BatchFlushSizeBound == \A x \in flushedBatchSizeHistory: x <= BatchSize
end define

process processor \in {"p0","p1"}
begin
p_i0:
    while TRUE do
p_i1:
        if Len(batch) >= BatchSize then
            flushTasks := Append(flushTasks, batch);
            batch := <<>>;
        end if;
p_i2:
        batch := Append(batch, 1)
    end while
end process

process flusher = "f"
begin
f_i0:
    while TRUE do
f_i1:
        await Len(flushTasks) > 0;
f_i2:
        flushedBatchSizeHistory := flushedBatchSizeHistory \cup {Len(Head(flushTasks))};
        flushTasks := Tail(flushTasks);
    end while
end process
end algorithm
*)
\* BEGIN TRANSLATION (chksum(pcal) = "dd4e3172" /\ chksum(tla) = "33df772a")
VARIABLES batch, flushTasks, flushedBatchSizeHistory, pc

(* define statement *)
BatchSizeBound == Len(batch) <= BatchSize
BatchFlushSizeBound == \A x \in flushedBatchSizeHistory: x <= BatchSize


vars == << batch, flushTasks, flushedBatchSizeHistory, pc >>

ProcSet == ({"p0","p1"}) \cup {"f"}

Init == (* Global variables *)
        /\ batch = <<>>
        /\ flushTasks = <<>>
        /\ flushedBatchSizeHistory = {}
        /\ pc = [self \in ProcSet |-> CASE self \in {"p0","p1"} -> "p_i0"
                                        [] self = "f" -> "f_i0"]

p_i0(self) == /\ pc[self] = "p_i0"
              /\ pc' = [pc EXCEPT ![self] = "p_i1"]
              /\ UNCHANGED << batch, flushTasks, flushedBatchSizeHistory >>

p_i1(self) == /\ pc[self] = "p_i1"
              /\ IF Len(batch) >= BatchSize
                    THEN /\ flushTasks' = Append(flushTasks, batch)
                         /\ batch' = <<>>
                    ELSE /\ TRUE
                         /\ UNCHANGED << batch, flushTasks >>
              /\ pc' = [pc EXCEPT ![self] = "p_i2"]
              /\ UNCHANGED flushedBatchSizeHistory

p_i2(self) == /\ pc[self] = "p_i2"
              /\ batch' = Append(batch, 1)
              /\ pc' = [pc EXCEPT ![self] = "p_i0"]
              /\ UNCHANGED << flushTasks, flushedBatchSizeHistory >>

processor(self) == p_i0(self) \/ p_i1(self) \/ p_i2(self)

f_i0 == /\ pc["f"] = "f_i0"
        /\ pc' = [pc EXCEPT !["f"] = "f_i1"]
        /\ UNCHANGED << batch, flushTasks, flushedBatchSizeHistory >>

f_i1 == /\ pc["f"] = "f_i1"
        /\ Len(flushTasks) > 0
        /\ pc' = [pc EXCEPT !["f"] = "f_i2"]
        /\ UNCHANGED << batch, flushTasks, flushedBatchSizeHistory >>

f_i2 == /\ pc["f"] = "f_i2"
        /\ flushedBatchSizeHistory' = (flushedBatchSizeHistory \cup {Len(Head(flushTasks))})
        /\ flushTasks' = Tail(flushTasks)
        /\ pc' = [pc EXCEPT !["f"] = "f_i0"]
        /\ batch' = batch

flusher == f_i0 \/ f_i1 \/ f_i2

Next == flusher
           \/ (\E self \in {"p0","p1"}: processor(self))

Spec == Init /\ [][Next]_vars

\* END TRANSLATION
====