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

*From*: jack malkovick <sillymouse333@xxxxxxxxx>*Date*: Sun, 3 Sep 2023 11:34:36 -0700 (PDT)*References*: <567b1fd6-8c0b-4a6a-b791-8df033766859n@googlegroups.com> <CAFrvoiNHvKdzCcFSv+m5BmCMhN=PNeWZ5XFxUhk0s2_Zx1+9yQ@mail.gmail.com>

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.

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

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

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

- 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):