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.