Appending to a collection of objects

[sha...@gmail.com]

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.

[Hillel Wayne]

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7dd7cd28-e341-4ca2-be89-3b12862dbc23o%40googlegroups.com.

[Stephan Merz]

Also, you may want to consider if using (unordered) sets rather than sequences is sufficient for your protocol, as this would generate fewer distinct states.

However, it is unlikely that you will be able to check a significant protocol for 9 replicas. Since model checking exhaustively explores the state space and sees states that conventional testing would not be likely to encounter, model checking using 3 or 4 replicas can often give you good confidence that there are no remaining errors.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/0eaf4b12-df56-19a7-c928-a892ec55d5e0%40gmail.com.

[sha...@gmail.com]

Thank you Hillel that works perfectly.

Thank you for your suggestion Stephan, unfortunately I need to use the sequence as ordering matters for me. In fact the actual interleaving really matter for me so the correct solution would be to use the while loop variant that I original asked the question about. However, it blows up the state too much and I still have not specified the entire algorithm yet.

-Alex