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?
On Thursday, 19 October 2017 15:26:14 UTC-5, Jose Ayerdis wrote: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")