Help with UI(?) problem working through TwoPhase lecture in course

[Dan Kortschak]

I have started working through the TLA+ course and have come to a part that I am unable to get to work. When I attempt to run the model for TwoPhase, I get errors that TPInit and TPNext are unknown operators (in image), despite them being defined in the TwoPhase.tla file (e.g. for TPInit in second image).

I suspect that I have misunderstood the instructions for how to set up the module at 4:40 in video 6. The approach that I took was to File→Open Module→Add TLA+ Module... I suspect that this is not the correct method, particularly since the TwoPhase.tla and TCommit.tla appear different (star on TCommit.tla but not on TwoPhase.tla — I have not been able to find the significance of this in the docs).

Can someone suggest what I have done wrong?

thanks

[Morgan Weetman]

Hi Dan,

I think many of us run into this issue, try this: https://groups.google.com/u/1/g/tlaplus/c/REfGFm9bJMU/m/BuJ9N8NnGwAJ

cheers

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d4a447ba-05dc-4c5b-a0bc-1791c8fc1d3bn%40googlegroups.com.

[Dan Kortschak]

Thanks, Morgan.

That has fixed the issue — I looked for a corrections note, but only on the page for the video, not on the corrections page where it clearly explains this. Now I know.

Dan