Re: [tlaplus] How to terminate or explicitly set a pc to "done" in pluscal

[Stephan Merz <stepha...@xxxxxxxxx>]

My question is is there a way I can set pc="DONE" or how to make it terminate once I know that they have reached a concensus.

In order to answer this specific question, you can always insert

  goto Done

in your PlusCal algorithm, even if there is no explicit label 

  Done: ...

Also, if it is irrelevant for your algorithm, there is no need to check the Termination property that the PlusCal translator generates: it is perfectly reasonable to verify some specific temporal property that expresses that your algorithm has terminated.

Stephan