Summary: find_matching_del_effect needs to check that the atom of the matching
delete effect must be true whenever the action is applied.
Here the details for the task of this issue:
The invariant synthesis finds an (invalid) mutex group
Atom enabled-philosopher-2-forks--pid-rfork()
Atom advance-tail-forks-3-()
Atom queue-tail-forks-3--qs-0()
Atom blocked-trans-philosopher-2-forks--pid-rfork().
For this mutex group it passes the balance check for actions
block-read-queue-empty-philosopher-2-forks--pid-rfork-forks-2--fork-zero-0
advance-empty-queue-tail-forks-3--queue-1-qs-0-qs-0-fork-fork-zero-one-0
block-read-wrong-message-philosopher-2-forks--pid-rfork-forks-2--fork-empty-0
queue-read-philosopher-2-forks--pid-rfork-forks-2--fork-0
queue-write-philosopher-3-forks--pid-wfork-forks-3--fork-0
advance-empty-queue-tail-forks-3--queue-1-qs-0-qs-0-fork-empty-zero-one-0
queue-write-philosopher-2-forks-__-pidp1__4_-wfork-forks-3--fork-0
among which at least
queue-write-philosopher-3-forks--pid-wfork-forks-3--fork-0 and
queue-write-philosopher-2-forks-__-pidp1__4_-wfork-forks-3--fork-0
seem fishy.
For both actions, no fact from the mutex group occurs as precondition.
Both actions have an add effect advance-tail-forks-3- and a delete
effect blocked-trans-philosopher-2-forks--pid-rfork that is matched
to this add effect, so for the balance checker the actions are balanced.
The problem is that find_matching_del_effect does not check that
blocked-trans-philosopher-2-forks--pid-rfork must have been true when the action
is applied, which is indeed not the case, leading to an invalid mutex group.
|