"Uknown Operator" in refinement mapping

[Åsmund Kløvstad]

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?

[loki der quaeler]

Hi,

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

Thanks - loki

[Hillel Wayne]

I was able to reproduce it with this minimal set of files:

------------------------------ MODULE abstract ------------------------------
VARIABLES x

Init ==
  /\ x = FALSE

Next == TRUE

Spec == Init /\ [][Next]_x

=============================================================================

-------------------------------- MODULE main --------------------------------
VARIABLE x

Abstract == INSTANCE abstract

Refinement == abstract!Spec

=============================================================================

On 4/6/2020 4:24 PM, loki der quaeler wrote:

Hi,

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

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/66188707-0c64-4d23-98d3-ede4f84fe1c7%40googlegroups.com.

[Leslie Lamport]

Hillel's example does not show a bug in anything but the spec.  Look 

below to see why.

Leslie

[Hillel Wayne]

*headdesk*

This is not one of my prouder moments in life.

(After fixing that I couldn't reproduce)

--

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/379f3349-7b39-4067-9065-a84409a63aaa%40googlegroups.com.

[Åsmund Kløvstad]

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

[Stephan Merz]

 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

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5794ed15-b774-4acd-81c0-b464924fa4cf%40googlegroups.com.
<minimal.zip>

[Åsmund Kløvstad]

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!

Stephan

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.