[no subject]

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)

(+55) 12 98106-4129