[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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.