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