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

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

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 !