# Re: [tlaplus] Weaker equivalences and refinement mappings

Oh. Because {1, 2, 4, 8, 16, ...} is included in {1, 2, 4, 6, 8, 10, ... } right?

On Sunday, September 3, 2023 at 8:54:48 PM UTC+3 Abhishek Singh wrote:
Hi Jack,

TLC works as expected. In spec1, you may see the behavior (x=0) -> (x=1) -> (x=2) ->... Your refinement map says that this behavior can be mapped to (x=0, y=2*0) -> (x=1, y=1*2) -> (x=2, y=2*2) ->..., which is a valid behavior of Spec2. You can also test that y=x*2 is an invariant of Spec2. (You state that y is doubling at each step possibly yielding the geometric sequence 1,2,4,8,..., but this behavior is not specified anywhere.)

You can also try incorrect refinement maps such as x<-x, y<-x*3, which should yield an error trace.

Regards,
Abhishek

On Sun, Sep 3, 2023 at 11:08 AM jack malkovick <sillym...@xxxxxxxxx> wrote:

Suppose we have this spec

VARIABLES x

Init == x = 0

Next == x < 10 /\ x' = x + 1

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

And this one

VARIABLES x, y

Init == x = 0 /\ y = 0

Next == x < 10 /\ x' = x + 1 /\ y' = y + 2

Spec2 == Init /\ [][Next]_vars /\ WF_vars(Next)

The intention is to use TLC to show something like.

Spec1 equivalent \EE y : Spec2!Spec2 (at least what concerns the behavior of x)

Because TLC does not suport temporal existential quantifiers, I've tried something like

Refinement == INSTANCE Spec2 WITH x <- x, y <- x * 2

and checked the property Refinement!Spec2 and it worked!

I was glad that it did but also a little bit surprised. It's true that my intention was to check the "equivalence" of the two specs as "projected" on x, but how come wasn't TLC bothered that y was doubling at each step and in Spec2 it's just increasing by 2 ?

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