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

[tlaplus] BUG: temporal properties are incorrectly evaluated

Good day everyone.

Found a behaviour that I would classify a bug. The spec:


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.