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

Re: Different behaviour of RandomElement during model checking and simulation mode

This commit[1] fix the bug. The new nightly build with the fix is available at [2]

[2] https://tla.msr-inria.inria.fr/tlatoolbox/ci/products/

Il giorno lunedì 25 giugno 2018 16:19:24 UTC+2, Giulio Salierno ha scritto:
Dear all, 
considering the following snippet of TLA, i can't figure out why the invariant (x = y)  is always verified using the model-checking mode while it’s violated during the simulation mode (as i expect). Moreover using the DFS instead of BFS it's being violated. The invariant should not be eventually violated also during the model-checking execution? I expect that exist in some behavior a state in which x != y.
Thank you

---------------------------- MODULE RandomCheck ----------------------------

Init == /\ x = 0
        /\ y = 0 
Next == /\ x' = RandomElement(-1..1)
        /\ y' = RandomElement(-1..1)
        /\ PrintT(x)
        /\ PrintT(y)

Invariant == x = y