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

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?

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.