Issue810

Title Bug in invariant synthesis
Priority bug Status resolved
Superseder Nosy List gabi, malte
Assigned To gabi Keywords translator
Optional summary

Created on 2018-08-10.11:15:48 by gabi, last changed by malte.

Files
File name Uploaded Type Edit Remove
example.py gabi, 2018-12-05.13:57:27 text/x-python
Messages
msg8148 (view) Author: gabi Date: 2018-12-05.13:57:27
I had a closer look into this and there is no such bug. Method ensure_cover
(indirectly) calls get_assignment for every part, which correctly constraints
the non-counted variables.

I attached a python file with the example from the bug report and verified that
we indeed get the correct behavior.
msg7339 (view) Author: gabi Date: 2018-08-10.11:15:48
This bug has been reported to the Fast Downward mailing list by Masataro Asai a
while ago. The implementation of ensure_covers is not correct. For the renaming
that allows to cover the effects, we need constraints on the parameters of the
invariant, not on the counted variable.

Masataro's original email:

I stopped reimplementing AIJ09 paper, but when I reviewed it today, I found the
definition of covers(V,phi,psi) is incorrect and different from the source code.
While the paper says "counted variables (those not in V)", it is actually
parameterized variables (those in V) that are subject to renaming.

I show this from two direction (source code and examples).

In InvariantPart (each atom in the invariant), "order" O is a list of index.
When p[i] is the i-th parameter of the invariant, O[i] is an index of p[i] in
the arguments of the atom. Therefore O does not contain the index for counted
variables.

In ensure_cover -> invariant.get_covering_assignments -> part.get_assignment,
"equalities" collects the equality (renaming/alias/assignment) constraints for
each index in O. This means the constraints are on parameters, not on counted
variables.

In fact, in the example shown in p22,

  Precondition: at(x, l1 ) ∧ at(x, l2 )
  Add effects: at(x, l3 ) ∧ at(x, l4 )

the text says the case l1 = l2 and l3 != l4 is problematic. However, what we
actually get by following Fig.7 for an invariant ∀?thing (at ?thing ?counted) is
something like

(AND (OR (!= ?X ?X) (!= ?L3 ?L4)) ; for ensure_equality
     (== ?L3 ?COUNTED) ; for ensure_cover with e.atom
     (== ?L4 ?COUNTED) ; for ensure_cover with e'.atom
     ;; for ensure_conjunction_sat
     (OR (!= ?X ?X) (!= ?L1 ?L3))
     (OR (!= ?X ?X) (!= ?L1 ?L4))
     (OR (!= ?X ?X) (!= ?L2 ?L3))
     (OR (!= ?X ?X) (!= ?L2 ?L4)))

Here, (!= ?L3 ?L4) and (== ?L3 ?COUNTED) and (== ?L4 ?COUNTED) is a
contradiction and is never satisfied.

Instead, the correct result is

(AND (OR (!= ?X ?X) (!= ?L3 ?L4)) ; for ensure_equality
     (== ?X ?THING)  ; for ensure_cover with e.atom
     (== ?X ?THING)  ; for ensure_cover with e'.atom
     ;; for ensure_conjunction_sat
     (OR (!= ?X ?X) (!= ?L1 ?L3))
     (OR (!= ?X ?X) (!= ?L1 ?L4))
     (OR (!= ?X ?X) (!= ?L2 ?L3))
     (OR (!= ?X ?X) (!= ?L2 ?L4)))

In this case, there is a solution (== ?L1 ?L2 ?V1), (== ?L3 ?V2), (== ?L4 ?V3),
(== ?X ?THING) which makes the operator too heavy.
History
Date User Action Args
2018-12-05 14:27:09maltesetnosy: + malte
2018-12-05 13:57:27gabisetstatus: unread -> resolved
assignedto: gabi
messages: + msg8148
files: + example.py
2018-08-10 11:16:08gabisetkeyword: + translator
2018-08-10 11:15:48gabicreate