Issue335

Title Translate fails with "negated axiom" error
Priority bug Status resolved
Superseder Nosy List gabi, malte, patrik, ronwalf, rpgoldman, ukuter
Assigned To malte Keywords
Optional summary

Created on 2012-05-14.02:34:08 by rpgoldman, last changed by malte.

Files
File name Uploaded Type Edit Remove
cntr-domain-edited.pddl rpgoldman, 2012-05-14.02:34:46 application/octet-stream
cntr-domain-partial-diagnosis.pddl rpgoldman, 2012-05-17.19:56:47 application/octet-stream
cntr-domain.pddl rpgoldman, 2012-05-14.02:34:58 application/octet-stream
cntr-problem.pddl rpgoldman, 2012-05-17.17:51:01 application/octet-stream
mst.pddl patrik, 2014-08-08.09:22:27 application/octet-stream
mst2.pddl patrik, 2014-08-08.09:24:09 application/octet-stream
robot_domain_bad.pddl ronwalf, 2013-03-09.22:19:48 application/octet-stream
robot_problem.pddl ronwalf, 2013-03-09.22:20:06 application/octet-stream
Messages
msg3291 (view) Author: malte Date: 2014-08-09.10:37:25
> The purpose of the "indirect-path" precondition in the remove operator is to
> ensure that an edge can only be removed if it does not disconnect the two
> nodes.

I see -- I thought yesterday that this would somehow limit the set of solutions
you could get, but I guess it doesn't limit you in any way that would be a
worry, i.e., only rules out stupid actions. In particular, an optimal solution
would never want to disconnect something.
msg3290 (view) Author: patrik Date: 2014-08-09.10:33:58
Hi Malte,

Thanks for the quick fix! Now it only runs out of memory. (It still does with
even with the new definition of is-a-forest. With this, the only negated axiom
is path, but that seems to be enough.)

The purpose of the "indirect-path" precondition in the remove operator is to
ensure that an edge can only be removed if it does not disconnect the two nodes.
(In the same way, the no-path precondition of the add operator is to ensure that
an edge can only be added if it connects two previously disconnected
components.) This is checked by checking that there is a path that does not
traverse the edge. I couldn't think of a better way to do it.
msg3282 (view) Author: malte Date: 2014-08-08.11:44:20
Hi everyone,

looking at the history of this issue, I'm sorry that it has been
lingering so long. I quickly tend to forget planner-related TODOs if
I'm not triggered by emails, so in general if there's a bug that
bothers you and I'm the one it's assigned to, please don't hesitate to
send a reminder if there's no activity for more than a few weeks.
(Only if you want, of course -- it's not your job to work around my
poor task management, but it might help resolve some issues that you
care about more quickly.)

Thanks a lot, Patrik! I think this is the same issue as before. The
source seems to be that negations of statically true axioms were never
implemented. Whether these axioms occur natively in the PDDL or are
created internally to represent complex action preconditions (or
similar) doesn't make a difference there.

I've made a change that might resolve this, but I'm not really sure if
the solution is correct because it must have been more than 10 years
since I last touched this part of the code, and I don't remember it
well. With the change, at least I don't get errors with any of the
examples you provided any more.

Going through the various examples you attached:

- For Robert's original monster-catching problem (cntr-domain.pddl,
  cntr-problem.pddl), I now find a 37-step plan (with --search
  "astar(blind())") which VAL accepts. Ditto when using
  cntr-domain-edited.pddl instead of cntr-domain.pddl. With
  cntrl-domain-partial-diagnosis.pddl, the search component claims
  there's no solution, which is probably plausible, given that this is
  the minimized domain file with lots of actions commented out.

- Ron's robot problem doesn't parse any more with the most recent
  translator. I get the error message "Undeclared predicate:
  htn_used_block". If I add a declaration for this predicate, I can
  translate the problem after the change, and the planner claims there
  is no solution. Is this correct?

- Patrik's MST problem really causes the translator to explode.
  Patrik, I think this would make a nice test case to show that
  certain algorithmic decisions in the translator should be revisited.
  I would like to open a new issue for this and add you to the nost list,
  but of course feel free to remove yourself if you don't want to follow
  this.

  To handle the task, I need to reduce it to two states (Australian
  states, that is :-)). Then it seems to work, but it's hard to really
  test it with this problem size because cycles aren't possible.

  BTW, here's an alternative formulation of the "is-forest" predicate
  that might be simpler:

  - repeatedly mark each vertex that has at most one unmarked
    neighbor; something like: derive (marked ?x) if

     (not (exists (?y ?z) (and
         (not (= ?y ?z))
         (edge ?x ?y) (not (marked ?y))
         (edge ?x ?z) (not (marked ?z)))))

  - we have a forest iff every vertex is marked

  If you also get rid of "indirect-path" (which I don't think is
  strictly needed; and is it even correct to use it in the
  precondition? why not allow removing the direct edge instead?), maybe it
  won't blow up so much any more.

Gabi has also had a look at the change and agrees with it, but isn't
familiar with the surrounding code either. I've pushed the change to
the main repository and am closing this, but of course, feel free to
reopen if the problem isn't resolved.

Cheers,
Malte
msg3281 (view) Author: patrik Date: 2014-08-08.09:22:27
Here is a another example that triggers the same fault. However, I believe this
example is different from the others. It has no complex operators with
conditional effects (in fact, it still fails if all operators are commented
out); the axioms (including the failing one) is part of the domain, not
generated by the translator.

