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

Different behaviour of RandomElement during model checking and simulation mode

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