BUG: temporal properties are incorrectly evaluated

[dmitry.n...@gmail.com]

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.

[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

[Andrew Helwer]

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

[dmitry.n...@gmail.com]

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 написал: