[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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


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:

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.