Re: [tlaplus] How to give a refinement mapping from one subactions to many subactions

OK, let me show it in another way.

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 form

x' = [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,
Stephan

On 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.