[tlaplus] BUG: temporal properties are incorrectly evaluated

[dmitry.novoselov@xxxxxxxxx]

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.

-- 
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/b659a447-0cc3-40f7-86fe-9c6c8eb4e57d%40googlegroups.com.