Infinite behaviors

Hi,

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]
       IN
        /\ 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!

Regards,

Pedro

Pedro Yuri Arbs Paiva

Engenheiro Eletrônico

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

(+55) 12 98106-4129