Unknown operator error during the TLA+ lectures

[Michael Chonewicz <wawrzync...@xxxxxxxxx>]

Hi. I'm following the TLA+ video lectures and I got to part 6 with TwoPhase Transaction. In the video I'm instructed to create a new spec, named TwoPhase in the same folder as the first spec, TCommit. No problem there. Then I'm supposed to create a new model where i have to fill in the initial predicate and next-state relation. This is the part that doesn't work. Even though i fill in TPInit and TPNext, the IDE tells me that these two are unknown operators.

I think this is because there is multiple specs and the second model assumes i still want to be working on TCommit spec. The fact that if I put the init predicate from the TCommit spec resolves this problem kind of confirms my theory. I have been looking for hours and i have not found a way of configuring which spec is supposed to be checked by the model.

What can I do to resolve this?