[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Different behaviour of RandomElement during model checking and simulation mode
On 25.06.2018 16:19, Giulio Salierno wrote:
> 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 is violated using 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 some model-checking execution?
> Thank you
is it correct that you observe this behavior with a recent Toolbox
nightly build only?