Hello,
> On 16 Feb 2018, at 21:10, Pedro Paiva <pedr...@xxxxxxxxx> 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.
--
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...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus .
For more options, visit https://groups.google.com/d/optout .