[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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
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.
Pedro Yuri Arbs Paiva
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129
Description: RTF file