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.)