Hi,
You can do this by assigning a new function, like this:
pending_messages := [r \in 1..total_replicas |->
IF r /= self
THEN Append(pending_messages[r], message)
ELSE pending_messages[r]
]
--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) doif i \in OtherReplicas(self) thenpending_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 thenpending_messages_1 := pending_messages_1 \o <<message>>;end if;if self /= 2 /\ Replicas >= 2 thenpending_messages_2 := pending_messages_2 \o <<message>>;end if;if self /= 3 /\ Replicas >= 3 thenpending_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.