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

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

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

On Monday, May 1, 2023 at 5:11:55 PM UTC+9:30 Morgan Weetman wrote:

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

On Mon, May 1, 2023 at 5:01 PM 'Dan Kortschak' via tlaplus <tla...@xxxxxxxxxxxxxxxx> wrote:

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

-- 
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/2beb038e-3fd8-4ad9-a192-af7db5a79613n%40googlegroups.com.