Stuttering when adding

[marc magrans de abril <marcmagra...@xxxxxxxxx>]

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

Attachment: Channel.tla
Description: Binary data

Attachment: Client.tla
Description: Binary data

Attachment: Server.tla
Description: Binary data

Attachment: System.tla
Description: Binary data