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

*From*: Changgeng Zhao <zcg...@xxxxxxxxx>*Date*: Mon, 26 Mar 2018 19:59:40 -0700 (PDT)*References*: <c2c1a8ae-df92-458c-8100-9626eac2f23b@googlegroups.com> <0DFAF9F1-460F-4EB3-9BF6-021508EE331F@gmail.com>

OK, let me show it in another way.

On Friday, March 23, 2018 at 9:45:06 PM UTC+8, Stephan Merz wrote:

Suppose I have one higher level specification:

VARIABLE a \* a is an integer

Next == \/ otherSubActions

\/ a' = a + 1

And now I want to design a implementation which refines the above specification, but in the implementation it batches the a' = a + 1 steps:

VARIABLE a \* a is an integer

Next == \/ otherSubActions

\/ a' = a + 10

In the implementation the variable "a" always increases 10 at a time, which means batching 10 steps of the specification's subAction2.

I think this is actually a kind of refinement, but I can not use stuttering variables to prove it, because : after each step of Specification, the variable "a" will change, while stuttering steps don't change any external state.

On Friday, March 23, 2018 at 9:45:06 PM UTC+8, Stephan Merz wrote:

Hello,I have a hard time understanding the question. For one thing, the parameter a of subaction1 appears to be a variable (since you use a') but in subaction2 the quantified variable a denotes a value, and therefore a' = a.Also, when you write a specification that involves sets of values, you typically use functions and have actions with conjuncts of the formx' = [x EXCEPT ![a] = ...]Then, if you try to combine several of those you obtain\A a \in A : x' = [x EXCEPT ![a] = ...]which is contradictory when A has more than one element.Perhaps you could share a more complete specification to clarify what you are trying to achieve.Regards,StephanOn 23 Mar 2018, at 04:33, Changgeng Zhao <zcg...@xxxxxxxxx> wrote:I am trying to prove one algorithm refines another algorithm. Let's call them Implementation and Specification.For example, the Specification has one subaction that :subaction1(a) == /\ F1(a)/\ F2(a')While in the Implementation, it will batch several of this step in one subaction, which is like:subaction2(A) ==\A a \in A :/\ F1(a) /\ F2(a')(A is a set consisting of element a, and each element doesn't interfere with other elements in A)Then how can I represent it with the format of refinement mapping, for example using auxiliary variables? Or is it not a refinement mapping cause they doesn't have same behavior?--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplu...@xxxxxxxxxxxxxxxx.

To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.

Visit this group at https://groups.google.com/group/tlaplus .

For more options, visit https://groups.google.com/d/optout .

**References**:**How to give a refinement mapping from one subactions to many subactions***From:*Changgeng Zhao

**Re: [tlaplus] How to give a refinement mapping from one subactions to many subactions***From:*Stephan Merz

- Prev by Date:
**Fairness condition for messages** - Next by Date:
**relevant conferences?** - Previous by thread:
**Re: [tlaplus] How to give a refinement mapping from one subactions to many subactions** - Next by thread:
**Re: How to give a refinement mapping from one subactions to many subactions** - Index(es):