Hi Pedro,
> On 19 Feb 2018, at 22:09, Pedro Paiva <pedr...@xxxxxxxxx> 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
--
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 .