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

[tlaplus] Re: Unknown operator error during the TLA+ lectures

Thank you, that worked perfectly!

On Wednesday, February 6, 2019 at 8:21:56 PM UTC+1, neil.o...@xxxxxxxxx wrote:
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.



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?

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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.