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 ?
--