The answer to your two questions is that they are "silly expressions". See Section 6.2 (page 67) of Specifying Systems.
Leslie
On Saturday, November 4, 2017 at 10:50:38 PM UTC-7, Greg Wiley wrote:
In the TLA book on page 57, the definition for RdMiss(p) contains the formula:
buf[p].op = "Rd"
However, buf is function with domain Proc and range that includes
requests, values, and NoValue. So, buf[p] might not be a function with a
domain containing "op". It might not be a function at all.
I guess I have two questions:
What does f["op"] mean when "op" is not in the domain of the function, f?
What does f["op"] mean when f is not a function?
I'm looking specifically for what those things mean in TLA+ but a mathematical
context is more than welcome.
TIA, -=greg