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?