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

*From*: Abhishek Singh <abhishek1729@xxxxxxxxx>*Date*: Sun, 3 Sep 2023 12:54:33 -0500*References*: <567b1fd6-8c0b-4a6a-b791-8df033766859n@googlegroups.com>

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 <sillymouse333@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+unsubscribe@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/CAFrvoiNHvKdzCcFSv%2Bm5BmCMhN%3DPNeWZ5XFxUhk0s2_Zx1%2B9yQ%40mail.gmail.com.

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

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

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