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

[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,

thanks for the report and providing the corresponding spec off-list. We
will look into the issue.

Thanks
Markus