TLA+ video course: Can't add invariants/property from imported module

[Dane Hillard]

In the video course, lecture 6, Leslie indicates to add an invariant to the model for the TwoPhase specification—namely, TCConsistent from the TCommit module. I have a specification open with TwoPhase as the root module, and as expected the toolbox is also showing the TCommit module because TwoPhase imports it. When I attempt to add the TCConsistent invariant, TLC indicates an error:

Unknown operator: 'TCConsistent'

I ran into this same limitation again in lecture 8 when attempting to add TCSpec as a property. I've attached a screenshot of my setup; the two modules contain exactly the content from the example repository, so perhaps I've done something else silly?

Toolbox version: 1.7.1

OS: macOS 12.2.1

Java: openjdk 18

[Markus Kuppe]

Hi Dane,

it's `TC!TCConsistent` because TwoPhase instantiates TCommit under `TC` on line 163.

Markus

[Dane Hillard]

Thanks Markus, that worked like a charm. What would have been the best place to learn this was the proper syntax?