Re: [tlaplus] Re: Reproducing deadlock in TLA+

[Dmitry Neverov <dmitry.neverov@xxxxxxxxx>]

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?

On Sat, Nov 16, 2019 at 2:22 AM Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:

On 15.11.19 17:10, Leslie Lamport wrote:
> Deadlock means reaching a state in which Next is not enabled.  A little
> simple logic shows that, for all t in Thread, in any state in which
> wasVictim[t] and owner[t] are Booleans, at least one of BecomeVictim(t),
> AcquireLock(t), and ReleaseLock(t) is enabled.
>


For such a small model, the Toolbox can also visualize the state graph
that shows no deadlock states.

M.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/rp5cE4IzEnM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/d64cf80a-43d0-e114-1f53-29aa49762034%40lemmster.de.

-- 
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.