Remove mapping, proposition names *are* PDDL ground fluents. Fix ambiguity in DP names

[marfvr]

Proposed changes

After this commit, to specify the PPLTL formula, there is no need to provide an explicit mapping, since it is assumed that the propositions are the ground fluents.

E.g. if previously the formula was specified as follows:

formula = "on_b_a & O(ontable_c)"

Now we require that the propositions can be interpreted as PDDL predicates, i.e.:

formula = '"on b a" & O("ontable c")'

Pylogics does not allow spaces in the proposition name; therefore, the double quotes are always required.

Only exception is when the predicate is unary:

formula = 'Y(O(made-p4)))'

(as in openstacks).

@LBonassi95 @francescofuggitti I would like to make a thorough discussion with you on this PR since it changes quite a few things.

Fixes

n/a

Types of changes

What types of changes does your code introduce? Put an x in the boxes that apply

• [X] Bugfix (non-breaking change which fixes an issue)
• [ ] New feature (non-breaking change which adds functionality)
• [X] Breaking change (fix or feature that would cause existing functionality to not work as expected)

Checklist

Put an x in the boxes that apply.

• [ ] I have read the CONTRIBUTING doc
• [ ] I am making a pull request against the develop branch (left side). Also, you should start your branch off our develop.
• [ ] Lint and unit tests pass locally with my changes
• [ ] I have added tests that prove my fix is effective or that my feature works

Further comments

n/a

[marfvr]

Alternative considered: add parenthesis: "(p a b)"

Pros: more adherence to PDDL format; Cons: parenthesis might add too much cognitive overload, considering that they can occur also in the formula

[codecov[bot]]

Codecov Report

Merging #262 (838f43c) into main (dd7b158) will decrease coverage by 0.96%. The diff coverage is 94.20%.

Additional details and impacted files

@@            Coverage Diff             @@
##             main     #262      +/-   ##
==========================================
- Coverage   89.79%   88.84%   -0.96%     
==========================================
  Files          12       11       -1     
  Lines         549      484      -65     
==========================================
- Hits          493      430      -63     
+ Misses         56       54       -2     

Flag	Coverage Δ
unittests	88.84% <94.20%> (-0.96%)	:arrow_down:

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files	Coverage Δ
plan4past/__main__.py	0.00% <0.00%> (ø)
plan4past/helpers/utils.py	97.77% <97.22%> (-2.23%)	:arrow_down:
plan4past/compiler.py	98.18% <100.00%> (-0.24%)	:arrow_down:
plan4past/utils/derived_visitor.py	100.00% <100.00%> (ø)
plan4past/utils/predicates_visitor.py	100.00% <100.00%> (ø)
plan4past/utils/rewrite_formula_visitor.py	100.00% <100.00%> (ø)
plan4past/utils/val_predicates_visitor.py	100.00% <100.00%> (ø)

[marfvr]

Consider the formula:

(a S (b & O(c))) 
| 
((a S b) & O(c))

We get the following derived predicates:

(:derived (val__Oc) (or (val__c) (Y-Oc)))
(:derived (val__Oc) (or (val__c) (Y-Oc)))
(:derived (val__a) (a))
(:derived (val__a) (a))
(:derived (val__a-S-b) (or (val__b) (and (val__a) (Y-a-S-b))))
(:derived (val__a-S-b-and-Oc) (and (val__a-S-b) (val__Oc)))
(:derived (val__a-S-b-and-Oc) (or (val__b-and-Oc) (and (val__a) (Y-a-S-b-and-Oc))))
(:derived (val__a-S-b-and-Oc-or-a-S-b-and-Oc) (val__a-S-b-and-Oc))
(:derived (val__b) (b))
(:derived (val__b) (b))
(:derived (val__b-and-Oc) (and (val__b) (val__Oc)))
(:derived (val__c) (c))
(:derived (val__c) (c))

The derived predicate val__a-S-b-and-Oc occurs twice with a different condition on the right. This is because we do not distinguish between open and close parenthesis. This has to be addressed.

Idea: replace ( with LPAR__ and ) with __RPAR. The result would be:

