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

Re: [tlaplus] How to build Codeplex Tlaplus Tools?

Silly me :) 


On Mon, Mar 30, 2015 at 10:36 AM, Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx> wrote:
On 30.03.2015 08:58, marc magrans de abril wrote:
> Today, I just tried a simple example (see below) were an integer is
> incremented by 1 (modulo 100). The model checker finds the error on
> Liveness1 and Liveness2 properties. However, the simulator does not find
> them.
> Is this a bug, or just something not understood on my side?

Hi Marc,

the problem is not a bug in simulation mode. Simulation - by default -
checks behaviors up to a length of 100 states. This is too short for
your invariants. Try increasing the "Maximum length of a trace" to more
than 100 states on the "Advanced Options" page of the Model editor.

Regular model checking obviously does not restrict behaviors to a
maximum length.


You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/XLAfgMVAu38/unsubscribe.
To unsubscribe from this group and all its topics, 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.
For more options, visit https://groups.google.com/d/optout.