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?