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

[tlaplus] Appending to a collection of objects



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.

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