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