Re: [tlaplus] Time-outs

many thanks, this is what I was looking for. very helpful indeed. thanks

On Saturday, September 21, 2019 at 5:31:05 PM UTC+1, Stephan Merz wrote:

I'm assuming that you are not trying to verify any real-time properties of your protocol but that you are only interested in qualitative properties of a protocol that includes timeout actions intended to recover possible faults of the underlying network, such as by resending messages that may have been lost.

In that case, simply include the timeout action as a disjunct in the definition of the next-state relation. This means that the action can occur at any point in the protocol: timeout is modeled by non-determinism. You will probably want to include a precondition that implies that some action whose effect has been "lost" has indeed occurred previously. As a concrete example, have a look at the standard specification of the alternating bit protocol (which has timeout actions for resending lost messages).

The resulting specification is of course an over-approximation of the behavior of the actual protocol: if you can verify the properties that you are interested in, then the actual protocol (where the timeout action is more restricted) will be correct as well. If you find that the over-approximation is too coarse, you may have to add more preconditions. (Remember that as the writer of a specification you have access to the entire system state even if the implementation of a node in a distributed system only sees the local state of that node.) But I recommend to start simple and see how far you get.

Stephan

On 21 Sep 2019, at 18:16, Theorem <ibas...@xxxxxxxxx> wrote:

Hello
Is there a general way/guideline to model Timeouts in TLA+. e.g. in a message-passing network model, how can time-outs be modelled. In other words, should I consider time-out a fault? in fact, a more general question is that are Time-outs considered types of faults in a distributed system.

--
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 tla...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/36fe8213-63fc-47fc-86ea-bf15ba19a6f7%40googlegroups.com.