[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.

Andrew

On Saturday, September 21, 2019 at 9:16:07 AM UTC-7, Theorem 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 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.