Hello Pedro,another unrelated issue with your specification concerns the choice of the response in action respondAgent: you writeLET 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 `assignAgents`
The 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+unsubscribe@googlegroups.com .
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 .--
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@googlegroups.com .
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 .