Thanks! The code doesn't do a full reachability analysis, so that makes sense. A full reachability analysis would obviate the need for fixpoint iteration, but I am less sure if a fixpoint iteration might be needed if we want to make sure that everything is relaxed reachable *and* relevant (according to the relevance criterion used in the code).

I ran your code on the tidybot example I mentioned and it filters two unreachable propositions in the first round, but no operators. Later rounds don't change the task.

If you want to try out if my experimental branch would prune these, you are one day too late. ;-) Bitbucket repository with that branch gone. I have a copy in airepos under helmert/bitbucket/downward-malte, though. Feel free to give yourself access.

Another data point: there are relaxed unreachable operators in all Tidybot instances, some organic-synthesis instances and some organic-synthesis-split instances from the seq-opt track. For example, in tidybot-opt11-strips/p01.pddl 4485 out of the 4591 operators produced by the translator are relaxed unreachable.

From my experiments, it seems like the behaviour only occurs in the following
instances:
organic-synthesis-opt18-strips: p01
organic-synthesis-split-opt18-strips: p05, p18, p19
organic-synthesis-split-sat18-strips: p05, p10

Hi all, there was activity on this issue while the mail server moved. If you
don't want to miss progress on this issue, please check in the tracker if there
was anything you missed.

BTW, as an alternative implementation route, we could also implement this
filtering in the C++ code. Now that "the global task" is essentially gone, I
don't see any major technical obstacles for this.

One advantage of this is that it could be a nice first step towards the eventual
translator/search component unification. Another advantage is speed.

One disadvantage is that users of the translator that don't use our search
component would not benefit from the change, but I don't think is such a big
deal. It would not be a huge challenge to make it possible for the search
component to generate a SAS file if there is sufficient interest.

TL;DR: I found out what is going on here, but can't work on it further for now.

If someone wants to take over, I'm happy to give advice. It's not a complex part
of the code and doesn't really need familiarity with the translator code.

I looked into this a bit, focusing on unreachable facts, or more specifically
facts (variable/value pairs) that are not true in the initial state (or the
negation-by-failure for derived variables) and not the effect of any operator or
axiom.

If we prune all these facts, then of course this also implies pruning all static
variables (in the usual sense), at least if we also prune all variables of
domain size 1, which we do.

The translator does quite a bit of filtering already.

Firstly, it only instantiates operators that are relaxed reachable, so at this
stage, unreachable facts cannot exist.

Later on, it prunes (some) operators that are proved unreachable by the
invariant synthesis. (This takes some delete effects into account.) This pruning
can make facts look unreachable that previously looked reachable.

Therefore, there is a third pruning stage based on reachability analysis in
DTGs. As far as I recall it, it is somewhat simpler than a relaxed reachability
analysis. All values that cannot be reached are pruned, which also prunes all
operators that refer to them. Variables that are left with only one value are
pruned completely.

This last pruning step can lead to further pruning opportunities of the same
kind, but it is only performed once. If I add a fix-point iteration to this part
of the code, I get 11 rounds of pruning for the task Daniel mentioned until it
settles down.

So much for the analysis. The next question is what to do about it. Adding a
fixed-point iteration around the simplification would address the immediate
problem, but it seems quite a stupid and expensive thing to do. Most rounds only
filter one or two preconditions in Daniel's example. I think (but need to think
about this a little bit more and also study the code) that everything we
currently do would be covered by another relaxed exploration, which also has the
property that it wouldn't have to be done more than once. So that's one way to
proceed.

Before we proceed further, it may also be interesting to run an experiment to
check in how many cases this scenario occurs.

Either way, I don't think I can find a lot of time for this in the near future.
If someone can help with the experiment or with the eventual coding, this will
progress more quickly.

Note to self and to people continuing with the work I started: the current code
in the issue875-experimental branch will probably confuse our normal translator
experiment parsers because outputs that used to be printed only once are now
printed multiple times.

Just wanted to add some more details so that we can reconstruct the case easier,
given that you are currently working on a number of translator-related issues
that might change the behaviour. 
I updated the repo before testing this on Dec 6, so revision a40b32d03b1b (which
is the subsequent commit, where nothing in the translator was changed inbetween)
should show the described behaviour.
Further, the variables in question are binary, with no operator affecting them,
but there exists actions with preconditions on both values of the variables.
Therefore, I guess the size of the generated task could decrease quite a bit
when removing the actions that can never be applied, anyway.

Thanks for looking into this! I'll add a simple sanity check to fix my issue, in 
the meantime.

The cache it was ;)

Hi Daniel, definitely worth reporting, thanks! I'll downgrade to "feature", though.

Not sure how quickly we can get to this, but if it takes too long, feel free to
ping us again.

I have the same Firefox version as you but cannot reproduce the issue. We were
fiddling with the issue tracker until yesterday, so perhaps you're just seeing
the effect of a transient problem that is now fixed. Is the wrong link problem
reproducible, even if you clear your cache?

Hi guys,
I noticed that the translator generates variables that are not changed by any 
operator. This happens for example in organic-synthesis-split-sat18 in instance 
p05. Here, the variables var0-var49 (from the output.sas) do not appear in any 
operator effect, only in preconditions.
Not sure if you want to consider this as a bug, since it does not affect 
correctness. On the other hand, the translator should be able to figure out 
that these variables can be removed. It breaks some of my code, since I assume 
that such variables do not exist, so maybe it also causes bugs in other parts 
of the planner.
BTW.. I have problems accessing the issue tracker with a recent firefox (63.0.3 
using linux). When I click the link to the tracker on fast-downward.org, I get 
back on the homepage, not to the tracker. Anyone else with similar issues? It 
works in chrome.
Cheers
Daniel