Re: [tlaplus] Simulator claims invariant to be violated, which should be not

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

On 25.02.2018 18:47, Christian Spann wrote:
> I am working with a model of a Byzantine Consensus algorithm with
> exploding state space which therefore is effectively non checkable. To
> show a specific bug I try to "jump" through the state space by
> defining inverted invariants of states I think that should be reached
> on the path to the buggy state in the state graph. This is a tedious
> task and from time to time I use the simulator to quickly evaluate how
> my current approach behaves further down the state graph before
> calculating the minimum path to my next step. Currently I experience a
> strange behaviour using the Modelchecker and the Simulator with the
> same spec (i.e. MC.tla). While the Modelchecker runs for days and
> reaches state graph depths 72 with 15 Million States generated, the
> Simulator computes two states and exits stating that an invariant is
> violated. (15 Million states seems not much, it used to be faster
> before Spectre Bugfixes ... )
>
> The invariant is the following:
>
> DecidedSafe ==
>       \A s,t \in Server : \A v \in View :
>          (/\ decided[s][v] # Undef
>           /\ decided[t][v] # Undef
>           /\ state[t] = Normal
>           /\ state[s] = Normal) => decided[s][v] = decided[t][v]
>
> Curiously none of the variables used in the predicate changes from
> state 1 to state 2, the output of the simulator including both states
> is appended to this mail. The call to the Simulator is:
>
> java tlc2.Generator -n 10 -d 75 MC.tla &> trace.log
>
> , the Modelchecker is called via:
>
> java tlc2.TLC -config MC.cfg  -workers 8 MC.tla &> mc.log
>
> As the spec of the algorithm contains unpublished work I do not want
> to send it to this list, but I can send it directly if it helps to
> identify the cause of my experience. 

Hi Christian,

the underlying bug - a null pointer - will be fixed in the next Toolbox
release. Until then you can launch simulation with:

java tlc2.TLC -simulate -depth 75 MC.tla &> trace.log

However, this currently does not support writing a trace file and the
Generator's parameter "-n" to restrict the number of traces. You will
have to manually kill simulation once it has generated a large enough
number of states.

Thanks

Markus