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

Infinite behaviors


I'm trying to model check my specification, but it is taking too long and the shown storage is over 5GB. I tried to figure it out what is happening, but I'm not sure. I am using a variable

network \in [Nodes -> Seq(Messages)]

and I'm asking myself whether the action

SendRequest(c,t) ==
    /\ isValidTask(t)
    /\ LET
        msg == [type |-> "request", src |-> c, dest |-> Master, data |-> t]
        /\ network' = [network EXCEPT ![Master] = Append(@, msg)]
        /\ UNCHANGED <<regAgents, tasks, assigned, notifications, status>>

leads to an infinite behavior, since it can add requests infinitely (because a sequence is not limited). Am I understanding it wrong?

Is there any way to limit the size of the variable "network" (maybe some kind of assumption)? If so, would it solve the question?

Another point: is it possible to avoid this storage from TLC?

I attached the whole spec as well. Thanks!


Pedro Yuri Arbs Paiva
Engenheiro Eletrônico
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129

Attachment: zkmacProtocolNet.tla
Description: Binary data