[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: TLC simulation error with liveness properties
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
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  and attached a condensed test spec.
>  https://github.com/tlaplus/tlaplus/issues/164