Another couple of options you can use are
1. Set Simulation Mode under Advanced Options > TLC Options. It's not exhaustive, but it gives more confidence in unbounded traces.
2. Set Depth-First Mode under Advanced Options > TLC Options. This lets you specify a max bound to check. Warning: it's highly experimental and shouldn't be used as your only source of model.
On Thursday, 1 March 2018 13:06:34 UTC-6, Stephan Merz wrote: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]) <= 5State 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,StephanTo unsubscribe from this group and stop receiving emails from it, send an email to tlaplu...@xxxxxxxxxxxxxxxx.--PedroRegards,I attached the whole spec as well. Thanks!Another point: is it possible to avoid this storage from TLC?Is there any way to limit the size of the variable "network" (maybe some kind of assumption)? If so, would it solve the question?leads to an infinite behavior, since it can add requests infinitely (because a sequence is not limited). Am I understanding it wrong?and I'm asking myself whether the actionHi,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)]
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>>
--Pedro Yuri Arbs PaivaEngenheiro EletrônicoInstituto Tecnológico de Aeronáutica (T-16)
You received this message because you are subscribed to the Google Groups "tlaplus" group.
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>--
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+unsubscribe@googlegroups.com .
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 .