Two errors in handling of derived predicates

[patrikhaslum]

I have found two errors in VAL's handling of derived predicates.

I'll attach/upload the following PDDL files which exhibit the errors (if that's possible):

blocker-strips.pddl: Domain file.
blocker-strips-small.pddl Sample problem #1.
blocker-strips-small.soln (Valid) Plan for sample problem #1.
blocker-strips-12.pddl Sample problem #2.
blocker-strips-12.soln (Valid) Plan for sample problem #2.

The errors are as follows:

1. The computation of the stratification is not correct. Every dp ends up in the same stratum, even when they should not. (This happens with both sample problems above.) The cause of this error is that the procedure that checks whether a dp occurs in the body of an axiom uses DerivationRules::NNF (defined in Validator.cpp), which attempts to use "goal( const goal& )" as a copy constructor for arbitrary goal subclasses. This does not work: the construction "new goal( *g )" returns a object of class "goal", which is an abstract parent class of all goal types, and therefore itself not recognised as any goal type.

   Fixing the NNF conversion procedure fixes this problem. However, the NNF conversion looks like it is intended to do a complete deep copy of the goal (because the goal it returns is deleted by the function that calls it, occurNNF). I'm not sure if this is actually guaranteed by the NNF conversion (even after correction). It may be safer not to delete the NNF-converted goal formula. This will entail some memory leakage, but it's relatively small (stratification is only done once, I believe).

2. The evaluation of a derived predicate in the problem goal (at the end of plan execution) appears to run into an infinite loop. This happens regardless of whether stratification is correct or not. It only happens on sample problem/plan Patched to support clang++ and g++ 4.9.1 without compiler errors. #2, not on problem/plan VS Compilation #1 (though since both share the same domain, the have the same set of axioms). It also only happens when the validator checks the goal, not when it checks preconditions of actions.

[patrikhaslum]

It appears not to be possible to upload/attach test files here. Instead, they are now included in the inval distribution at http://users.cecs.anu.edu.au/~patrik/pddl/inval.tar.gz (under tests/axioms).

[DerekLong101]

Thanks for that, Patrik. I will take a look - your proposed fix is plausible, but I'd like to avoid the leak if I can. This machinery dates back to Richard Howey days and I will need to dig around to see if I can remember the details. Memory management in VAL is not as robust as I would have liked (and C++-11 would make a lot of things so much easier).

[patrikhaslum]

Avoiding the memory leak should not be too difficult: It seems that goal formulas, when deleted, recursively delete their parts, so the NNF conversion just has to make sure it does a full deep copy of the formula while transforming it. Then the returned formula can be deleted after use (in occurNNF).

[guicho271828]

@patrikhaslum It might be too late to come here, but I checked your sample files in the archive.
Maybe you are no longer interested in this topic, but I just want to leave a comment here for someone else that was interested.
First, couple of files have inconsistency in the action and the predicate names between the pddl and the solution files --- I attach the diff here

modified   tests/axioms/bw-axioms-THN.pddl
@@ -38,13 +38,13 @@
 	    (forall (?x - block)
 		    (not (holding ?x))))
 
-  (:action pick-up
+  (:action pickup
    :parameters (?ob - block)
    :precondition (and (clear ?ob) (ontable ?ob) (handempty))
    :effect (not (ontable ?ob))
    )
 
-  (:action put-down
+  (:action putdown
    :parameters (?ob - block)
    :precondition (holding ?ob)
    :effect (ontable ?ob)
modified   tests/axioms/bw-axioms-small.pddl
@@ -2,6 +2,6 @@
 (define (problem size-five) 
   (:domain blocksworld-with-axioms)
   (:objects A B C D E)
-  (:init (on-table A) (on B A) (on C B) (on-table D) (on E D))
+  (:init (ontable A) (on B A) (on C B) (ontable D) (on E D))
   (:goal (and (on A D) (on C B)))
   )

Second, some derived predicates in the files contain duplicated parameters which is not allowed in the PDDL2.2 paper. (Perhaps it implies equality between them, but this sounds nonstandard)

  ;; ?a has motive for (has ?a ?i) if ?a has motive for (has ?c ?i):
  (:derived (motive-for-has ?a - character ?a - character ?i - item)
	    (exists (?c - character)
		    (motive-for-has ?a ?c ?i)))

[patrikhaslum]

Hi Masataro,

The blocksworld domain (as per comment in the file) was modified to match the naming convention for the IPC 2000 instances and plans. You're right that the sample instance and plan in the inval repository do not match it.

However, the files triggering the errors in VAL are the blocker domain (not blocksworld). From a quick test with an up-to-date version of VAL, at least the second error (inf loop in goal evaluation) is still present.

I did not notice the requirement that variables have to be different (though, again, this does not occur in the domain file that triggers the errors). INVAL supports axioms with non-unique variables in the head, and it is indeed treated as a equality constraint.

[patrikhaslum]

PS. Should perhaps mention that INVAL is now on github: https://github.com/patrikhaslum/INVAL. The version in the archive linked to above is probably a bit old (though the mismatch between the blocksworld domain and instance/plan has not been fixed).

[guicho271828]

I think you did not include the sample files in the github INVAL repository.

BTW I plan to push to my own validator https://github.com/guicho271828/ArriVAL (the name comes from a pun about Lisp being a very ALIEN language...) I read some source code comments in INVAL and learned couple of new things about axioms (like maximum/minimum stratification).

[patrikhaslum]

You're right, the test case collection was not in the repository! It is now. (I also fixed the blockworld instance and plan.)