Doubt about refinement

[Pedro Paiva]

Hi there,

Reading the paper [1], I ended up with some doubts about the refinement:
Allocator => SimpleAllocator

I understand that refinement is an implication, in the sense that SchedulingAllocator satisfies the SimpleAllocator's spec as well. I got into trouble trying to understand the module AllocatorRefinement, which is stated below:

EXTENDS SchedulingAllocator

Simple == INSTANCE SimpleAllocator

SimpleAllocator == Simple!SimpleAllocator

THEOREM Allocator => SimpleAllocator

Actually, I can't understand what this means: Simple!SimpleAllocator (the use of operator "!" is not clear to me). I tried to read about it in Specifying Systems, but the question still remains.

Furthermore, what should be the conditions to write a spec that implements another one? Thanks!

[1] S. Merz: The TLA+ Specification Language. https://members.loria.fr/SMerz/papers/tla+logic2008.html

Regards,

--

Pedro Yuri Arbs Paiva

Engenheiro Eletrônico

Instituto Tecnológico de Aeronáutica (T-16)

(+55) 12 98106-4129

[Stephan Merz]

Hello,

> On 16 Feb 2018, at 21:10, Pedro Paiva <pedr...@gmail.com> wrote:
>
> Hi there,
>
> Reading the paper [1], I ended up with some doubts about the refinement:
> Allocator => SimpleAllocator
>
> I understand that refinement is an implication, in the sense that SchedulingAllocator satisfies the SimpleAllocator's spec as well.

in a linear-time formalism such as TLA+, a (lower-level) specification R refines a (higher-level) specification S if every behavior that is allowed by R is also allowed by S. When R and S are expressed as temporal logic formulas, this just means that the implication R => S is valid.

> I got into trouble trying to understand the module AllocatorRefinement, which is stated below:
>
> EXTENDS SchedulingAllocator
> Simple == INSTANCE SimpleAllocator
> SimpleAllocator == Simple!SimpleAllocator
>
> THEOREM Allocator => SimpleAllocator
>
> Actually, I can't understand what this means: Simple!SimpleAllocator (the use of operator "!" is not clear to me). I tried to read about it in Specifying Systems, but the question still remains.

Module AllocatorRefinement extends SchedulingAllocator, so it conceptually contains all definitions etc. that appear in that module. In particular, the formula "Allocator" on the left-hand side of the implication is just the one defined in module SchedulingAllocator.

Now, we want to state a theorem that expresses that (the system described by) "Allocator" is a refinement of the high-level specification, expressed as formulas "SimpleAllocator" in module SimpleAllocator. (Perhaps what confuses you is the module and the formula expressing the specification have the same name – admittedly not a good choice, but allowed by TLA+.) So we need to import the definitions from that module, and although in simple cases we could just again extend module SimpleAllocator, this is likely to lead to name clashes between definitions of operators with the same name (such as "Init" or "Next"). Instead, we create an "instance" of that module: that is what the line "Simple == ..." does. Conceptually, we get a copy of all the definitions etc. contained in module SimpleAllocator, but prefixed by "Simple!" [1]. I could therefore have stated the refinement theorem as

THEOREM Allocator => Simple!SimpleAllocator

but at the time when the report was written, TLC wouldn't accept properties called something like "X!Spec", so I introduced a new definition for "SimpleAllocator" (now in the name space of module AllocatorRefinement) that abbreviates that formula. I could have chosen a completely different name, and anyway nowadays you can just let TLC check "Simple!SimpleAllocator" as a temporal property.

> Furthermore, what should be the conditions to write a spec that implements another one? Thanks!

Not sure I understand the question. You should make sure that the above implementation is valid. Perhaps you are thinking in terms of proof obligations as in proof-based formal methods, and indeed if you were using a theorem prover such as TLAPS you'd have to think of how you can prove the above temporal logic implication from state- and action-level formulas, but here we are just doing model checking and let TLC compute the state graphs of the involved specifications. Arguably, you learn less about why your refinement holds, but you have much less work (also, you get a counter-example when TLC finds that the implication is not valid).

Hope this helps – feel free to contact me by direct email if you have further questions.

Regards,
Stephan


[1] In general, instantiation is more powerful and in particular allows variables of the instantiated module to be substituted by state-level expressions of the instantiating module (this is known as a "refinement mapping"), but in this simple case, this extra complexity is not needed.

[Pedro Paiva]

Hi Stephan,

Thank you again for the help.

"Perhaps what confuses you is the module and the formula expressing the specification have the same name" that confused me, indeed. So I can use "Simple!" to access anything from module SimpleAllocator, right? e.g. "Simple!alloc" to access the variable "alloc" from module "SimpleAllocator".

And when you check "PROPERTIES SimpleAllocator" with TLC, you're checking Simple!SimpleAllocator (which is defined only as "SimpleAllocator")?

Best regards,

Pedro

--
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@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Stephan Merz]

Hi Pedro,

> On 19 Feb 2018, at 22:09, Pedro Paiva <pedr...@gmail.com> wrote:
>
> "Perhaps what confuses you is the module and the formula expressing the specification have the same name" that confused me, indeed. So I can use "Simple!" to access anything from module SimpleAllocator, right? e.g. "Simple!alloc" to access the variable "alloc" from module "SimpleAllocator".

you can refer to any defined entity e (operator, assumption, theorem) from module SimpleAllocator as Simple!e within the namespace of the instantiating module. SANY will reject Simple!alloc since alloc is declared, not defined, in module SimpleAllocator. If you need to refer to the value of the variable from within the instantiating module, you have to add a definition like

varalloc == alloc

in module SimpleAllocator, then refer to Simple!varalloc.

> And when you check "PROPERTIES SimpleAllocator" with TLC, you're checking Simple!SimpleAllocator (which is defined only as "SimpleAllocator")?

Again, you have to consider which namespace you are in. SimpleAllocator exists in the namespace of the refinement module because it is a defined operator (whose definition is Simple!SimpleAllocator). Without that definition, SimpleAllocator is not a defined operator, but Simple!SimpleAllocator refers to the operator imported through the instantiation.

I am assuming that you are using the Toolbox, and then you can either enter "SimpleAllocator" or "Simple!SimpleAllocator" as a temporal property to be checked. At the time when I wrote the report, the Toolbox didn't exist and one had to write a so-called configuration file that told TLC which properties to check (among other things). In that configuration file, the name "Simple!SimpleAllocator" is not allowed, hence the need for the definition. Actually, the Toolbox generates a TLA module and configuration file for you and also generates similar definitions to work around this limitation, but you as a user don't have to be aware of this.

Regards,
Stephan

[Pedro Paiva]

Alright, Stephan, thank you once again!

Regards,

Pedro

--
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@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.