# Re: [tlaplus] Weaker equivalences and refinement mappings

No. Please explain why you believe that the sequence 1,2,4,8,16,... is relevant to any of your specs or refinement maps. My claim in the previous email was that it was not relevant.

-Abhishek

On Sun, Sep 3, 2023 at 1:34 PM jack malkovick <sillymouse333@xxxxxxxxx> wrote:
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/567b1fd6-8c0b-4a6a-b791-8df033766859n%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ea0a3f30-12c1-4659-87fb-a5434911d530n%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFrvoiOQdChCr_RLUd7v7n_Bn62%2BhYSc_ss8NWOF%2Bo0ajuMevA%40mail.gmail.com.