Bizzare TLC error on checking liveness with weak fairness

[tlalearner]

I have a pretty simple spec which contains a liveness property with weak fairness defined. This will throw an error upon execution:

---------- MODULE test ----------

 

EXTENDS TLC

\* Example: {0,1}

CONSTANT constantDataSet

VARIABLE stateA, unusedState

vars == << unusedState, stateA >>

testAction ==

    /\ \E x \in constantDataSet : 

        /\ x \notin stateA

        /\ stateA' = stateA \union {x}

        

next == \/ (testAction /\ UNCHANGED << unusedState >>)

init == /\ unusedState = {}

        /\ stateA = {}

spec == 

   /\ init

   /\ [][next]_vars

   /\ WF_vars(testAction)

livenessPropertyToTest ==

    <>[](constantDataSet \subseteq stateA /\ stateA \subseteq constantDataSet)

==================================  

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.lang.RuntimeException

: 

In evaluation, the identifier unusedState is either undefined or not an operator.

line 10, col 12 to line 10, col 22 of module test

However, if I move the UNCHANGED << unusedState >> from the definition of next to testAction, then the spec runs without an issue.

testAction ==

    /\ \E x \in constantDataSet : 

        /\ x \notin stateA

        /\ stateA' = stateA \union {x}

    /\ UNCHANGED << unusedState >>

        

next == \/ testAction

I'm having a hard time understanding why this fixes it. Aren't the above and below specs identical?  

[Stephan Merz]

They are not identical because the fairness conditions are different: when UNCHANGED is part of the definition of `next', it is not included in WF_vars(testAction), and in particular TLC cannot evaluate if an occurrence of `testAction' changed `vars' or not. I bet that everything works fine if you write WF_vars(next) for your original spec.

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ac36a0c7-531c-4f02-aa49-6d4b50ad5e58n%40googlegroups.com.