> I didn't want to open up a big discussion, and if we consider this as a feature
> then I don't think it is worth our time right now, given the upcoming ICAPS
> deadline.

I think it makes sense to decide on a policy; this doesn't mean we have to make all the necessary code changes immediately.

Independently of this, we can add this specific check.

I primarily wanted to make clear that there are many other similar gaps, some of them subtle (e.g. goals like "second variable has value 3 and first variable has value 2" are unsupported because goals must be sorted). Or perhaps the sortedness is actually already validated; I didn't double-check.

I see, I was not aware that SAS files not generated with the translator are somewhat unexpected, or at least nothing we consider common enough to deal with them explicitly. However, for some things (e.g. preconditions) the checks whether the values actually exist for a variable seems to be there, so I found it strange that this is not the case for the initial state, which ultimately made me report this as a bug.

I didn't want to open up a big discussion, and if we consider this as a feature then I don't think it is worth our time right now, given the upcoming ICAPS deadline.

I think it would be good to add this check (I think we already have similar checks for preconditions and similar), but it's a somewhat subtle question whether we consider this a bug or not, and consequently whether we have many other similar bugs or not.

Currently, the search component intentionally only performs limited checks if its input file is well-formed. The idea is that if the translator doesn't create something illegal, then the search component doesn't have to verify it.

The translator output file format is at least to some extent an implementation detail of the overall planner. We do document it, but the original intention of this was for other people to use the translator's output file, not for the search component to use SAS files created externally. While we do mention "you can write your own SAS file" an option occasionally, our policy so far has been that this is a "do at your own risk" thing, and we don't promise full error checking of this input. The actual input language we support is PDDL.

Full checking could add substantial overhead; there are many checks currently missing, such as:

- stratification condition for axioms
- only derived variables may appear in heads of axioms
- only non-derived variables appear in action effects

More subtly, there are also normalization conditions (documented only in source code comments in the translator) that the search code is currently allowed to rely on and that externally generated SAS files might violate, e.g. that preconditions are sorted and not duplicated.

There are also some things that we cannot reasonably check; e.g., if someone specifies a mutex that isn't a mutex, it would be PSPACE-complete to find this out. But we could at least be explicit regarding the promises we make around this, and I think this is the only example of this kind. I think everything else could be checked in linear time.

So: what should our policy for this be? Once we've answered this, we should also document this answer clearly.

(We can change this specific point regardless. But if we don't change our policy to "the search component is responsible for validating its input", it would not be a bug fix but a new "feature" or improvement.)

When reading a .sas file as input, the responsible component does not complain if the value of a variable in the initial state does not exist. I have attached a file where this is the case. (The file was produced with Machetli based on sokoban-opt08-strips/p02.pddl, hence the strange action names and non-fitting effects. I made some more changes by hand and accidentally forgot to change the value of the variable in question, so this part was not Machetli's fault.) Variable 0 is assigned the value 16 in the initial state, but variable 0 has only 4 values. Running the problem with

./fast-downward.py problem.sas --search "astar(lmcut())"

works smoothely on revision 641d70b36 and even finds a plan.