Re: [tlaplus] Weaker equivalences and refinement mappings

11: x = 10 /\ y = 20
(It's precisely 11 states. You can verify it with TLC)

Now let's check the refinement:
Spec3:
1: x = 0 /\ y = 2 * x = 2 * 0 = 0 --> x = 0 /\ y = 0
2: x = 1 /\ y = 2 * x = 2 * 1 = 2 --> x = 1 /\ y = 2
3: x = 2 /\ y = 2 * x = 2 * 2 = 4 --> x = 2 /\ y = 4
4: x = 3 /\ y = 2 * x = 2 * 3 = 6 --> x = 3 /\ y = 6
5: x = 4 /\ y = 2 * x = 2 * 4 = 8 --> x = 4 /\ y = 8
6: x = 5 /\ y = 2 * x = 2 * 5 = 10 --> x = 5 /\ y = 10
7: x = 6 /\ y = 2 * x = 2 * 6 = 12 --> x = 6 /\ y = 12
8: x = 7 /\ y = 2 * x = 2 * 7 = 14 --> x = 7 /\ y = 14
9: x = 8 /\ y = 2 * x = 2 * 8 = 16 --> x = 8 /\ y = 16
10: x = 9 /\ y = 2 * x = 2 * 9 = 18 --> x = 9 /\ y = 18
11: x = 10 /\ y = 2 * x = 2 * 10 = 20 --> x = 10 /\ y = 20

Note that every state of Spec3 corresponds perfectly to the state with the same number of Spec2. Hence the refinement is valid. BTW, that's not the requirement. The requirement is to map every behavior of SpecA to SpecB. Multiple states of SpecA can be mapped to a single state of SpecB.

I hope this clarifies things.
Samyon.

On Sunday, September 3, 2023 at 9:46:11 PM UTC+3 Abhishek Singh wrote:

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