The buildbot caught an issue with Python 3, which is now fixed.

I made the change pointed out by Gabi in the code review and tested that the
code still works (in addition to the fix, I temporarily added "assert
effect_conditions is cond" to make sure that the behaviour is also the same;
that assertion is of course not committed).

The fix is now merged. Thanks, everyone!

As discussed offline, I've made a pull request on bitbucket.

I have rewritten the questionable parts of simplify.py, and it now works for
Anders's example.

I also tested the new code and the new task validation on all benchmarks in the
Fast Downward repository (including those we rarely test that are not part of
lab's predefined suites). It turned out that the assumptions that mutex groups
were sorted was wrong, so I've added a sorting call. Now all benchmark tasks
translate smoothly and validate correctly before and after simplification. (The
validation step needs to be manually switched on because it is very time-consuming.)

I also noticed that in some domains (at least airport-adl, if I recall
correctly) there are many mutex groups of size 1. They are useless, but they are
also harmless, so they are not declared illegal for now. If we want to get rid
of them, I think we want to get rid more generally of mutex groups that only
refer to one variable (which are generally useless and occur quite frequently).
If anyone would like to see this, please open an issue. (This doesn't entail
volunteering to do the work. ;-))

The bad news from the experiments (not quite unexpected) is that the new
implementation of simplify is significantly slower, roughly a factor of 3 on
average. The total time for simplification across all (2000+) benchmarks
increases from 497.09 to 1343.36 seconds, or roughly 0.5 seconds per instance.

In terms of total translator time, this means we now take 7% longer when summing
runtimes over all instances. I think this is acceptable, but if we are worried
about this speed loss, we could speed up this bit e.g. by adding a dedicated
implementation for tasks without conditional effects. My recommendation is to
merge it in its current form, though.

Is anyone interested in seeing the full experimental results? (It's no problem
to upload them, it's just that they'd take 134M on the server.)

@Gabi: I can merge this with or without a code review, whatever you prefer. Let
me know. If you'd like to do a code review, please also let me know if you
prefer Rietveld or bitbucket.

> so I'd rather start by making some of the currently implicit
> assumptions about the operator representations more explicit.

Wow, that was more work than I expected.

@Gabi: at some point, can you look at the comments/docstrings in

 
https://bitbucket.org/malte/downward/commits/3211fe2dae620f2579af0acc02a97a0b2fc7c6ba

and tell me if you're fine with the requirements listed there? (There's no
hurry.) For now, these are just requirements that are intended to be enforced
inside the translator, but we could make them documented aspects of the output
format at some point.

If we end up doing that, it would tie into our open issues related to changes to
the output format etc.

(I don't think there's a need to check the validation code itself unless you
want to -- just checking the documentation should be enough. While I'm not
convinced the code is correct, if there are glaring errors, they are likely to
be caught by the experiments I'm planning to do once the bug in simplify.py is
fixed.)

I've started working on this today.

Analysis:

The error is in the translator's "simplify.py". In Anders's failing example, we
determine that some of the propositions can be pruned:

===========================================================================
Detecting unreachable propositions...
variable count: 4 => 4
number of removed values: 2
variable conversions:
variable 0 [size 2] => 0 [size 2]
    value 0 => 0
    value 1 => 1
variable 1 [size 2] => 1 [size 2]
    value 0 => 0
    value 1 => 1
variable 2 [size 2] => 2 [size 2]
    value 0 => 0
    value 1 => 1
variable 3 [size 6] => 3 [size 4]
    value 0 => 0
    value 1 => 1
    value 2 => always false
    value 3 => always false
    value 4 => 2
    value 5 => 3
===========================================================================

The way to read this is that, for example, for variable 3 we should replace
value 0 by value 0 (so leave it as is), change value 1 to 1, get rid of value 2,
get rid of value 3, change value 4 to 2, and change value 5 to 3.

So var3=2 and var3=3 can go away.

The code that tries to perform the pruning then chokes on the following operator:
===========================================================================
(start-process o1 tw1 th1)
Prevail:
Pre/Post:
  v1: -1 -> 1
  v3: 4 -> 0 [1: 0]
  v3: 4 -> 2 [3: 0]
  v3: 4 -> 5 [1: 1]
===========================================================================

We have to be careful when reading this to remember that "preconditions" listed
with a particular pre/post entry are actually global operator conditions, not
parts of a conditional effect. So for example, "v3: 4 -> 0 [1: 0]" means that
v3=4 is a precondition, and there is a conditional effect that sets v3 := 0 if v1=0.

The problematic bit is this pre/post entry:
  v3: 4 -> 2 [3: 0]

This seems to set v3 to the value 2, which we have determined is a value to be
pruned. So this looks like an impossible effect. This is alright because it can
never trigger: we have the precondition v3=4, and this effect has the effect
condition v3=0, which obviously cannot hold at the same time.

The correct thing in this case is to just discard the whole pre_post entry. But
note that this would not be correct if this were the *only* effect on v3,
because simply dropping the pre_post entry would lose the precondition in that
case. In that case, we would need to add v3=4 to the *prevail* conditions of the
operator.

Our current code notices that something dangerous is going on there. It isn't
smart enough to convert preconditions into prevail conditions, or to determine
in which cases this should be done and in which cases another pre/post entry on
the same variable also encodes the condition. Instead of doing something
potentially unsafe, the code merely gives up by failing an assertion.

So we know now what is going on here, and I've also looked at simplify.py
closely enough to have an idea how to fix this. I think a comparatively small
local change would be possible, but the code is already getting quite
convoluted, so I'd rather start by making some of the currently implicit
assumptions about the operator representations more explicit.

bug reported on the Fast Downward mailing list by Anders Jonsson (08.05.2015):

=============================================================================================
During experiments with Fast Downward we encountered a translation error that we
were unable to fix. Since we are not sure whether this is a modelling mistake
(on our side) or a translation problem, I decided to post a minimal example
here. With reachability detection turned on we obtain the following error:

  File "/home/anders/projects/planners/fast-downward/src/translate/simplify.py",
line 268, in translate_pre_post
    assert new_post is not always_false

I also attach the SAS translation that I obtained with reachability detection
turned off. The translator identifies a fairly strange invariant based on
conditional effects (var3), and this invariant appears to be the culprit during
reachability testing. Even though there are multiple ground actions of type
"start-process" that could cause these effects, the translator correctly
identifies that these actions are mutually exclusive since each deletes the
precondition "inactive(tw1)" which, once deleted, cannot be added again. We
think that the problem is that the conditional effects of type "count2" are
unreachable, but from our side this is difficult to infer when doing modelling
without performing some kind of analysis of the problem on our own.
=============================================================================================

I have attached Anders's example.

I started a branch for this issue in my bitbucket repository. There isn't really
much of substance there yet. I just wanted to add a note of this because I'll
move to other things for the next week.

See email thread "Potential translation error" on the Fast Downward mailing list
(May 2015).