On Thursday, May 26, 2022 at 12:00:50 AM UTC-4 Markus Alexander Kuppe wrote:
Hi Dane,
it's `TC!TCConsistent` because TwoPhase instantiates TCommit under `TC` on line 163.
Markus
> On May 25, 2022, at 5:49 PM, Dane Hillard <dane.h...@xxxxxxxxxx> wrote:
>
> 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
>
> <Screen Shot 2022-05-25 at 20.37.29.png>