[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.
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.
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.