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

[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.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e5f1c587-0928-4e08-9eba-84bcba04f192%40googlegroups.com.