Re: Unknown operator error during the TLA+ lectures

[neil.o...@xxxxxxxxx]

Hey Michael,

Yeah this is really confusing first time around :)

So you have created the new TwoPhase module inside the TCommit specification (File > Open Module > Add TLA+ Module > "TwoPhase").

To create a model that checks just the TwoPhase specification, you need to now create a brand new specification (File > Open Spec > Add New Spec). In this dialog, select the file TwoPhase.tla as your root-module. Leave the Specification name as TwoPhase.

This will create a new specification called TwoPhase, and will show both the TwoPhase.tla module and the TCommit.tla module within it (because TwoPhase implements TCommit via the INSTANCE keyword).

You can now create a model inside this new specification, and it should work as expected.

HTH,

Neil

On Wednesday, 6 February 2019 15:32:49 UTC, Michael Chonewicz wrote:

Hi. I'm following the TLA+ video lectures and I got to part 6 with TwoPhase Transaction. In the video I'm instructed to create a new spec, named TwoPhase in the same folder as the first spec, TCommit. No problem there. Then I'm supposed to create a new model where i have to fill in the initial predicate and next-state relation. This is the part that doesn't work. Even though i fill in TPInit and TPNext, the IDE tells me that these two are unknown operators.

I think this is because there is multiple specs and the second model assumes i still want to be working on TCommit spec. The fact that if I put the init predicate from the TCommit spec resolves this problem kind of confirms my theory. I have been looking for hours and i have not found a way of configuring which spec is supposed to be checked by the model.

What can I do to resolve this?