Re: [tlaplus] Infinite behaviors

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]) <= 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

On 1 Mar 2018, at 19:35, Pedro Paiva <ped...@xxxxxxxxx> wrote:

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...@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.

<zkmacProtocolNet.tla>