Silly == /\ pc = "grape"
/\ 1[2] = "orange"
And changing the definition of Next:
Next == Pick \/ Add1 \/ Silly
Silly == /\ pc = "middle"
/\ 1[2] = "orange"
Silly == /\ 1[2] = "orange"
/\ pc = "grape"
One last thing I wondered, does the order of terms matter?
Regarding the order of terms, I remember reading that's one of those things where TLC is enforcing a convenient subset of TLA+, whereas TLAPS behaves differently. Mathematically the order doesn't matter, and a formal proof may take advantage of that fact, but the model checker takes the easier route of short-circuit evaluation.
Cheers,
Justin (barely starting to play with TLA+ myself)
From:
<tla...@googlegroups.com> on behalf of Greg Wiley <azte...@jammm.com>
Reply-To: "tla...@googlegroups.com" <tla...@googlegroups.com>
Date: Sunday, November 5, 2017 at 3:39 PM
To: tlaplus <tla...@googlegroups.com>
Subject: [tlaplus] Re: What does f[x] mean when f is not a function?
It appears I am guilty of thinking like a computer programmer.
Thank you for that. Because of other conjucands, RdMiss would never be a step from a state where buf[p] is not a request.
--
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 post to this group, send email to tla...@googlegroups.com.
Visit this group at
https://groups.google.com/group/tlaplus.
For more options, visit
https://groups.google.com/d/optout.