[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re:

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"} : ...


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.