[BUG] Deadlock detection may report false negatives

[konnov]

No deadlock detected, though TLC reports a deadlock

Input specification

See #110

The command line parameters used to run the tool

apalache check EWD840.tla

Expected behavior

A deadlock must be reported, see #110

System information

• Apalache version 0.15.1

[konnov]

No deadlock is reported in version 0.11.0. It must have been broken a while ago.

[konnov]

@lemmy it is not exactly an implementation bug. This is how we report deadlocks in symbolic execution: If for some k, there is no k+1-th extension of a symbolic path. In this spec, there is always a symbolic extension (you can apply SendMsg). But there is indeed a concrete state that has a deadlock.

It is true that this is not precisely deadlock detection, but a less precise version of deadlock detection. I have to think how to make it work for all the cases, when TLC can find a deadlock. Most likely, this will require us to deal with ENABLED, which requires additional constraints. So it should be definitely harder to find a deadlock in Apalache than in TLC.