Re: [tlaplus] Tagged formulas

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

On Thursday, January 14, 2016 at 4:03:18 PM UTC+2, Ron Pressler wrote:

    VARIABLE x

    Capture(e) == CHOOSE k \in {e} : k = e

    Next == /\ x' = x + 1 

                  /\ PrintT(x)                   \* => 1

                  /\ PrintT(x')                  \* => 2

                  /\ PrintT(Capture(x))    \* => 1

                  /\ PrintT(Capture(x)')   \* => 2

    Spec == (x = 1) /\ [][Next]_<<x>>

So Capture(x)' /= Capture(x), and this seems to be more than just level-checking.

Just to clarify: My proposal for Capture would yield Capture(x)' = 1 instead of 2 (because Capture(x)' = Capture(x) = x = 1) , so changing the treatment of CHOOSE to display this behavior would change actual semantics.