[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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/cf66f27a-054f-4c3e-bc36-bb5463a99e49n%40googlegroups.com.