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

*From*: Charles Gordon <charles...@xxxxxxxxx>*Date*: Wed, 25 Nov 2015 23:03:11 -0800 (PST)*References*: <1bb4f7e9-ffc4-45ee-af7a-a1035168b414@googlegroups.com>

Alright, I think I was just misunderstanding the answer given in the Hyperbook. The answer is:

On Wednesday, November 25, 2015 at 5:37:28 PM UTC-8, Charles Gordon wrote:

Let s1 -> s2 -> s3 -> ... be an infinite behavior satisfying A's behavior specification. For any variable v of A, definevto 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 behaviorsigmasatisfies 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:LetCountbe a specification with a single variablenwhose 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, thenCountimplements A under some refinement mapping.The definition of a refinement mapping is given four paragraphs earlier as:Arefinement mappingfrom a specificationHto a specificationAis an assignment of an _expression_vto each variable v ofA, wherevis defined in terms of the variables ofH.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 operatorev(i)which gives the value ofv(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?

**Follow-Ups**:**Re: Hyperbook Question 6.4***From:*Charles Gordon

**References**:**Hyperbook Question 6.4***From:*Charles Gordon

- Prev by Date:
**Hyperbook Question 6.4** - Next by Date:
**Re: [tlaplus] PlusCal sometimes not working in TLA+ Toolbox** - Previous by thread:
**Hyperbook Question 6.4** - Next by thread:
**Re: Hyperbook Question 6.4** - Index(es):