[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Invalid counter-example with Liveness checking


I'm working on a TLC bug [1] where it reports an invalid counter-example
with Liveness checking. If anybody has specs/models that exhibit this
bug, please share them with me.

If you do, please indicate if you agree to make the spec available at
the TLC source repository [2] under MIT [3] or if I should keep it private.


[1] http://tlaplus.codeplex.com/workitem/8
[2] https://tlaplus.codeplex.com/SourceControl/latest
[3] https://tlaplus.codeplex.com/license