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:
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?
