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

Re: [tlaplus] Video lecture 6 (Two-Phase Commit)



Can you search a thread named 

“How to run models on deifferent modules in the same spec” 

I think you are facing the similar problem. I short yes you have to create a new spec.

Thanks
Maneet

On Fri, Aug 3, 2018 at 7:05 AM Sebastian Hunt <howswiftlyd...@xxxxxxxxx> wrote:
Just starting out with the toolbox and enjoying the lectures. But I did hit a snag. The lecture 6 instructions to create a spec for Two-Phase Commit say:

"In the Toolbox, create a new module named TwoPhase in the same folder as TCommit."

Since I was following on immediately from Lecture 5, I already had the TCommit spec open in the toolbox. So I did:

File > Open Module > Add TLA+ Module

and carried on my merry way. But, when I created a new model, the toolbox complained that the names "TPInit" and so on were "unknown operators".

It seems it is necessary to create a new TwoPhase *spec* rather than just a new module.

Am I right in thinking then that a model can only refer directly to the names declared and defined (and "included") in the root module of a spec, not those of any other module? This would seem reasonable, if so, but somehow it was not clear to me.

Seb

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
--
Regards
Maneet Bansal