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

*From*: Charles Gordon <charles...@xxxxxxxxx>*Date*: Tue, 1 Dec 2015 08:59:54 -0800 (PST)*References*: <1bb4f7e9-ffc4-45ee-af7a-a1035168b414@googlegroups.com> <b3274b0b-2daa-49ed-8cb6-1f62c43790cb@googlegroups.com>

Section six of the Hyperbook has been my personal "pons asinorum". For any current or future readers of the Hyperbook having the same difficulty, I found sure footing only after reading the first six sections of this paper:

http://research.microsoft.com/pubs/64074/lamport-actions.pdf

The Hyperbook introduces a lot of terminology in section six (state predicate, property, temporal formula, theorem, formula) and it wasn't clear to me how they related to each other (or which were simply synonyms), and how they related to earlier terms (specification, invariant, predicate, behavior, state). The above paper provides very clear definitions of those terms and their relationships, which made the Hyperbook immensely easier to understand. If I were starting over again, I'd want to read the first five sections of the Hyperbook, then the first six sections of "The Temporal Logic of Actions" (linked above), then section six of the Hyperbook.

On Wednesday, November 25, 2015 at 11:03:11 PM UTC-8, Charles Gordon wrote:

On Wednesday, November 25, 2015 at 11:03:11 PM UTC-8, Charles Gordon wrote:

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, 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 <=>sigmasatisfies AThe forward implication (sigma satisfies H =>sigmasatisfies A) seems straightforward, given the definition of a refinement mapping, but I'm having a harder time convincing myself of the backwards implication (sigmasatisfies 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?

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

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

- Prev by Date:
**Re: PlusCal: implicit label Error (PlusCal translator bug?)** - Next by Date:
**Re: Hyperbook Question 6.4** - Previous by thread:
**Re: Hyperbook Question 6.4** - Next by thread:
**Re: Hyperbook Question 6.4** - Index(es):