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?