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

[tlaplus] Weaker equivalences and refinement mappings

Suppose we have this spec


Init == x = 0

Next == x < 10 /\ x' = x + 1

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

And this one


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.