Re: [tlaplus] TLA+ video course: Can't add invariants/property from imported module

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.hillard@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>

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/232C41FB-8485-42BB-B909-9D0BD72D45F3%40lemmster.de.