How to run models on different modules in the same Spec

[Tony Zhang <nz...@xxxxxxxxxxx>]

I'm new to TLA and have been following the video lectures. However, I am encountering a problem with the toolbox in Lectures 6 and 7.

As per the instructions, I created the modules TwoPhase and PaxosCommit, under the same spec called TCommit, which also contains a module named TCommit.
However, I am only able to run models using initial predicate "TCInit" and next-state relation "TCNext" belonging to TCommit.

If I supply, for instance, "TPInit" and "TPNext" belonging to TPCommit as the Init and Next arguments of the model, errors are detected. Apparently it can't find the definitions "TPInit"and "TPNext"?

Any help is appreciated. Thank you!