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

[Jose Ayerdis <josea...@xxxxxxxxx>]

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")