Re: [tlaplus] Re: Stuttering when adding

[TLA Plus <tlapl...@xxxxxxxxx>]

   the simulation mode is pretty useful when the state space is too big

The TLA+ tools are now an open-source project.  Anyone who wants to fix this bug is welcome to download the code and try to do so.

   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>>)

This formula uses symbols that are not defined in any of the
modules you sent.  I don't know why you expect us to understand it.

 

Leslie Lamport

On Mon, Jun 10, 2013 at 6:47 AM, marc magrans de abril <marcmagra...@xxxxxxxxx> wrote:

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>>_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

--
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 http://groups.google.com/group/tlaplus?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.