Thanks for reviewing! This one is done.

Done with comments, and the experiments look good.

The comparison against the baseline still looks good:
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v5-issue707-base-v2-issue707-v5-compare.html

Also the experiments for the new pruning options are done:
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v5-pruning-variants.html
Compared to the previous version, there is a clear effect on the configurations
using ShrinkFH, due to the previous bug that caused pruning to happen
independently of the chosen options. Interestingly, ShrinkFH is also the
strategy that suffers the most from turning off pruning, in particular from not
pruning irrelevant states, which causes it to use the map-based partitioning
more frequently.

From my side, if you are happy with my latest commits, this is ready to be merged.

I addressed your comments and ran a debug experiment, which did not show any
assertion failures:
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v5-debug-issue707-base-v2-issue707-v5-compare.html

Full experiments for v5 (release) are on the way.

Done with my comments.

Oups, sorry: https://bitbucket.org/SilvanS/fd-dev/pull-requests/27/issue707/diff

> Pull request ready for the upcoming sprint:
>
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v4-issue707-base-v2-issue707-v4-compare.html

Hi Silvan, that's not the pull request. Can you send me a link to the pull request?

Experimental results look good.

Forgot to mention the latest experiments:

http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v4-issue707-base-v2-issue707-v4-compare.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v4-pruning-variants.html

I brought the code up to date and also turned pruning into a manually triggered
transformation (and hence dropped pruning from the validity invariant for
transition systems).

Pull request ready for the upcoming sprint:
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v4-issue707-base-v2-issue707-v4-compare.html

Again ran the new configurations (no pruning of unreachable and/or irrelevant
states); the same comment as in msg6156 apply.

http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v3-pruning-variants.html

As there was a bug with detecting unsolvable factors, I re-ran the experiment on
the unsolvable instances and everything works fine now
(http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v3a-pruning-variants.html).

I updated the code to incorporate the recent changes from other issues and to
also make "prune" a public method of the interface of FTS.

The comparison still looks good (with -2 coverage twice which I assume to be noise):
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v3-issue707-base-v2-issue707-v3-compare.html

I also ran the same configurations, using no pruning or only pruning either
unreachable or irrelevant states. No crashes or other problems.
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v2-pruning-variants.html

I'm just a little surprised that pruning does not have an exclusively positive
effect across all configurations and benchmarks, but sometimes less pruning even
results in higher coverage. From what I saw in a comparison report for some DFP
configurations, this results from different merge orders as a result of
different transition systems:
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v1-v2-dfp-compare.html Even
more surprising to me is that this effect happens for DFP when turning off
pruning of irrelevant states, although we need to compute goal distances for DFP
anyways.

Anyways, this is probably not really related to the issue, but something that
might be interesting to look further into.

I implemented the following solution:
- Two options for M&S: prune_unreachable_states and prune_irrelevant_states (not
sure if the latter is really useful for anything)
- Distances do not compute max_* information, i.e. max_h, max_g, or max_f. Users
(= shrink_fh) need to compute this on their own.
- Each shrink and merge strategy needs to specify the methods
"requires_init_distances" and "requires_goal_distances". The decision about
which distance information is actually computed depends on both the pruning
options and the chosen shrink/merge strategies, e.g. if the shrink strategy
requires h values, the merge strategy requires g values, and no pruning is
chosen, then all distances will be computed, and similarly the other way round
(if neither the shrink nor the merge strategy require any distance information
but full pruning is used, then all distances will be computed.

The comparison of typical M&S configurations (i.e. all using "full pruning" and
hence full distance computation as always) looks fine: 
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue707-v1-issue707-base-issue707-v1-compare.html

(Running the same configurations with all other three pruning variants is still
on the way, after discovering a problem with unsolvable instances and not
pruning irrelevant states.)

I added the following options for pruning: no pruning, only reachable states,
only irrelevant states, or both (default).

I'm not quite sure how the interaction with the shink strategies should be
handled: bisimulation based shrinking expects that there are no states with h =
INF (used as end sentinel in the successor signatures), and fh-shrinking decides
based on the max_f value whether to use a map or a vector for the buckets. If no
unreachable or no irrelevant states are pruned, max_f will often be infinity,
which I assume will result in often using (the slower?) map for the buckets.

Another complication is with the computation of distances: this computation also
sets the max* values, but it ignores all values of infinity, assuming that such
states are pruned. With pruning being configurable, we would need to let the
distance computation know about what pruning happens and we would have max*
values be infinity, with the above complications.

item N suggest to let the shrink strategies (and merge strategies?) tell the
algorithm if they need g and/or h values, but I think this could need to be
strengthened to require pruning of unreachable and/or irrelevant states, which
would turn this option somewhat less useless (fh-shrinking would require full
pruning, bismiulation based shrinking would require at least irrelevant pruning).

To conclude, I wonder whether the shrink/merge strategies should require
computation of g/h values or rather pruning of unreachable/irrelevant states,
and if the Distances should be responsible to determine max* values and which
states to be pruned, or if this should happen from outside, with the distance
information of Distances.

Again, without typo: meta issue567

This is part of meta isuse567 and addresses item N.

  - Distances computation could be made more fine-grained. Which things
    do we really need to recompute after shrinking? When do we need g
    values, and when don't we? It might be a good idea to give the
    shrink strategies and merge strategies a methods that let them tell
    the overall algorithm whether they are interested in g values and/or
    h values; e.g., only shrink_fh would be interested in g values;
    merge_dfp is interested in h values; shrink_bisimulation is
    interested in h values when using greedy bisimulation or when using
    h for initialization (which at the moment we always use?).
  - Should we make pruning irrelevant and/or unreachable states
    configurable? Should it be a *separate* step that is controlled by
    the main merge-and-shrink loop? (Logically, it is a separate
    transformation of the factored transition system. In practice, it
    might be more efficient to couple it with other steps.)
  - The vector<bool> of prunable states should probably be accessed the
    same way as the g and h values, rather than using a separate
    interface as it is done currently (g and h are stored in the
    Distance object and requested individually; prunability is returned
    as a complete vector).

To start, I want to address bullet points 2 and 3, i.e. it should be
configurable to perform no pruning, prune only unreachable or irrelevant states,
or both as previously. I wonder whether it would be worth to actually
distinguish the reason of why a state was pruned, i.e. to replace PRUNED_STATE
by UNREACHABLE_STATE and IRRELEVANT_STATE. For some applications this may be
useful, e.g. computing unsolvability certificates or using symmetrical lookups,
where it is important to not consider unreachable states as dead-ends. For
regular merge-and-shrink, there would be no need to distinguish the reason of a
state being pruned, I think, it would be enough to make it configurable. What do
you think, should we still add such a distinction?