A short note on composition in TLA+

------ MODULE Queue ------

EXTENDS Sequences, TLC, Integers, FiniteSets

CONSTANTS QueueId

RECURSIVE ReplaceInQueueDataInner(_,_,_,_)

OUTQUEUE == 1
OUT_I == 2
LOCAL_DATA == 3
TMPQ == 4
TMPOUT == 5

ReplaceInQueueDataInner(N,V,Val,Vec) ==
IF N = V
THEN <<Val>> \o Tail(Vec)
ELSE <<Vec[1]>> \o ReplaceInQueueDataInner(N+1,V,Val,Tail(Vec))

ReplaceInQueueData(V,Val,Vec) == ReplaceInQueueDataInner(1,V,Val,Vec)

InitQueueState == << << >>, 0, << >>, {}, << >> >>

\* incoming message format is <<cmd,sender,...>
\* where cmd is
\*
\* 0 - erase my output
\* 1 - enqueue for recipient
(*--algorithm queue

variables
inqueue, \* ordered messages in
out = {}, \* repository for live

queue_data = InitQueueState

process QueueRunner = QueueId

begin
ServiceInputs:
while TRUE do
ContinueQueueService:
print(222000);
await inqueue /= << >>;

print(222001);
queue_data := ReplaceInQueueData(LOCAL_DATA, Head(inqueue), queue_data);

print(222002);
inqueue := Tail(inqueue);

\* Remove output for this target.
if queue_data[LOCAL_DATA][1] = 0 then
print(222004);
out := out \ {(CHOOSE x \in out: x[1] = queue_data[LOCAL_DATA][2])};
else
SendQueuedData:
print(222003);
print(queue_data[LOCAL_DATA]);
queue_data := ReplaceInQueueData(OUTQUEUE, Append(queue_data[OUTQUEUE], Tail(queue_data[LOCAL_DATA])), queue_data);
end if;

\* Try to place new outputs
ResetTmpq:
print(222005);
queue_data := ReplaceInQueueData(TMPQ, {}, queue_data);
ResetOutI:
queue_data := ReplaceInQueueData(OUT_I, 1, queue_data);

StartDequeue:
while queue_data[OUT_I] <= Len(queue_data[OUTQUEUE]) do
ContinuqDequeue:
if {o \in out: o[1] = queue_data[OUTQUEUE][queue_data[OUT_I]][1]} = {} then
queue_data := ReplaceInQueueData(TMPQ, queue_data[TMPQ] \union {queue_data[OUT_I]}, queue_data);
out := out \union {queue_data[OUTQUEUE][queue_data[OUT_I]]};
end if;
IncOutI:
queue_data := ReplaceInQueueData(OUT_I, queue_data[OUT_I] + 1, queue_data);
end while;

print(222006);
\* Erase dequeued entries
queue_data := ReplaceInQueueData(TMPOUT, << >>, queue_data);
ResetOutI2:
queue_data := ReplaceInQueueData(OUT_I, 1, queue_data);

StartFixup:
while queue_data[OUT_I] <= Len(queue_data[OUTQUEUE]) do
ContinueFixup:
if {i \in queue_data[TMPQ]: i = queue_data[OUT_I]} = {} then
queue_data := ReplaceInQueueData(TMPOUT, Append(queue_data[TMPOUT], queue_data[OUTQUEUE][queue_data[OUT_I]]), queue_data);
end if;
IncOutI2:
queue_data := ReplaceInQueueData(OUT_I, queue_data[OUT_I] + 1, queue_data);
end while;

queue_data := ReplaceInQueueData(OUTQUEUE, queue_data[TMPOUT], queue_data);

end while;

end process;

end algorithm;*)
\*snip
====
----- MODULE QueueProducer -----

EXTENDS FiniteSets, Sequences, Integers

CONSTANT ProcessId, TargetId

(*--algorithm producer

process Producer = ProcessId
variables
inqueue,
out = {}
begin
ProduceAMessageForConsumer:
inqueue := Append(inqueue, <<1, TargetId, "hithere">>);
end process;

end algorithm; --*)
\* snip

=====
----- MODULE QueueConsumer -----
EXTENDS TLC, Sequences, FiniteSets

CONSTANT ProcessId

(*--algorithm consumer

process Consumer = ProcessId
variables
inqueue,
myitem,
out = {}
begin
AwaitQueueItemForMe:
print(444000);
await {x \in out: x[1] = ProcessId} /= {};
GotItemTakeIt:
print(444001);
myitem := CHOOSE x \in out: x[1] = ProcessId;
ShowItem:
print(myitem);
RetireMyQueueOutput:
inqueue := Append(inqueue, <<0, ProcessId>>);
end process;

end algorithm;--*)
\* snip

=====
  • Variables that are initialized to values other than our defaultInitValue must be preinitialized at the level above, otherwise initial setup will fail.
  • The parent module ultimately instantiates _every_ piece of state used by each subset, so things like queue_data in Queue allow utilities to shorten that complexity to just one state variable and their formal inputs and outputs, but it all needs to be visible to the consumer.
  • Since these runnable parts of the spec are distinct subsets of the state space, we’ll get messages like “Next is never enabled” from TLA+ if we don’t describe to TLA+ exactly what we want; that each INSTANCE’ Next rule is evaluated distinct from the others (\/ “or”) at the top level, and that each contains UNCHANGED rules for all the variables that belong to state it _isn’t_ involved in.
  • pluscal uses a “pc” variable to drive the state machine. We must provide working space for it for each instance.
------ MODULE Test -------
EXTENDS Naturals, TLC, Sequences

VARIABLES inqueue, out, queue_pc, queue_data, producer_pc, consumer_pc, consumer_item

Producer == INSTANCE QueueProducer WITH ProcessId <- 2, TargetId <- 3, inqueue <- inqueue, out <- out, pc <- producer_pc, defaultInitValue <- << >>
Consumer == INSTANCE QueueConsumer WITH ProcessId <- 3, pc <- consumer_pc, myitem <- consumer_item, defaultInitValue <- << >>
Queue == INSTANCE Queue WITH QueueId <- 1, inqueue <- inqueue, out <- out, pc <- queue_pc, queue_data <- queue_data, defaultInitValue <- << >>

Init == out = {} /\ Queue!Init /\ Producer!Init /\ Consumer!Init

Next ==
\/ (Queue!Next /\ UNCHANGED << producer_pc, consumer_pc, consumer_item >>)
\/ (Producer!Next /\ UNCHANGED << queue_data, queue_pc, consumer_pc, consumer_item >>)
\/ (Consumer!Next /\ UNCHANGED << queue_data, queue_pc, producer_pc >>)

=====

--

--

--

An old programmer learning new tricks.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

GMAT, GRE Functions and Graphing Question

GMAT, GRE, QUANT, quantitative, math, test prep, functions

dbt Orchestration in Azure DevOps Pipelines

Scaling Performance of DNN Inference in FPGA clusters using InAccel orchestrator

[Part 2] Delivering a Unified Omnichannel Experience using Headless Commerce

How to deploy django app on heroku for free

How low code helps software developers embrace rapid change

Conway’s Game of Life (in Ruby)

Another story about microservices: Hexagonal Architecture

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
art yerkes

art yerkes

An old programmer learning new tricks.

More from Medium

“She Waved at Me”

CS373 Spring 2022: Scarlett Shires, Week 2

Language and Culture: The Creolization of Sheng