Hi,
I am starting to play around with TLA+ and specifically PlusCal.
I am attempting to model a replication protocol, and part of the protocol includes a replica sending a message to all other replicas.
I have an ordered inbound queue for each replica defined as:
pending_messages = [r \in 1..total_replicas |-> <<>>];
and my sending loop is:
i:=0
while (i <= total_replicas) do
if i \in OtherReplicas(self) then
pending_messages[i] := pending_messages[i] \o <<message>>;
end if;
i := i + 1;
end while;
The issue I am seeing is an explosion of states. by defining all the message channels as separate variables as so:
pending_messages_1 = <<>>;
pending_messages_2 = <<>>;
pending_messages_3 = <<>>;
pending_messages_4 = <<>>
and
if self /= 1 /\ Replicas >= 1 then
pending_messages_1 := pending_messages_1 \o <<message>>;
end if;
if self /= 2 /\ Replicas >= 2 then
pending_messages_2 := pending_messages_2 \o <<message>>;
end if;
if self /= 3 /\ Replicas >= 3 then
pending_messages_3 := pending_messages_3 \o <<message>>;
end if;
if self /= 4 /\ Replicas >= 4 then
pending_messages_4 := pending_messages_4 \o <<message>>;
end if;
assert self < 5;
This is not ideal as it means I cannot have a variable that states I want to have 9 replicas.
So my question is the following. Is there are way to append something like I did with the while loop but having the all the appends occur in a single "atomic" operation.