[tlaplus] Model network using set or bag

[Alberto Carretero <angelalbertoc.r@xxxxxxxxx>]

I see several discussions here on the topic of message passing or atomic communication but I have not found any on which representation is best for message passing and I wonder if there is a standard way, or at least, one that is better for TLC.

In general I see that there are two different possibilities. There are several specs like PaxosMadeSimple[1] that use a set of all the messages ever sent. Duplicates do not need to be modeled specifically as messages are never deleted and message loss is equivalent to never receiving the message. There is even a comment written presumably by Lamport in the spec that states:

> (* The algorithm is easiest to understand in terms of the set msgs of all  *)
  (* messages that have ever been sent.  A more accurate model would use one *)
  (* or more variables to represent the messages actually in transit, and it *)
  (* would include actions representing message loss and duplication as well *)
  (* as message receipt.                                                     *)

I read "more accurate" as closer to a real implementation but not necessarily more expressive as I think that all the safety properties can also be modeled using a set. Is that right?

Now, on the other hand we have specs such as Raft[2][3] that use a bag of messages to model the network (correspondence between msg and count). Duplicates are handled by incrementing the count and drops by decrementing it. To me, this representation should be much less performant when model checking in TLC as each duplicate / drop changes the state and can be interleaved with any other action. Even if the network is constrained to disallow duplicates, more states will be generated compared to the set as messages can be received by the destination and then resent by the sender; effectively duplicating the number of generated states.

At this point, it looks to me like using a set would be preferred in general, but then I see most specs preferring a bag. What am I missing? Are there any other advantages? Or maybe sets are more efficient but the effect is not meaningful enough.

[1]: https://github.com/tlaplus/tlaplus/blob/master/general/performance/PaxosMadeSimple/PaxosMadeSimple.tla
[2]: https://github.com/ongardie/raft.tla
[3]: https://github.com/etcd-io/raft/blob/main/tla/etcdraft.tla

-- 
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 visit https://groups.google.com/d/msgid/tlaplus/fa267fbb-f81c-4739-9801-5c5f9852da41n%40googlegroups.com.