This commit[1] fix the bug. The new nightly build with the fix is available at [2]
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 ----------------------------
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