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.
Justin (barely starting to play with TLA+ myself)
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.
I experimented with SimpleProgram, adding this definition:
Silly == /\ pc = "grape"
/\ 1 = "orange"
And changing the definition of Next:
Next == Pick \/ Add1 \/ Silly
TLC claimed my model is fine. That is what I expected from reading the silly expressions text.
Then, I changed the definition of Silly:
Silly == /\ pc = "middle"
/\ 1 = "orange"
TLC then said I was being ridiculous, using an integer as a function.
I think I get it.
One last thing I wondered, does the order of terms matter?
Silly == /\ 1 = "orange"
/\ pc = "grape"
It does. TLC tells me that this _expression_ is ridiculous even though it
is logically equivalent to the first. To use a potentially silly _expression_,
I must ensure that the predicates guarding it are evaluated first due
to what appears to be a short-circuit evaluation. I think the text might
be telling me that but I will study it more to be sure.
Thank you again.
On Saturday, November 4, 2017 at 10:55:07 PM UTC-7, Leslie Lamport wrote: