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

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

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,

On Thursday, October 19, 2017 at 5:56:01 PM UTC-4, Hillel Wayne wrote:
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")