41 views
Skip to first unread message

Pedro Paiva

unread,
Feb 9, 2018, 1:43:21 PM2/9/18
to tla...@googlegroups.com
Hi,

My name is Pedro andI'm starting to learn TLA+, trying to apply it to my research work. Basically, I am modeling a system with clients, agents and a master agent. The master receives tasks from the clients and assigns these tasks to the agents. A task is simply a record (agent, configuration). And clients must be notified whether success or failure. I am not concerned now with success of the task.

Part the condition for a client request is no other client requesting the same agent to perform a task. I express this here:

CRequest(c, T) ==
    /\ T \in Task
    /\ tasks[c] = noTask
    /\ \A cc \in Clients : tasks[cc] \in Task => tasks[cc].agent # T.agent
    /\ tasks' = [tasks EXCEPT ![c] = T]
    /\ UNCHANGED <<regAgents, assigned, notifications, status>>

The problem is: when I add this condition, TLC runs without errors, but no other actions are executed, except this CRequest. I noticed this looking at

Imagem inline 1

the number of counts for each line with primed variables. Without this condition, the other actions are performed, but then I cannot check the safety property. I attached the whole specification as well. Could someone help me understand why TLC behaves this way? I believe it is my mistake since I have not much experience. Thank you a lot.

Regards,

--
Pedro Yuri Arbs Paiva
Engenheiro Eletrônico
Instituto Tecnológico de Aeronáutica (T-16)
zkmacProtocol.rtf

par...@gmail.com

unread,
Feb 10, 2018, 2:38:59 AM2/10/18
to tlaplus
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.

Stephan Merz

unread,
Feb 10, 2018, 2:52:23 AM2/10/18
to tla...@googlegroups.com
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!


--
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...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Pedro Paiva

unread,
Feb 10, 2018, 6:50:36 AM2/10/18
to tla...@googlegroups.com
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...@gmail.com>:
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...@gmail.com 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...@googlegroups.com.
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...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Jay Parlar

unread,
Feb 10, 2018, 9:30:30 AM2/10/18
to tlaplus
On Saturday, 10 February 2018 06:50:36 UTC-5, Pedro Paiva wrote:
> @ 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.

That sound like you're trying to use \A as a "for loop", which isn't correct. Remember that your action has to take a single step. That step might involve your `assigned` and `status` variables changing quite a bit, but you can't explicitly "loop" in your formula to make that happen.

Does this do what you want?

assignAgents ==
LET toAssign == {a \in Agents : available(a)} IN
/\ assigned' = assigned \cup toAssign
/\ status' = [s \in DOMAIN status |-> IF s \in toAssign THEN "working" ELSE status[s]]
/\ UNCHANGED <<regAgents, tasks, notifications>>


--
Jay Parlar

Stephan Merz

unread,
Feb 10, 2018, 9:32:57 AM2/10/18
to tla...@googlegroups.com
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


To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.

Pedro Paiva

unread,
Feb 10, 2018, 9:51:35 AM2/10/18
to tla...@googlegroups.com
Jay and Stephan, thank you again! Indeed, I was thinking "\A c \in Client" as a "for loop", which is not correct, as Jay just said. It makes sense to reformulate it using set expressions.

Regards,
Pedro
Reply all
Reply to author
Forward
0 new messages