[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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.


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


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]
        /\ 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
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.