[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: azte...@xxxxxxxxx*Date*: Sat, 4 Nov 2017 18:05:19 -0700 (PDT)

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

**Follow-Ups**:**Re: What does f[x] mean when f is not a function?***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Specifying Systems fig 3.2 : is my understanding correct?** - Next by Date:
**Re: What does f[x] mean when f is not a function?** - Previous by thread:
**Re: [tlaplus] Specifying Systems fig 3.2 : is my understanding correct?** - Next by thread:
**Re: What does f[x] mean when f is not a function?** - Index(es):