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

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

Hi,

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?

Cheers,

Marc

------------------------------ MODULE Example1 ------------------------------

EXTENDS Integers

VARIABLE x

Init == x = 0

Next == x' = ( x + 1 ) % 100

Spec == Init /\ [][Next]_<<x>> /\ []<><<TRUE>>_<<x>> 

Liveness1 == <>(x = -1000)

Liveness2 == <>(x = 101)

=============================================================================