# Re: [tlaplus] Re:

@ Jay P.: the idea behind /\  \A c \in Clients: LET a == tasks[c].agent is doing an assignment in batches. I have a doubt, however, using existential quantifier \E would not make it possible to leave some task unassigned forever? With \A it checks every task and whether it can be assigned or not. But in fact, it doesn't work properly, for what I intended.

@ Stephan: thanks for the tip, I was indeed looking for some way to choose randomly one element in {"ok", "error"} set.

Best regards,

2018-02-10 5:52 GMT-02:00 Stephan Merz :
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,
Stephan

P.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:

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.

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