[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Re: Reproducing deadlock in TLA+
I'm new to TLA and it looks like deadlock was a wrong term to use. What I wanted to see is a report of EventualSuccess violation. My reasoning was that it is violated when only stuttering steps occur. I thought that maybe TLA needs non-stuttering steps. To check I've added a 'time' variable and an action which increments it. It didn't work: model checking doesn't finish. I'm clearly doing something wrong.
I was able to reproduce the situation when one of the treads never tries to lock by by introducing an additional variable 'dead' (a function from Thread to BOOLEAN), an additional step for thread to die, and an enabling condition that a dead thread cannot become a victim. Is it the right way to model the situation when one of the threads never tries to lock? Is the EventualSuccess formula a wrong thing to check in this spec? Are there any examples of the spec where a similar property is violated?
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAC%2BL6n09md_5UN6rxKTsj6zG%3Dc2DSAdbQvwoTp-fZ-AguupZ%3Dg%40mail.gmail.com.