| 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
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 tlaplus+u...@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.
|