Re: [tlaplus] Appending to a collection of objects

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

On 24 Jul 2020, at 17:38, Hillel Wayne <hwayne@xxxxxxxxx> wrote:

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

On 7/24/2020 5:41 AM, shamis@xxxxxxxxx wrote:

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.

--
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/0eaf4b12-df56-19a7-c928-a892ec55d5e0%40gmail.com.

--
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/CBE6B7C1-985E-467D-866A-D41C74F1B10A%40gmail.com.