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

Hi Hillel,

Thanks for explanation, peeking into WF_vars definition was insightful. The spec formula, with its WF_vars and SF_vars, and the notion of a model's properties still were a bit magic for me. Now I understand them better, thanks a lot!

воскресенье, 21 июля 2019 г., 22:58:51 UTC+3 пользователь Hillel Wayne написал:

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