Re: [tlaplus] Re:

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

Your formula, somewhat simplified, is

\A c \in Client :

   LET a == tasks[c].agent

   IN  IF available(a)

       THEN status' = [status EXCEPT ![a] = "working"]

       ELSE status' = status

Suppose that you have two clients c1 and c2, and that the corresponding task agents are distinct, say, a1 and a2. Further assuming that available(a1) holds, this formula implies either

  [status EXCEPT ![a1] = "working"] = [status EXCEPT ![a2] = "working"]    or

  [status EXCEPT ![a1] = "working"] = status

depending on available(a2), and both of these are false [1]. So, the formula is satisfiable only in particular cases, e.g. if both a1 and a2 are unavailable, in which case the action just stutters, or if a1=a2.

Your action as you have written it only makes sense if the action updates the status of just one client, hence the existential quantifier. If you want to update the status of several clients, you have to reformulate the entire action using set expressions.

Stephan

On 10 Feb 2018, at 12:50, Pedro Paiva <pedr...@xxxxxxxxx> wrote:

Hi, thank you! Very helpful answers.

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

--

Pedro Yuri Arbs Paiva

Engenheiro Eletrônico

Instituto Tecnológico de Aeronáutica (T-16)

(+55) 12 98106-4129

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