Message from verifier complains about "Quantifiying over variable that is a method parameter"

[rpgoldman]

Here is the command:

pandaPIparser -V domain.hddl p01.hddl shop-plans/p01.hddl

(I will make all the files available)

Here's the output:

 Matching Task 36 Curpos=0 #sources=1
 Task is: ship-an-order o5
 Attempting matching with source __t_id_8
  Setting ?o = o5
   Unassigned variable ?p
      Quantifiying over variable that is a method parameter: ?p

Task 36 is as follows:

36 (ship-an-order o5) -> ship-an-order-1 8

Here is the task definition:

 (:task ship-an-order :parameters (?o - order))

Here's the definition of ship-an-order-1:

  (:method ship-an-order-1
    :parameters (?order - order ?avail ?new - count)
    :task (ship-an-order ?order)
    :precondition
    (and (goal-shipped ?order)
         (not (shipped ?order))
         (forall (?p - product) (imply (includes ?order ?p) (made ?p)))
         (stacks-avail ?avail)
         (next-count ?avail ?new))
    :ordered-subtasks
    (ship-order ?order ?avail ?new))

This seems to be related to the verifier not liking the quantified precondition. In the source, obviously, there is no method here, but I believe there's something in the transformation performed by pandaPIparser and/or pandaPIgrounder that is expanding this precondition into a method?

Gist with all the input files

[galvusdamor]

I found another issue that is strange: when I run the verifier without verbose output (with -v instead of -V), it produces a different result and notably does not stop.

pandaPIparser is configured as follows
  Colors in output: true
  Mode: plan verification
  Verbosity: 0
  Lenient mode: false
  Ignore given order: false

Checking the given plan ...
IDs of subtasks used in the plan exist: true
Tasks declared in plan actually exist and can be instantiated as given: true
Methods don't contain duplicate subtasks: true
Methods don't contain orphaned tasks: true
Task with id=35 is decomposed with method "make-product-1", but there is no such method.
Task with id=49 is decomposed with method "make-product-1", but there is no such method.
Task with id=54 is decomposed with method "make-product-1", but there is no such method.
Task with id=69 is decomposed with method "make-product-1", but there is no such method.
Task with id=74 is decomposed with method "make-product-1", but there is no such method.
Methods can be instantiated: false
Order of applied methods is under no matching compatible with given primitive plan.
Order induced by methods is present in plan: false
Plan is executable: unknown
Plan verification result: false

This error message also makes sense, as there is no such method and the mentioned IDs decompose different tasks (make-product-complex, make-a-product), which is impossible.

As for the error that you got: The id of the matching task is the ID of the subtask and not of the decomposition that we are currently evaluating. The number of the decomposition we are looking at is given one line before:

Generating Matchings for task with id=31
 Matching Task 36 Curpos=0 #sources=1
 Task is: ship-an-order o5
 Attempting matching with source __t_id_8
  Setting ?o = o5
   Unassigned variable ?p
      Quantifiying over variable that is a method parameter: ?p

The problem lies in the decomposition that is applied to task id=31, which is this method.

  (:method one-step-ship-order
    :parameters (?o - order ?p - product)
    :task (one-step)
    :precondition
    ;; prefer to ship an order, if possible...
    (and (goal-shipped ?o)
         (not (shipped ?o))
         ;; if we must, we could maintain this predicate
         ;; to avoid use of FORALL.
         ;; (ready-to-ship ?o)
         (forall (?p - product) (imply (includes ?o ?p) (made ?p)))
         (started ?o))
    :ordered-subtasks
    (ship-an-order ?o))

The problem here is the variable ?p that is quantified over in the precondition - the variable has already been defined as a parameter of the method - which is not allowed. The variables used in quantification are always local variables.

I've also just fixed the mismatch in error between -v and -V.

[rpgoldman]

The problem here is the variable ?p that is quantified over in the precondition - the variable has already been defined as a parameter of the method - which is not allowed. The variables used in quantification are always local variables.

I think I just expected that normal scoping rules -- in which the inner variable shadows the parameter variable -- would apply. Is there a specification of scoping rules anywhere in the PDDL or HDDL specs? I have a vague memory of having seen it somewhere, but can't recall where.