(:derived (val__LPAR__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR__RPAR__RPAR-or-LPAR__LPAR__LPAR__a__RPAR-S-LPAR__b__RPAR__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR__RPAR) (or (val__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR__RPAR) (val__LPAR__LPAR__a__RPAR-S-LPAR__b__RPAR__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR)))
(:derived (val__LPAR__LPAR__a__RPAR-S-LPAR__b__RPAR__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR) (and (val__LPAR__a__RPAR-S-LPAR__b__RPAR) (val__OLPAR__c__RPAR)))
(:derived (val__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR__RPAR) (or (val__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR) (and (val__a) (Y-LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR__RPAR))))
(:derived (val__LPAR__a__RPAR-S-LPAR__b__RPAR) (or (val__b) (and (val__a) (Y-LPAR__a__RPAR-S-LPAR__b__RPAR))))
(:derived (val__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR) (and (val__b) (val__OLPAR__c__RPAR)))
(:derived (val__OLPAR__c__RPAR) (or (val__c) (Y-OLPAR__c__RPAR)))
(:derived (val__OLPAR__c__RPAR) (or (val__c) (Y-OLPAR__c__RPAR)))
(:derived (val__a) (a))
(:derived (val__a) (a))
(:derived (val__b) (b))
(:derived (val__b) (b))
(:derived (val__c) (c))
(:derived (val__c) (c))

Which is quite verbose, but now the two conflicting derived predicates now have distinct names:

(:derived (val__LPAR__LPAR__a__RPAR-S-LPAR__b__RPAR__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR) (and (val__LPAR__a__RPAR-S-LPAR__b__RPAR) (val__OLPAR__c__RPAR)))
(:derived (val__LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR__RPAR) (or (val__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR) (and (val__a) (Y-LPAR__a__RPAR-S-LPAR__LPAR__b__RPAR-and-LPAR__OLPAR__c__RPAR__RPAR__RPAR))))

Of course other alternatives than LPAR__ and __RPAR could be considered...

[marfvr]

An even simpler formula is: O(a) & "Oa", which generates:

(:derived (val__Oa) (Oa))
(:derived (val__Oa) (or (val__a) (Y-Oa)))
(:derived (val__Oa-and-Oa) (val__Oa))
(:derived (val__a) (a))

Again, val__Oa is ambiguous: it both resolves to the predicate name Oa, or to the "once a" rule.

[marfvr]

Copying from c891195:

with this change, we translate each formula special symbols (operator symbols, parenthesis etc.) into a sequence of characters that can be part of a valid derived predicate name.

This means that, given a name of a derived predicate, one can simply do the inverse replacement and recover the original formula.

This approach has two major drawbacks:

1. the output of the compiler is much more verbose; e.g. the formula 'Y(a)' gets translated into 'val__YLPAR__a__RPAR'
2. the new approach imposes restrictions on the allowed symbols in a PPLTL formula. E.g. symbols that start with VAL__ or Y__, or symbols that contain one of the following as substring:

• LPAR__ (left parenthesis)
• __RPAR (right parenthesis)
• NOT__ (not symbol)
• __AND__ (and symbol)
• __OR__ (or symbol)
• __QUOTE__ (quote) are forbidden.

This policy might be more conservative than needed, but in this way we should have the guarantee that the encoding is an invertible mapping (such property basically proves non-ambiguity of the encoding, because it means there is a one-to-one relationship between 'string representation of pylogics formulas' and 'string representation encoded as PDDL predicate name').

[LBonassi95]

Regarding the collision between "Val" (and "Y") PDDL predicates corresponding to different PPLTL subformulas, I think it is a good idea to use unique identifiers for these atoms. I propose the following pattern val_id-[PPLTL operator | Atom]_{Ids of Arguments} Example: for O(O(a)) we generate: [ val_p0-a val_p1-Once_p0 val_p2-Once_p1 ]

Other examples: (a S (b & O(c))) [ val_p3-Since_p5_p2, val_p2-And_p1_p0, val_p0-O_p4, val_p4_c, val_p5_a, val_p1_b ]

((a S b) & O(c)) [ val_p3-And_p2_p0, val_p2-Since_p5_p1, val_p0-Once_p4, val_p4_c, val_p5_a, val_p1_b ] Let me know what you think about this approach.