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

*From*: Abhishek Singh <abhishek1729@xxxxxxxxx>*Date*: Sun, 3 Sep 2023 13:45:55 -0500*References*: <567b1fd6-8c0b-4a6a-b791-8df033766859n@googlegroups.com> <CAFrvoiNHvKdzCcFSv+m5BmCMhN=PNeWZ5XFxUhk0s2_Zx1+9yQ@mail.gmail.com> <ea0a3f30-12c1-4659-87fb-a5434911d530n@googlegroups.com>

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

**Follow-Ups**:**Re: [tlaplus] Weaker equivalences and refinement mappings***From:*'Samyon Ristov' via tlaplus

**References**:**[tlaplus] Weaker equivalences and refinement mappings***From:*jack malkovick

**Re: [tlaplus] Weaker equivalences and refinement mappings***From:*Abhishek Singh

**Re: [tlaplus] Weaker equivalences and refinement mappings***From:*jack malkovick

- Prev by Date:
**Re: [tlaplus] Weaker equivalences and refinement mappings** - Next by Date:
**Re: [tlaplus] Weaker equivalences and refinement mappings** - Previous by thread:
**Re: [tlaplus] Weaker equivalences and refinement mappings** - Next by thread:
**Re: [tlaplus] Weaker equivalences and refinement mappings** - Index(es):