Video lecture 6 (Two-Phase Commit)

[Sebastian Hunt <howswiftlyd...@xxxxxxxxx>]

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