Doubt about refinement

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