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
=============================================================================
----Hi,
This sounds like a potentially 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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/66188707-0c64-4d23-98d3-ede4f84fe1c7%40googlegroups.com.