Hello Pedro,another unrelated issue with your specification concerns the choice of the response in action respondAgent: you write  LET r == CHOOSE x \in {"ok", "error"}: TRUE IN ...However, CHOOSE models deterministic (although arbitrary) choice, so r will either always equal "ok" or always equal "error". You certainly want the choice to be non-deterministic (i.e., both results may occur and will be explored by the model checker). You should therefore write  \E r \in {"ok", "error"} : ...Regards,StephanP.S.: What a strange idea to attach an RTF file produced from a TLA+ specification rather than the original module!On 10 Feb 2018, at 03:29, par...@xxxxxxxxx wrote:If you enable Deadlock checking, you'll see that the system deadlocks after a CRequest has taken place.For a CReply to take place, this enabling condition must be true:    /\ status[tasks[c].agent] \in {"ok", "error"}Looking at where you set to values for status, it happens in assignAgentsThe problem is in your first enabling condition in that action. You have:    /\ \A c \in Clients: LET a == tasks[c].agent But I think you meant that to be \E c \in Clients: ...When I changed it to use \E instead of \A, the model checker performed "as expected".I hope this helps!Jay P.-- 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+u...@xxxxxxxxxxxxxxxx.To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.Visit this group at https://groups.google.com/group/tlaplus.For more options, visit https://groups.google.com/d/optout.