Merged.

Great!

I refactored the shrink strategy classes, mainly reducing the complexity of
which method calls which method. All of the commonly used functionality of
shrink strategies is now implemented in private methods of the base class. This
was also made possible because the "threshold" parameter of bisimulation was
moved to be an option of all shrink strategies.

The performance did not change:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-05-12-issue522-v4-comp.html

As discussed offline, we now settled to remove any default behaviour for shrink
strategies and strategies. Also label reduction must be manually set (before
shrink/merge yes/no). Furthermore, I changed the labels class to be created by
the parser (like shrink and merge strategies), and all options related to label
reduction are handled there.

The current solution (see bitbucket pull request) disables a command line string
such as "astar(merge_and_shrink())", because both reduce_labels_before_...
options need to be specified if they do not have a default value. Maybe setting
the default to false is acceptable with the warnings and the documentation? On
the other hand, this could lead to use cases where users do not enable label
reduction, which was always enabled by default before, and with no default
values, they would need to make sure to set the right option. Anyway, I think
that having defaults for shrink and merge strategies but not for label reduction
is strange. Maybe we can have no defaults at all for the three core components?
But then, what will the "users" (in contrast to researchers) do?

Another detail I just stumbled across is that the Labels-class has its own
"NONE" type for label reduction, which is now redundant. Removing it however
leads to situations where with disabled label reduction, the Labels-class will
still output the chosen options for label reduction, though not applicable. We
could move the reduce_labels_before_...-options in the Labels-class, but is that
the right place for the option, what do you think? (It it not ideal anyway that
we currently have all the options for label reductions be specified in the
merge-and-shrink class, due to the lack of label-reduction being a specific
object that could be parsed like shrink or merge strategy objects.)

> but this would silently accept all configurations not
> using any label reduction at all

We could output a performance warning in cases like this, like we already do
with "use_expensive_statistics=true" (I think).

I think I like the solution with the two new options best; it's a clean
interface and it's good to be able to experiment with this from a researcher
perspective. I think the main disadvantage is that from a user perspective, it's
harder to be sure if you're using good settings, but I think this can be
mitigated by documentation.

We could keep the new options, without default values if that is possible, and
then either add documentation about which shrink strategy to use with which
label reduction option (but this would silently accept all configurations not
using any label reduction at all), or to hack the old behavior back in by
manually setting the correct label reduction option depending on the chosen
shrink strategy (not via a flag in the shrink strategy as it was earlier, but
just via setting the merge-and-shrink option accordingly when parsing the options).

I don't know -- suggestions welcome. (For what it's worth, I think it's possible
to have options without defaults.)

Do you think we should keep the new options for enabling and disabling label
reduction at different time points? If yes, how do we set good default values?
If not, we would need to make the option depending on the chosen shrink strategy
again, which is not nice neither.

I ran the experiments you suggested. The following three tables compare the
previous way of reducing labels against all three other options, specific for
the shrink strategies. "nolr" means no label reduction, "lrshrink"/"lrmerge"
means reducing labels before shrinking/merging, and "lrshrinkmerge" means both
reducing labels before shrinking and merging. The tables group configurations
according to the used merge strategies (three comparisons each for cggl, dfp and
rl merge strategies).

bisimulation shrinking:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-04-07-issue522-v2-bisim-comp.html
greedy bisimulation shrinking:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-04-07-issue522-v2-greedybisim-comp.html
fh shrinking:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-04-07-issue522-v2-fh-comp.html

Only with bisimulation and cggl/rl merge strategies, there is a benefit in terms
of coverage from switching from reducing labels before shrinking to before
merging. For all other configurations, coverage decreases compared to the
previous default of reducing labels.

That probably means that we should not reduce labels always at the same time
point in merge-and-shrink, no matter what configuration we use. This also means
that there is no sensible default value for the "reduce labels before shrinking"
and "reduce labels before merging" options.

OK, I had a brief look.

The point here may be the linguistic emphasis in the phrase "reduce labels
before shrinking". The emphasis is not "*reduce labels* before shrinking", which
sounds like the options are "do reduce" or "don't reduce". Rather, the emphasis
is "reduce labels *before shrinking*": the question is not whether or not to
reduce, but *when*. (The options are essentially "before shrinking" or "before
merging".)

The old code used to reduce labels before merging when using a shrink_fh
strategy; the new one does not. This means that label reduction opportunities
that don't exist before shrinking but do exist after shrinking are not made use
of. The stage right after constructing a composite abstraction is perhaps the
most memory-critical one in M&S because this is right after we have multiplied
something out and before we've taken measures to make it smaller again.

I cannot comment on bitbucket directly with the given link, so one comment on
the diff there:

removed old comment:
    /* Set this to true to apply label reduction before shrinking, in
       addition to the times when it is usually applied. Some shrink
       strategies may require labels to be reduced (e.g. ones based on
       bisimulations), and others might prefer reduced labels because
       it makes their computation more efficient.
    ...
    */

This comment seems to be wrong -- it's not really "in addition to the times when
it is usually applied" since the option disables label reduction before
computing composites, if I read the code correctly.

Generally speaking, it may be useful to make the behaviour here configurable,
but it doesn't have to be at the shrink strategy level, it can be at the
merge_and_shrink_heuristic level:

- reduce labels before shrinking: yes/no
- reduce labels before merging: yes/no

So there would be four different combinations of the two options. I'd be
interested in seeing how well each of these performs for our usual heuristics.
We never really explored this, I think, and I think this might be some
interesting data to have.

Yes, always (sorry, that seemed to be the most plausible to me).

https://bitbucket.org/SilvanS/fd-dev/branch/issue522#diff

(Can you point to a diff?)

> I removed the "reduce labels before shrinking" option, which was true for
> bisimulation based shrinking, and false for bucket based shrinking.

What is the new behaviour? Always reduce labels before shrinking? Never?

I removed the "reduce labels before shrinking" option, which was true for
bisimulation based shrinking, and false for bucket based shrinking. The results
are really bad, but I don't understand why. There was a comment in the code that
label reduction is expensive and that bucket based shrinking does not benefit
from it, but why? In particular, do you have an idea why memory usage goes up so
much?

http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-04-07-issue522-base-v1-comp.html

This part of meta issue432.

The topic of this issue is quite general; from my list of TODOs:

- Does ShrinkStrategy::shrink_before_merge need to check if the new
  target size of an abstraction differs from the current size? check
  if this test is performed via "must_shrink" in all implementations
  of shrink strategies. If yes, then the method does not differ from
  ShrinkBisimulation:shrink_before_merge. As a consequence of having
  only one shrink_before_merge in the base class, we could make
  "compute shrink sizes" private. It should be clear however that
  every shrink strategy is responsible to decide on their own if
  they need/want to shrink or not.

- shrink(): why is the parameter called threshold and not target?
  The bisimulation class renames threshold to target and uses its
  own threshold parameter, which has a different meaning.

Considering the first item, I think that the confusing way of who is
calling what at the moment can be simplified. Considering the second
item, I wonder if we should have a threshold parameter as a general
option for shrink strategies? This is somewhat unspecific to
bisimulation based shrinking. It would also bring back together the
mechanisms of when to shrink and when not of all shrink stratgies.
This is also true for label reduction, which is applied before
shrinking with bisimulation, but afterwards for the other strategies.