search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
443 stars 40 forks source link

[BUG] Deadlock detection may report false negatives #711

Open konnov opened 3 years ago

konnov commented 3 years ago

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

konnov commented 3 years ago

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

konnov commented 3 years ago

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