Alright, I think I was just misunderstanding the answer given in the Hyperbook. The answer is:
Let s1 -> s2 -> s3 -> ... be an infinite behavior satisfying A's behavior specification. For any variable v of A, define v to equal ev(n), where ev(i) is the value of v in state si, for any positive integer i.
I had read that as being true for all possible infinite behaviors of A, implying that ev(n) needed to be a general mapping from Count. However, I think the intended reading is that exactly one infinite behavior of A is selected, and ev(n) is "hard coded" to the values of that behaviors states. Is that accurate? If that is the case, I believe I understand the question and its answer. If not, I'm obviously still confused!
As a side note, the definition of what it means for H to implement A reads (in part):
We say that H implements A ... iff, for each behavior sigma satisfying the behavior specification of H, the behavior sigma satisfies the behavior specification of A.
Is it correct to read that as (roughly):
\A sigma \in the_set_of_all_behaviors : sigma satisfies H <=> sigma satisfies A
The forward implication (sigma satisfies H => sigma satisfies A) seems straightforward, given the definition of a refinement mapping, but I'm having a harder time convincing myself of the backwards implication (sigma satisfies A => sigma satisfies H).
Is "The Existence of Refinement Mappings" the right paper to read for more background on refinement mappings? Is there more material elsewhere that explains this concept in another way (I just find it personally helpful to read multiple different explanations)?
Thank you!
On Wednesday, November 25, 2015 at 5:37:28 PM UTC-8, Charles Gordon wrote:
I am working my way through the TLA+ Hyperbook and have run into some trouble with question 6.4 on page 68. The question reads:
Let Count be a specification with a single variable n whose behavior specification allows the single infinite behavior
[n = 1] -> [n = 2] -> [n = 3] -> [n = 4] -> ...
Show that if A is any specification whose behavior specification allows an infinite behavior, then Count implements A under some refinement mapping.
The definition of a refinement mapping is given four paragraphs earlier as:
A refinement mapping from a specification H to a specification A is an assignment of an _expression_ v to each variable v of A, where v is defined in terms of the variables of H.
This confuses me, as the question seems to imply that it is possible to create a refinement mapping for variables that we know nothing about (the variables of A, which are not specified in the question). Furthermore, we need the refinement mapping to define the new "bar" variables in terms of the variables of Count (of which there is just one). The answer given in the hyperbook is to use an operator ev(i) which gives the value of v (from A) for state i. But wouldn't that operator need to be defined in terms of variables from A, when by definition the refinement mapping is to be defined in terms of variables from Count? What am I missing? Is this just a foreshadowing of the idea (later in this section) that all states have values assigned to all variables, so that the variables of A are actually present in the Count behavior listed in the question?