you may want to check a previous thread  about modeling timeouts.
The main question you should consider is if including clocks in your TLA+ model is necessary for the properties you wish to verify. Including clocks inevitably blows up your state space, and it may be enough to consider that an action triggered by a timeout may non-deterministically occur at any time during the execution. This is clearly an over-abstraction and may therefore lead to spurious counter-examples where the timeout occurs "too soon", but you can try to rule out those counter-examples by adding enabling conditions to your actions. (In particular, these conditions may refer to variables that are not visible to the process in the implementation of your system, they express global synchronization conditions that are ensured by the timers in your implementation.)
As for the handlers, I'd start simple and introduce detail when you've become confident with your spec. An initial model could use direct message passing between clients and servers, and you can add an indirection later on.
Hope this helps,
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/BEF22B9E-E280-4987-9E76-4D75C4792601%40gmail.com.