Add forall tag to preconditions

[mass2010chromium]

Done by exploding the forall into a bunch of and conditions (in both the ASP side and the checking side in the simulator).

Also allow removing nonexistent predicates (predicates not specified are assumed to be false)

[miestrode]

Hello! Thank you for your interest in contributing to PDDLSIM! I'll review this PR shortly with my comments. From a brief look however, disregarding the code added, there are still several things to add, such as tests. I'll include everything in my review.

[galk-research]

Also missing:

• A slightly more detailed note about motivation for the feature (i.e., what PDDL domains did you encounter that have a forall clause, or what usage do you forsee)
• Documentation of the change in code

[miestrode]

Some parts of the code look good, but there remains work to be done. To summarize:

• Support for non-existent predicates is not something we plan to add. Please remove such support that you partially added.
• You still need to add the proper domain requirement to the parser, and proper validation of the "forall" condition (Can't use the condition if requirement is not present). We take validation seriously.
• The approach currently used for GGA with "forall" conditions (exploding to "and" conditions) is problem-dependent, and thus not ideal. There's no need to re-architect things however. Instead, you probably want to do things as follows: You make a rule for the condition of the forall, which is parameterized by the quantification variables as normal. Then you make a separate rule, let's name it rule2, not parameterized at all, that uses the first rule (let's name it rule1, as follows: rule2 :- rule1(X, Y, Z, ...) : type_x(X), type_y(Y), type_z(Z), .... This essentially amounts to using conditions. See section 3.1.11 of the Potassco user guide for more information.
• This PR lacks any tests for the new condition. You can look at the existing tests to see what needs to be done. This will include GGA tests, validation tests, serialization tests, etc. Testing is important, and we have tests. As the PR's author its your job to write these.

Not a part of the PR, but also important, is writing about this feature in the PDDLSIM wiki. You can read in the wiki more about the writing guidelines. I'd appreciate it if you send here a Markdown version of a page explaining this feature, that we can use in the wiki.

Finally, as Gal mentions, I'd would be nice to know why this feature is necessary in the first place. It is a part of the PDDL spec, that's true, but what specific domains did you encounter that required it? Knowing this could help us in the future.

[miestrode]

This is a crash recovery file on Vim, right? In that case, I really don't think this should be in the .gitignore. Just don't commit it, and once it serves its purpose ideally remove it from your filesystem.

[mass2010chromium]

Vim creates .swp files whenever a file is opened; basically if you git status while vim is still open it'll show a bunch of .swp files. I can remove it from the .gitignore

[galk-research]

Yeah, I actually think it is a good idea to include in the ..gitignore. Otherwise, these swp files show up in the status checks and "untracked". Technically this is harmless, but in practice, this is annoying and distracting.
So putting *.swp and *~ in the .gitignore file is good practice.

[miestrode]

I mean, personally, I've never had this issue while using Vim, and am kind of of the belief that a .gitignore should only include what's relevant to the project itself, and is independent of the tooling used by developers, but if you really feel like this is fine, I'm also not too against it.

It does feel like just using Git's core.excludesfile would be enough though, but I'm not a very frequent Vim user anymore.

[miestrode]

This should probably also allow quantification over all objects (no type specified). You should probably create a parameterized parser (like say typed_list{item}) for this purpose, to be as general as possible.

[miestrode]

Why is this comment still here? Is this part of the PR, or not? If not, remove it.

[mass2010chromium]

Removed.

[miestrode]

Why is there a diff here? These lines look the exact same. Weird.

[mass2010chromium]

Maybe an ending newline diff? I don't know...

[miestrode]

You needed to add a new kind of requirement for this feature, that being universal-preconditions, like you can see is done for other features, such as OR-conditions. This will need to be wired elsewhere, as is explained in my review, and in here.

[mass2010chromium]

I'm so sorry 😭 I did not see the contributor guide

I just realized that what I essentially ended up doing is a rewrite of the ASP based successor generation logic https://github.com/galk-research/pddlsim/wiki/ASP-Based-Successor-Generation ... I can update the wiki documentation if you are ok with that or maybe we can try a different approach...

Though in my opinion the new method is slightly more straightforward conceptually (though it needs some weird additional conditions inserted to satisfy clingo).

[miestrode]

This seems to be a remnant of copying from EqualityCondition. Please change this. A proper __repr__ implementation is actually very key to allow agents to work with your universal conditions (via the RSP protocol).

[mass2010chromium]

Fixed.

[miestrode]

Should be "a", not "an", and in parnetheses, write forall, for consistency with other documentation.

[miestrode]

Why is this called loop_var? Where is the loop here? Also try to not use shortenings. quantification_variable, or just variable is better here. Also what is Typed? We have a Typed[T] but not Typed here. You probably meant somethingf like Typed[Identifier], although to be entirely honestly, you'll likely want to allow quantification over multiple variables (with the necessary grammar changes), so I would look to ActionDefinition for inspiration.

[mass2010chromium]

Fixed renamed to (variable).

Type list[Typed[Variable]]

[miestrode]

I'd really rather you not add the problem to the action definition, as this basically destroys caching, which we currently make use of. You don't need to do this! You can encode universal quantification just fine without explicitly mentioning objects from the problem, and making a bunch of and conditions. I'll elaborate on this when I summarize my review.

[mass2010chromium]

Yeah, I agree that this is disgusting -- to be perfectly transparent this is the first time I'm dealing with ASP so I think I didn't solve the problem in a good way :)

I'll fix it to match your implementation

[mass2010chromium]

Fixed as of latest commit but ended up doing a rewrite

[miestrode]

I know the idea here is to allow non-existent predicates, but this is not something we plan to support. Non-existent predicates will always remain an error, for the foreseeable future.

[miestrode]

Also I'm pretty sure you'd have to modify the parser for this anyway, since we currently do validation on all PDDL input.

[mass2010chromium]

Sorry, I should've specified the intent; I ran into an error where I was setting a predicate to False as part of an action's effect; but if that predicate is already false, then this causes an error. This change was intended to allow that behavior, not to allow non-existent predicates.

[miestrode]

Oh, I see, yeah you're totally right, this would be a bug. It's a shame we didn't catch it earlier. Please remove this from the PR. I'll open a separate PR fixing this, and adding a test so the issue doesn't arise again.

[mass2010chromium]

This came up when running simulation of a pick and place task:

(define (domain tabletop)
 (:requirements :equality :typing :negative-preconditions :disjunctive-preconditions)
 (:types
  scene_object
  immovable - scene_object
  graspable - scene_object

  robot
 )

 (:predicates
  (on ?x - scene_object ?y - scene_object)  ; x is on y
  (in ?x - scene_object ?y - scene_object)  ; x is in y (y is a container)
  (carry ?r - robot ?x - scene_object)      ; Robot is carrying object
  (free ?r - robot)                         ; Robot has hands free.
                                            ;   Exactly one of `free` and `carry` must be set.
  (openable ?x - scene_object)              ; Affordance of being a container that can be open or closed.
                                            ;   Represented as an attribute instead of a class, since either
                                            ;   graspable or immovable objects can be openable...
                                            ;   For example, a drawer or refridgerator.
                                            ;   Openable objects must have exactly one of `open` or `closed` set.
  (open ?x - scene_object)                  ; Container is open.
  (closed ?x - scene_object)                ; Container is closed. Cannot have objects placed in it.
 )

 (:action pickup_from ; Pick up object x from on object z. To pick up a stack of objects, pick up the bottom object
  :parameters (?x - graspable ?r - robot ?z - scene_object)
  :precondition
  (and
   (free ?r)
   (or  ; The object we pick up should be on or in something (not held in hand)
     (on ?x ?z)
     (and (in ?x ?z) (not (closed ?z)))
     (forall (?o - scene_object)  ; Pick from the top.
       (not (on ?o ?x))
     )
   )
  )
  :effect
  (and
   (carry ?r ?x)
   (not (free ?r))
   (not (on ?x ?z))
   (not (in ?x ?z))
  )
 )

 (:action place_on ; Place object x onto object z. (Stacks them)
  :parameters (?x - graspable ?r - robot ?z - scene_object)
  :precondition
  (and
   (carry ?r ?x)
   (not (carry ?r ?z))
   (forall (?o - scene_object)  ; Disallow building stacks in containers.
     (not (in ?z ?o))
   )
  )

 (:action place_in ; Place object x into object z.
  :parameters (?x - graspable ?r - robot ?z - scene_object)
  :precondition
  (and
   (carry ?r ?x)
   (not (carry ?r ?z))
   (open ?z)
  )
  :effect
  (and
   (not (carry ?r ?x))
   (free ?r)
   (in ?x ?z)
  )
 )

 (:action open  ; Open object x using robot gripper. Gripper must be free
  :parameters (?x - scene_object ?r - robot)
  :precondition
  (and
   (free ?r)
   (closed ?x)
   (openable ?x)
  )
  :effect
  (and
   (not (closed ?x))
   (open ?x)
  )
 )

 (:action close ; Close object x using robot gripper. Gripper must be free
  :parameters (?x - scene_object ?r - robot)
  :precondition
  (and
   (free ?r)
   (open ?x)
   (openable ?x)
  )
  :effect
  (and
   (not (open ?x))
   (closed ?x)
  )
 )
)

Forall is used to constrain objects from being stacked inside containers, and to force the robot to pick up one object at a time.

The problem file is generated at runtime for us so I thought it would be cleaner to encode the logic this way instead of enumerating things in the domain definition.

[mass2010chromium]

Then you make a separate rule, let's name it rule2, not parameterized at all, that uses the first rule (let's name it rule1, as follows: rule2 :- rule1(X, Y, Z, ...) : type_x(X), type_y(Y), type_z(Z), ....

How would this work with other rules though? I was thinking of doing this when implementing actually but doesn't this require all the subconditions of the forall condition to also be parametrized? As far as I understand it the current implementation of ASP translation translates all conditions into non parametrized rules. For a given action:

# objects_asp_part
type0(object0).
type0(object1).
...

# predicates
predicate0(object0).
predicate1(object0, object1).
...

# action parameters
# For example, for action with parameters: (?var0 - type0 ?var1 - type2)
#   and precondition: (and (predicate0 ?var0) (predicate5 ?var0 ?var1))
#   (reusing the ID names for simplicity)
1={var0(O):type0(O)}=1.  # Bind var0 (type type0)
1={var1(O):type2(O)}=1.  # Bind var1 (type type2)

# conditions/predicates
rule0: var0(T0), predicate0(T0).
rule1: var0(T0), var1(T1), predicate5(T0, T1).
rule2: rule0, rule1.

The problem being in the rule definitions; none of the subrules are parametrized. So to implement forall would require parametrizing all the rules that are children of the forall condition, is that what you think is the cleanest solution? @miestrode

[mass2010chromium]

Just to be clear, is this what you're talking about (as a toy implementation of forall, not using the codebase's naming conventions)?

type0(a).
type0(b).

on(a).
on(b).
% off(b)

cond(O) :- on(O).
forall :- cond(O) : type0(O).

[miestrode]

Yes, this is what I'm talking about. Each rule is only used once, and it makes perfect sense: the rules representing subconditions of the universal quantification body, are naturally quantified over the variables of the universal quantification. This will require some modification to the existing ASP code, but is otherwise the cleanest. Also, this is the only way to cleanly reprsent foralls with multiple quantifiers, while avoiding some kind of exponential increase in subconditions, IIUC.

On an unrelated note, you'll need to add validation against name-clashing when using foralls, don't re-define variables of the action definition for instance.

[miestrode]

Regarding your earlier comment about the forall use-case: I'm pretty sure you should be able to replace it, by introducing some new predicates. I'm not too certain because I don't fully understand just how flexible the domain is supposed to be, but at the very least you can replace some usages I believe, as it's ultimately a small extension to the well known blocksworld domain. Please do correct me if I'm wrong.

[mass2010chromium]

Regarding your earlier comment about the forall use-case: I'm pretty sure you should be able to replace it, by introducing some new predicates. I'm not too certain because I don't fully understand just how flexible the domain is supposed to be, but at the very least you can replace some usages I believe, as it's ultimately a small extension to the well known blocksworld domain. Please do correct me if I'm wrong.

Maybe, I would have to think about it -- My "first thought" solution of adding a "top_open" predicate I think doesn't work (without introducing new actions) since there isn't an easy way to determine when to add the predicate when removing objects from on top of another object, without using a forall to check that no other objects are still on the surface. Or it could just be my incompetence/inexperience with writing these things 😅

At least I think blocksworld does not support putting multiple blocks on top of the same block.

[mass2010chromium]

On an unrelated note, you'll need to add validation against name-clashing when using foralls, don't re-define variables of the action definition for instance.

What's the behavior if a name is redefined? Should it be an error? Or does it behave like a scope (variable is named like that only within the forall)?

[mass2010chromium]

@miestrode getting to implementation, I'm thinking of changing the entire asp implementation to use the "parametrized form"(?):

% Object definitions (unchanged)
type0(a).
type0(b).
type1(c).

type0(O) :- type1(O).

% Dummies needed for implementing OR condition to absorb variables
true(a).
true(b).
true(c).

% State of the simulation predicates (unchanged)
on(b).
on(c).
off(a).

% Lowest level predicates
rule1(O) :- on(O).
rule2(O) :- off(O).

% AND predicate
and(A, B) :- rule1(A), rule2(B).

% OR predicate
or(A, B) :- rule1(A), true(B).
or(A, B) :- rule2(B), true(A).

% Action with precondition
action(A, B) :- or(A, B).

% Final output for action groundings
#show action/2.
% AND: action(b, a) action(c, a)
% OR: action(b,a) action(b,b) action(b,c) action(c,a) action(c,b) action(c,c) action(a,a)

That way forall doesn't have to be a special case. But the OR condition seems to require you to absorb all the extra arguments somehow? Do you know a better way to do this?

[mass2010chromium]

See comment in _asp.py:

Add rules corresponding to a precondition of an action in PDDL.

Preconditions are added like so:

(predicate X Y Z):
  -> rule1(X, Y, Z) :- predicate(X, Y, Z).

(and (A) (B)):
  -> rule(X, Y) :- ruleA(X), ruleB(Y).

(or (A) (B)):
  -> rule(X, Y) :- ruleA(X), true(Y).
     rule(X, Y) :- true(X), ruleB(Y).

(not (A)):
  -> rule(X) :- true(X), not ruleA(X).

(= X Y):
  -> rule(X, Y) :- true(X), true(Y), X = Y.

(forall (X, Y) (C)):
  -> rule(A) :- true(Z), ruleC(X, Y, Z) : X, Y.

where A, B, C are conditions, depending on variables X, Y, Z respectively,

where the exact rule namings are slightly different in the code, but translated
  to ruleA/ruleB/ruleC to match the A, B, C conditions,

where the true(*) facts are just always true for any object
  (defined in object asp section).

Loosely. The actual arguments will depend on the number of used
variables in the subconditions, and forall quantification variables
are specified using their type facts.


Returns a pair (added rule ID, used variables, in call order).