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