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

Re: [tlaplus] Infinite behaviors

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