Definedness and satisfaction of disjunctions in numeric planning

[patrikhaslum]

While playing around with some numeric planning problem problems, I've come across some issues with VAL and/or the PDDL2.1 spec (specifically, the 2003 JAIR paper by Maria and Derek).

Question 1: Is a disjunction defined or satisfied in a state where some of the disjuncts are undefined?
For example, suppose an action precondition is: (or (p) (> (x) 0)). Is this action applicable in a state in which (p) is true and the value of the (ground) numeric fluent (x) is undefined?

VAL's answer is yes. (I've tested it with a number of variants, such as changing the order of the disjuncts, using imply instead of or, negating the undefined disjunct, and it comes up the same in every case.) If we place the undefined condition inside a negation instead of a disjunction, i.e., make the precondition (not (> (x) 0)), then VAL issues a warning ("Attempt to access undefined numeric expression!") and prints the somewhat cryptic status message "validator failed" (instead of the usual "plan failed") in the final summary.

However, the 2003 JAIR paper is quite vague on what is correct. The closest thing I've been able to find is definition 9, which says that "...each numeric comparison is interpreted using standard equality and ordering for the reals and logical connectives are given their usual interpretations. [...] Comparisons involving \bot [the symbol for the undefined value] ... are all undefined, so that enclosing propositions are also undefined and not satisfied in any state."

The question is: What is the definition that VAL implements for the meaning of compound formulas when some atomic subformula is undefined, and where can we find the basis for this this definition?

Question 2: What is 1/0?

VAL deems an action with the precondition (> (/ 1 (x)) 1) to be applicable in a state where (x) is 0. It seems most likely that VAL simply applies float operations and accepts the result whatever it is. (For example, the value of (x) after the assignment (assign (x) (- (/ 1 (x)) (/ 1 (x)))) in a state where (x) is zero is "-nan".)

This is slightly at odds with the 2003 JAIR paper, which states that the values of primitive numeric expressions (i.e., ground functions) in a state must be either reals or undefined.

[DerekLong101]

You are quite right that VAL is not as careful about these issues as it should be. I'll have a look at improving the handling of undefined numbers.