It appears I am guilty of thinking like a computer programmer.
Thank you for that. Because of other conjuncts, 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[2] = "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[2] = "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[2] = "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.
-=greg
On Saturday, November 4, 2017 at 10:55:07 PM UTC-7, Leslie Lamport wrote:
The answer to your two questions is that they are "silly expressions". See Section 6.2 (page 67) of Specifying Systems.
Leslie