Different behaviour of RandomElement during model checking and simulation mode

[Giulio Salierno <salier...@xxxxxxxxx>]

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 ----------------------------
EXTENDS TLC,Integers
VARIABLE x,y




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

Invariant == x = y