Hello Pedro,
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.
Regards, Stephan
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
--
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.
<zkmacProtocolNet.tla>
|