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
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?