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).
On Monday, June 10, 2013 4:19:45 PM UTC+2, marc magrans de abril wrote:
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>>_myvarsHowever, 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,marcPS: I attach the tla spec files. The parameters being used are:NINFLIGHT --> 1NBUFFER --> 1NMAXTRANSACTION --> 1
Description: Binary data