you are right that your specification has an infinite state space due to the unbounded message channel. In order to make TLC explore only a finite fragment of that state space, add a state constraint such as
\A p \in Process : Len(network[p]) <= 5
State constraints can be added in the “advanced options” tab of the Toolbox interface for the model checker. Obviously, you give up on exhaustive checking, but a reasonable bound will give you good confidence in your verification results.
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?
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
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx
Visit this group at https://groups.google.com/group/tlaplus
For more options, visit https://groups.google.com/d/optout