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

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

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

Hi Giulio,

is it correct that you observe this behavior with a recent Toolbox
nightly build only?

Thanks
Markus