How to terminate or explicitly set a pc to "done" in pluscal

[Jose Ayerdis]

Hi this is kind of a noob question, just starting with tla+ and I'm doing a very simple synchronous consensus spec, my problem is that when I run my spec it enters a deadlock due to the fact that one node is unable to enter node because it fail.

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.

I have a temporal clause that is define such that terminate once everyone that are up have terminated (t)

ConsistentTermination == <>[](\A j \in UpNodes: t[j]=TRUE ) 

But the translated termination from tla+ is still reaching a deadlock. (Is there a way to ignore or not allow it to be check and instead check only the one above)

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

[Hillel Wayne]

You can disable deadlocks in the toolbox (it's above the "invariants" section); however, I'm not sure what the issue you're facing is. Would you be able to share a copy of your spec?

[Jose Ayerdis]

That worked, also I read from the pluscal manual

"The last disjunct of Next is added for TLC’s benefit. TLC has no way of distinguishing deadlock from termination, which is simply a desired form of deadlock."

Thanks for the help,

[Stephan Merz]

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