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

["'Dan Kortschak' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>]

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

-- 
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/d4a447ba-05dc-4c5b-a0bc-1791c8fc1d3bn%40googlegroups.com.

Attachment: Screenshot 2023-05-01 at 16.15.44.png
Description: PNG image

Attachment: Screenshot 2023-05-01 at 16.21.17.png
Description: PNG image