OK, there is breakage here both in terms of implementation and in terms of
concepts. I'll only describe the conceptual breakage, since it doesn't matter
much if an implementation of a broken concept is broken -- we need to come up
with a better concept anyway.
The basic problem is that currently, abstraction A may say that there is no need
to distinguish actions a and b, so they can be merged, and abstraction B may say
that there is no need to distinguish actions a and c, so they can be merged. But
then we lose the power to distinguish b and c, which we might need to. Well,
that's simplified a lot, but anyway.
More precisely, the current implementation is based on the idea that abstraction
A does not need to distinguish two operators which behave identically on all
variables not represented in A. Let's call such operators A-equivalent. The idea
is that instead of arcs labeled with operators, we have arcs labeled with
A-equivalence classes. The current implementation doesn't actually implement
that properly, but if it did, it would clearly give an overapproximation of the
real problem (since we're only adding synchronization labels by going from
operators to equivalence classes), and the question is whether or not that
overapproximation is strict (which would be undesirable).
The answer is yes. Consider a task with three variables a, b, c each with domain
{0, 1, 2}, initial value 0 and goal 2. There are seven operators: all have
precondition a=0,b=0,c=0, and all change a, b and c to some value in {1, 2}. We
write these operators as o_ijk, where i,j,k in {1, 2} are the values that a,b,c
are set to. Of the eight possible operators of that form, all are present except
for the one that sets a=2,b=2,c=2 (o_222). The task is clearly unsolvable.
However, here's what happens if we do label simplification:
Originally (we denote parallel arcs by commas):
Abs_a: 0 ---o_111,o_112,o_121,o_122--> 1
0 ---o_211,o_212,o_221--------> 2
Abs_b: 0 ---o_111,o_112,o_211,o_212--> 1
0 ---o_121,o_122,o_221--------> 2
Abs_c: 0 ---o_111,o_121,o_211,o_221--> 1
0 ---o_112,o_122,o_212--------> 2
After label simplification:
Abs_a: 0 ---{o_111,o_211},{o_112,o_212},{o_121,o_221},{o_122}--> 1
0 ---{o_111,o_211},{o_112,o_212},{o_121,o_221}----------> 2
Abs_b: 0 ---{o_111,o_121},{o_112,o_122},{o_211,o_221},{o_212}--> 1
0 ---{o_111,o_121},{o_112,o_122},{o_211,o_221}----------> 2
Abs_c: 0 ---{o_111,o_112},{o_121,o_122},{o_211,o_212},{o_221}--> 1
0 ---{o_111,o_112},{o_121,o_122},{o_211,o_212}----------> 2
We then merge Abs_a and Abs_b (or any other two -- due to symmetry, it doesn't
matter):
Abs_ab: 0,0 --o_111,o_112,o_121,o_122,o_211,o_212,o_221--------> 1,1
0,0 --o_111,o_112,o_121,o_122,o_211,o_221--------------> 1,2
0,0 --o_111,o_112,o_121,o_211,o_212,o_221--------------> 2,1
0,0 --o_111,o_112,o_121,o_211,o_221--------------------> 2,2
After label simplification:
Abs_ab: 0,0 --{o_111,o_121,o_211,o_221},{o_112,o_122,o_212}----> 1,1
0,0 --{o_111,o_121,o_211,o_221},{o_112,o_122,o_212}----> 1,2
0,0 --{o_111,o_121,o_211,o_221},{o_112,o_122,o_212}----> 2,1
0,0 --{o_111,o_121,o_211,o_221},{o_112,o_122,o_212}----> 2,2
Merging this with Abs_c, we get the spurious connection 0,0,0->2,2,2.
|
OK, seeing clearer. This is indeed a logic problem. With the example, it arises
in the last merge step, when merging varset {0,2,3} with varset {1} (all counts
are with respect to the numbering introduced by the preprocessor, not translator).
Label simplification finds the following equivalences for {0,2,3}:
o_0 ~ o_1 ~ o_3, o_2 ~ o_4, o_5 ~ o_6 ~ o_7 ~ o_8
and the following equivalences for {1}:
o_2 ~ o_5, o_4 ~ o_6
Moreover, the following operators are irrelevant for {1}:
o_0, o_1, o_3.
The equivalences mean that the abstraction for {0, 2, 3} has no arcs for
operators o_1, o_3, o_4, o_6, o_7 and o_8, while the abstraction for {1} has no
arcs for operators o_5 and o_6. Hence, we only get matches for operators o_0
(present in {0, 2, 3} and irrelevant in {1}) and o_2 (present in both). This
means that all operators not equivalent to these in either abstraction (namely,
o_6, o_7 and o_8) are lost. The problem become unsolvable because one of the
operators o_7 and o_8 is needed in every plan.
One example of a solution for the problem would be o_0, o_2, o_7.
How to fix this? Will need to rethink how and when exactly the label
simplifications should be applied.
|