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?
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.