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

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



On 23.05.2018 16:12, valentin....@xxxxxxx wrote:
> It seems the error only arises when all of the following conditions are met:
> * The liveness property involves <>. I don't hit the bug if e.g. Worked == [](\A t \in TASKS : var[t] < 2)

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.

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