It seems that the cause of the problem is that when the negation of a derived
proposition is used (in another axiom), a "negated axiom" for deriving the
negation of the proposition is created. But if the proposition is derived by an
axiom with empty body (like the base cases in path and path-not-through in this
example), then no such negated axiom can be formed, and the translator fails. If
this is indeed the problem, I guess adding a statically false proposition to the
condition of the negated axiom would solve it.
msg2399 (view) Author: ronwalf Date: 2013-03-09.22:19:48
I've attached another example.  It's still not very minimal (sorry).
You can change the last clause of the action "finished" from:
(forall (?obj - PACKAGE ?loc - ROOM) (and (goal_in ?obj ?loc) (in ?obj ?loc))
To its more correct form
(forall (?obj - PACKAGE ?loc - ROOM) (imply (goal_in ?obj ?loc) (in ?obj ?loc))
and FD no longer throws the translation error.
msg2221 (view) Author: malte Date: 2012-05-17.20:36:49
A literal that appears in a conditional add effect and a conditional delete
effect is problematic for the planner; it may or may not work.

The same literal appearing multiple times under different conditions should be fine.
msg2220 (view) Author: rpgoldman Date: 2012-05-17.20:04:29
Please remind me: am I correct in thinking that each literal must appear in at 
most one of the conjuncts of an effect?

And is it OK to have the literal appear positively in one effect and negatively 
in another?

I have a vague memory of a limitation like this.
msg2219 (view) Author: rpgoldman Date: 2012-05-17.19:56:08
Partial results.  If one looks at the cntr-domain-partial-diagnosis.pddl, you 
can see two comments that start with "HERE:" that shows a combination of actions 
that seem to be critical to breaking the translator.  Removing one of them is 
sufficient to make the parse pass.

One of them does have a conjunction of two negated literals as precondition.

I will look further for a smaller culprit.
msg2218 (view) Author: rpgoldman Date: 2012-05-17.18:23:01
OK, will do.
msg2217 (view) Author: malte Date: 2012-05-17.18:20:26
I had a first look at what is going on, but it's difficult to see if the error
is at the spot where the assertion throws or whether that part of the code gets
bogus input from other parts for some reason.

Would it be possible to trim the example (removing objects, operators,
conditions etc.) in such a way that the error still occurs, but it is smaller?
Right now there are 128666 grounded axioms, so it's hard to see what they do.

I could have a shot at that reduction too, but I don't have enough time today
(have to pepare a lecture for tomorrow). Maybe it's easier for you since you
know the domain?
msg2216 (view) Author: rpgoldman Date: 2012-05-17.17:51:12
Sorry!  Stupid oversight!
msg2215 (view) Author: malte Date: 2012-05-17.17:47:29
Thanks for the report! Can you attach a problem file?
msg2211 (view) Author: rpgoldman Date: 2012-05-14.03:01:22
It seems to be the following bit in the final operator:

    ; (FORALL (?O - OBSTACLE)
    ;   (WHEN (COMPROMISED ?O)
    ;       (NOT (COMPROMISED ?O))))
     ; (FORALL (?O - OBSTACLE)
     ;  (WHEN (COMPROMISE-ITEM ?O ?I)
     ;        (NOT (COMPROMISE-ITEM ?O ?I))))

(commenting this out makes translate work ok)

It's not obvious to me why this fails, since it seems like a standard PDDL idiom 
for "turn off all of a set of predicates that are on."  But I didn't write this 
domain, so I don't claim to understand it fully.
msg2210 (view) Author: rpgoldman Date: 2012-05-14.02:34:08
The attached domain and problem fail with an error (violated assertion) as 
follows:
AssertionError: Negated axiom impossible; cannot deal with that: (new-axiom@12 
tieable l1 log1 l9) axiom effect: Atom new-axiom@12(tieable, l1, log1, l9)

[I expanded the assertion error message a little -- before it didn't specify the 
failing axiom.]
History
Date User Action Args
2014-08-09 10:37:32maltesetstatus: chatting -> resolved
2014-08-09 10:37:25maltesetmessages: + msg3291
2014-08-09 10:33:58patriksetstatus: resolved -> chatting
messages: + msg3290
2014-08-08 11:44:20maltesetstatus: chatting -> resolved
nosy: + gabi
messages: + msg3282
2014-08-08 09:24:09patriksetfiles: + mst2.pddl
2014-08-08 09:22:27patriksetfiles: + mst.pddl
nosy: + patrik
messages: + msg3281
2013-03-09 22:20:06ronwalfsetfiles: + robot_problem.pddl
2013-03-09 22:19:48ronwalfsetfiles: + robot_domain_bad.pddl
nosy: + ronwalf
messages: + msg2399
2012-05-17 20:36:49maltesetmessages: + msg2221
2012-05-17 20:04:29rpgoldmansetmessages: + msg2220
2012-05-17 19:56:47rpgoldmansetfiles: + cntr-domain-partial-diagnosis.pddl
2012-05-17 19:56:08rpgoldmansetmessages: + msg2219
2012-05-17 18:23:01rpgoldmansetmessages: + msg2218
2012-05-17 18:20:26maltesetmessages: + msg2217
2012-05-17 17:51:12rpgoldmansetmessages: + msg2216
2012-05-17 17:51:01rpgoldmansetfiles: + cntr-problem.pddl
2012-05-17 17:47:29maltesetassignedto: malte
messages: + msg2215
2012-05-14 03:01:22rpgoldmansetstatus: unread -> chatting
messages: + msg2211
2012-05-14 02:34:58rpgoldmansetfiles: + cntr-domain.pddl
2012-05-14 02:34:46rpgoldmansetfiles: + cntr-domain-edited.pddl
2012-05-14 02:34:08rpgoldmancreate