[tlaplus] Bizzare TLC error on checking liveness with weak fairness

[tlalearner <squally3.1@xxxxxxxxx>]

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?  

-- 
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/ac36a0c7-531c-4f02-aa49-6d4b50ad5e58n%40googlegroups.com.