How to detect deadlock in mypyvy?

[gipsyh]

Dear developers of mypyvy,

I would like to inquire about how to detect deadlocks in mypyvy, which refers to situations where no actions can be executed.

Thank you.

[wilcoxjay]

As far as I know, nobody has done that in mypyvy yet.

The closest thing I can think of that is similar to what you are asking is the sat trace feature. We use it to ensure that actions can be executed in certain situations, which is a way of preventing accidental vacuity, where a typo causes an action to never be enabled.

Full deadlock detection is more complex than this, but perhaps it would give you a good start. You can see an example of using sat trace at the bottom of the lockserv example.

If sat trace is insufficient for your needs, then let's continue the discussion. Perhaps it wouldn't be too hard to add something to mypyvy to support what you want.