Re: [tlaplus] Re:

[Stephan Merz <stepha...@xxxxxxxxx>]

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:

   /\ 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+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.