(Merged six days ago.)

I noticed a small mistake: recomputing locally equivalent labels is only
necessary if combining potentially non-equivalent labels. I tested this and the
results are, if changed at all, better:
http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-06-23-issue539-v2-comp.html

Just for the record, simply integrating the latest default branch (with issue525
integrated; hg meld -r c66ee00a250a:d2e317621f2c) had the effet that (once
again) in the parcprinter domains, there is one instance where the shrinking
behavior is slightly changed, hence explaining the change in number of
expansions in the experiment posted above. In earlier issues where the exact
same difference occured, I figured out that this is due to the order in which
label groups are exposed to bisimulation shrinking. Still, in this case, I do
not understand what exactly in the changeset should have caused such a
difference in the behavior, but I just "accept" it as it is.

Not applying label reduction to transition systems incrementally did not have a
bad impact on computation time and even a slightly positive impact on memory
usage. Also the code is cleaner now, of course.

http://ai.cs.unibas.ch/_tmp_files/sieverss/2015-06-22-issue539-base-v1-comp.html

Merging and closing this one.

This is part of meta issue432.

I'd like to try to refactor the method that incorporates label reductions in
transition systems by potentially trading off speed against cleaner code.