checking that a pluscal spec implements another pluscal spec

[jack malkovick]

Hello! I have a question and I think it's not possible, but I'll give it a try.

Let's say I want to check that spec that refines another spec. The variables that they have in common should be the same (considering stuttering invariance of course). But they are both generated by PlusCal and they have a `pc` variable that clearly does not correspond state by state.

Can I somehow check that RefinedSpec => GeneralSpec ignoring that common `pc` variable?

[Stephan Merz]

In TLA+, the refinement that you want to prove is stated as

RefinedSpec => \EE pc : GeneralSpec

Unfortunately, no TLA+ verifier handles the \EE quantifier, so you'll have to explain how the pc variable of the high-level spec is implemented in the low-level spec. If you can recompute the value of that variable for any (reachable) state of the low-level spec, you can define that refinement mapping using an operator definition (in the module for the low-level spec)

AbstractPC == ...

Then instantiate the high-level spec

GSpec == INSTANCE HighLevel WITH pc <- AbstractPC

and check the property GSpec!Spec. If you cannot come up with the required mapping, you'll need to use history or prophecy variables, and things get more complicated [1,2].

Stephan

[1] http://lamport.azurewebsites.net/pubs/pubs.html#simple

[2] http://lamport.azurewebsites.net/pubs/pubs.html#auxiliary

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/621083e7-5318-4ef6-8fce-fb725ccf806an%40googlegroups.com.