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

*From*: Åsmund Kløvstad <aqissiaq@xxxxxxxxx>*Date*: Tue, 7 Apr 2020 07:00:35 -0700 (PDT)*References*: <5ea69a07-1f03-46fb-8a28-7fa7037dfa17@googlegroups.com> <66188707-0c64-4d23-98d3-ede4f84fe1c7@googlegroups.com> <5794ed15-b774-4acd-81c0-b464924fa4cf@googlegroups.com> <E22C2A19-C580-4630-9287-DC141E808B63@gmail.com>

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 writeTHEOREM SOSpec => HashmapSpec!HashmapSpec

The formula SOSpec is defined in the module that introduces the refinement, not in the one for the high-level spec.StephanOn 7 Apr 2020, at 15:00, Åsmund Kløvstad <aqis...@xxxxxxxxx> wrote: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.- ÅsmundOn 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!SOSpecThe 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>

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/2bdd81e3-8538-4c80-9263-ff42bb4217c7%40googlegroups.com.

**References**:**[tlaplus] "Uknown Operator" in refinement mapping***From:*Åsmund Kløvstad

**[tlaplus] Re: "Uknown Operator" in refinement mapping***From:*loki der quaeler

**[tlaplus] Re: "Uknown Operator" in refinement mapping***From:*Åsmund Kløvstad

**Re: [tlaplus] Re: "Uknown Operator" in refinement mapping***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: "Uknown Operator" in refinement mapping** - Next by Date:
**Re: [tlaplus] Q on prophecy vars again** - Previous by thread:
**Re: [tlaplus] Re: "Uknown Operator" in refinement mapping** - Next by thread:
**[tlaplus] Q on prophecy vars again** - Index(es):