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.