Re: [tlaplus] Re: TLC simulation error with liveness properties

[valentin....@xxxxxxx]

Hi Markus,

On Wednesday, May 23, 2018 at 4:15:14 PM UTC+1, Markus Alexander Kuppe wrote:
> 
> Hi Valentin,
> 
> that's a red herring. Changing diamond to box turns the liveness
> property into an invariant. Invariants get verified with a different
> algorithm.
> 

Right, that's actually obvious now that you point it out.

> ProcSet being a tuple indeed appears to be the root cause. I created an
> issue [1] and attached a condensed test spec.
> 
> Thanks
> Markus
> 
> [1] https://github.com/tlaplus/tlaplus/issues/164

Thanks !