Invalid counter-example with Liveness checking

[Markus Alexander Kuppe]

Hi,

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.

Thanks
Markus

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