Re: Stuttering when adding

After reading the toolbox dynamic Help I saw :(
>>Warning: Because of a bug in TLC, checking of liveness properties does not work in simulation mode.

That's a shame, the simulation mode is pretty useful when the state space is too big.

In any case, I still do not get why some formulas succeed even if they should be failing. Like:
EnabledProcessNew == <>[](ChNoLoss(down) )
=> []<>(ENABLED <<Server!ProcessNew>>_<<up,down,srvTransRcvd,srvBuffer>>)

(That is, enabling just losses in one of the two channels for client-server communication).

Notice, that I believe that the Channel.tla spec is correct, because I have checked using ChannelSpec.tla (although I could be also wrong).

I have a spec that has a finite set of states (although large). I am trying to check some temporal formulas. In order to do so, I have to avoid infinite stuttering steps at the end of the behavior by adding in the Spec:

/\ []<><<TRUE>>_myvars

However, still some formulas that should fail do not fail. I have been looking for an error in the spec, but O'm not able to find it.

I guess that it could possible that when I use the TLC in "model-checking mode" there is improvable collision in the hash values of the states. How likely is this?

However, when I run in "simulation mode" (with different seeds) I get an error-trace due to a temporal formula violation due to stuttering... but how is it possible? I thought I removed this behaviors by adding "/\ []<><<TRUE>>_myvars" to my Spec.

How could it be possible?

Thanks for the help,

marc

PS: I attach the tla spec files. The parameters being used are:

NINFLIGHT --> 1

NBUFFER --> 1

NMAXTRANSACTION --> 1