[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Video lecture 6 (Two-Phase Commit)
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.