[tlaplus] Re: BUG: temporal properties are incorrectly evaluated

I stumbled into a similar problem with my spec (accidentally defining a spec with no valid behaviors) so created an issue on github to warn users if this happens: https://github.com/tlaplus/tlaplus/issues/161

Andrew

On Sunday, July 21, 2019 at 12:58:51 PM UTC-7, Hillel Wayne wrote:

Hi Dmitry,

This isn't actually a bug. Your spec isn't machine-closed (see page 112 in Specifying Systems). Let's expand out the definition of WF_vars(HackStep):

WF_vars(HackStep) == <>[](ENABLED <<HackStep>>_vars) => []<><<Hackstep>>_vars)

In your spec, Hackstep is always enabled: there is no state where tmp' = 1 /\ UNCHANGED pc is forbidden. But Hackstep isn't part of your spec. So we can (handwaving a bit) rewrite it as

Spec == Init /\ [][(Step1 \/ Step2) /\ ~HackStep]_vars /\ []<><<Hackstep>>_vars

So we have that in a valid behavior, HackStep must happen infinitely often and also HackStep may never happen. No behavior could satisfy this, and it reduces to Spec == FALSE.

Saying GetsToDone is a property is equivalent to saying Spec => GetsToDone, which is equivalent to FALSE => GetsToDone, which is trivially true.

Always make sure your spec is machine closed. You can do that by only writing fairness properties that are subactions of Next.

Hillel

On Sunday, 21 July 2019 09:21:33 UTC-5, dmitry....@xxxxxxxxx wrote:
Good day everyone.

Found a behaviour that I would classify a bug. The spec:
VARIABLES tmp, pc vars == << tmp, pc >> Init == /\ tmp = 0 /\ pc = "Step1" Step1 == /\ pc = "Step1" /\ pc' = "Step2" /\ UNCHANGED << tmp >> Step2 == /\ pc = "Step2" /\ \/ pc' = "Step1" \/ pc' = "Done" /\ UNCHANGED << tmp >> HackStep == /\ tmp' = 1 /\ UNCHANGED << pc >> Next == \/ Step1 \/ Step2 \* Next doesn't have HackStep on it... \/ (pc = "Done" /\ UNCHANGED vars) Spec == /\ Init /\ [][Next]_vars /\ WF_vars(Next) /\ WF_vars(HackStep) \* ...but Spec does have a weak fairness requirement for HackStep GetsToDone == <>[](pc = "will never get this value")

If I add GetsToDone to the model' properties, the model passes. And it does fail as expected if I add HackStep to the Next action.

This may be cofusing even in such a tiny spec. And it took me quite some time to figure this out in the actual specification I was actually working on.

I am not sure the spec is simplest possible to manifest this behaviour. Hope it small enough to troubleshoot.