[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Appending to a collection of objects

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:

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 = <<>>


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.

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7dd7cd28-e341-4ca2-be89-3b12862dbc23o%40googlegroups.com.