[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Time-outs

thanks very much, this helps a lot

On Tuesday, September 24, 2019 at 10:22:32 PM UTC+1, Andrew Helwer wrote:
To expand on Stephan's point with an example, the spec might look as follows:

Next ==
    \/ ReceiveMessage
    \/ Timeout
    \/ ...

Where ReceiveMessage is enabled if a message has been delivered, while Timeout is enabled if no message has yet been delivered. Then your spec will cover the following behaviours:

(Message sent) -> (Message delivered) -> (Message received & processed)
(Message sent) -> (Receiver timeout) -> (Message delivered)
(Message sent) -> (Receiver timeout)

(In the final behaviour, the message is never delivered)

Which are probably all the behaviors you want to model in your system, if you have special timeout-handling logic which safety you want to assess.


On Saturday, September 21, 2019 at 9:16:07 AM UTC-7, Theorem wrote:
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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a2bebae8-63d8-46c9-9bb9-7381b7f41970%40googlegroups.com.