# Re: [tlaplus] Re: "Uknown Operator" in refinement mapping

That does seem to do what I want. Thank you!

I did some reading to figure out what I had misunderstood, so I'll post the findings of that here in case someone has a similar issue in the future.

I was basing myself on the example on page 6 and 7 here: https://lamport.azurewebsites.net/tla/hiding-and-refinement.pdf. In that example the lines

F == INSTANCE FIFO WITH queue <- qG \o qP
THEOREM Spec => F!Spec

appear in the module FIFO2 which contains a formula named Spec. HOWEVER there is also a formula called Spec in the module FIFO, and this is the one being referenced by the last Spec in the above theorem.

My error is exactly the same. The last HashmapSpec in Stephan's solution actually refers to a formula with the same name in the module hashmap. (I am changing my naming to avoid this trap again)

Thanks for the help!

On Tuesday, April 7, 2020 at 3:09:11 PM UTC+2, Stephan Merz wrote:
I think you want to write

THEOREM SOSpec => HashmapSpec!HashmapSpec

The formula SOSpec is defined in the module that introduces the refinement, not in the one for the high-level spec.

Stephan

On 7 Apr 2020, at 15:00, Åsmund Kløvstad <aqis...@xxxxxxxxx> wrote:

Hi, thank you for the response.
Here is a minimal example using the same hashmap spec and a very minimal SOSpec that gives me the same error.

- Åsmund

On Monday, April 6, 2020 at 11:24:34 PM UTC+2, loki der quaeler wrote:
Hi,

This sounds potentially like a parsing bug; could you provide a fully contained MODULE file in which this is reproducible?

Thanks - loki

On Monday, April 6, 2020 at 3:57:33 AM UTC-7, Åsmund Kløvstad wrote:
Hi,

I am working on a refinement mapping and getting an error I do not understand.

I'm attempting to show that SOSpec implements the spec hashmap and I've got the following in the module that contains SOspec:

(**************************)
(*Split-order spec        *)
(**************************)
SOSpec == SOInit /\ [][SONext]_<<keys, list, buckets, size, count>>

(*********)
(*A refinement mapping of the hashmap spec with the map defined by the SOFind action*)
(***********)
HashmapSpec == INSTANCE hashmap WITH map <- [k \in PossibleKeys |-> SOFind(k)]

(********************************)
(*Split-order implements hashmap*)
(********************************)
THEOREM SOSpec => HashmapSpec!SOSpec

The toolbox is giving me the error "Unknown Operator: SOSpec" after the bang on the last line. (And the same error if I try to check the property HashmapSpec!SOSpec with TLC)

It seems to me like SOSpec is very clearly defined a few lines earlier, so what does this error mean?

--
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 tla...@googlegroups.com.