v1: first implementation

v2: scoring function compute double scores rather than int

v3: latest default branch

I merged this issue to be able to continue with integrating the merge strategies
based on SCCs and possibly also the dynamic MIASM variant.

Experiments with the latest default branch still look good (= nearly no changes
in performance): 
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue644-v3-issue644-v3-base-issue644-v3-compare.html

If nobody insists on reviewing, I'll merge this one tomorrow (as discussed
offline with Malte in our last meeting).

PS: pull request is still here
https://bitbucket.org/SilvanS/fd-dev/pull-requests/17/issue644/diff

After lots of rounds of refinements, due to using the new design with
my fast downward clone containing all the merge-and-shrink additions, I
think this converged to a good state. Let me summarize the design:


MergeStrategy:
- abstract base class
- reference to FactoredTransitionsystem
- get_next() to compute the next merge

There are three types of inheriting classes of MergeStrategy:
1) the specific class MergeStrategyPrecomputed
2) the specific class MergeStrategyStateless
3) "mixed" type/"combined" type: all individual strategies that do not
fit 1) or 2)

1) MergeStrategyPrecomputed:
- has a MergeTree
- the merge tree and the factored transition systems must be
synchronized
- get_next() returns the next merge according to the tree

MergeTreeFactory:
- abstract base class
- given the task, compute a merge tree for it
- given the current factored transition system (and a subset of
indices), compute a merge tree merging all the specified indices

Current instances:
MergeTreeFactoryLinear:
- linear merge strategies (variable order)

not in the default branch:
MergeTreeMiasm

2) MergeStrategyStateless:
- has a MergeSelector
- get_next() returns the next merge according to the selector

MergeSelector:
- abstact base class
- given a factored transition system (and a subset of indices),
select a merge candidate

Current instances:
MergeSelectorScoreBasedFiltering:
- has a list of MergeScoringFunction
- selects a merge candidate by iteratively computing scores for all
remaining merge candidates and filtering out all candidates with a
score different from the best (minimum) score

not in the default branch:
MergeSelectorScoreBasedWeightedSum:
- similar to the filtering approach, but computes all scores for all
candidates and makes the final decision by computed a weighted sum
over all scores

MergeScoringFunction:
- abstract base class
- given a factored transition system and a list of merge candidates,
compute a list of scores (one for each candidate)

Current instances:
MergeScoringFunctionGoalRelevance:
- prefer candidates with a goal relevant component
MergeScoringFunctionDFP:
- computes the DFP score
MergeScoringFunctionSingleRandom/MergeScoringFunctionTotalOrder:
- used for tie-breaking
- always find a single candidate with a best score, either by random
choice or a total transition system order


I'd like to merge this soonish, but of course ideally, someone would
have a look at some of the new classes before. I think most important
would be the MergeTree and MergeTreeFactory(Linear) classes, followed
by the MergeSelectorScoreBasedFiltering class. Everything related to
scoring functions and the new simple merge strategies results merely
from splitting up existing code (like MergeDFP) into chunks of code
according to the design explained above. This does not mean these
classes are perfect, but chances are higher they are "better".

I'll run experiments after integrating the latest default branch and
post them before proceeding with anything.

Regarding msg5477: we have decided not to implement such a numbering for now
because it's a complication and we're not currently planning to do anything with
it. The only thing I would suggest doing related to this at this point is to
document the issue in the code (i.e., mention somewhere that "stateless
selector" merge strategies *do* have control over the order of merges, while
"static merge tree" merge strategies do not), and to document clearly in which
order the merges in static merge tree are performed.

In the meantime, after lots of polishing and changing scoring functions to
compute double rather than int, I ran experiments for a new version v2:

http://ai.cs.unibas.ch/_tmp_files/sieverss/issue644-v2-issue644-v1-issue644-v2-compare.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue644-v2-dfp-tiebreaking-abp-report-issue644-v1-issue644-v2-compare.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue644-v2-dfp-tiebreaking-pba-report-issue644-v1-issue644-v2-compare.html

short summary: no changes in performance at all.

When I started using this issue's code branch in my other code bases, I came
across the following problem with the new merge tree class: given that a merge
tree is specified to always compute one specific next merge out of the set of
possible merges (= all "sibling" leaf nodes), e.g. to always use the left-most
sibling leaves, it may be difficult (I think even impossible) to implement a
merge tree for a given merge order (i.e. a sequence of merges). Conceptually, a
merge tree leaves the choice of which sibling leaves to merge next to the user,
but in practice, I think that the ordering of a set of merges that could all be
done in parallel could make a difference (e.g. for exact label reduction).

Do you think that adding an option to number internal tree nodes, thus imposing
an order on the merges, would be a reasonable way to deal with this issue? The
only use case for the scenario I see so far is when constructing a merge tree
from a given merge sequence, e.g. for manually predefined strategies or MIASM.
For strategies that "do not care" about the precise sequence of merges, but only
about the hierarchy of merges as defined conceptually by a tree, the option
could simply be ignored, leaving the choice to the merge tree itself.

Or maybe a merge tree isn't the best data structure after all, but a list of
merges could be more amenable? It could even be easier to update such a list, if
one decides to use it in a context where merges are not always performed
according to this list (e.g. when combining several merge strategies), hence
requiring to update the list to take into account that merge. But then again, a
merge tree better corresponds to the concept of a merge strategy, which
prescribes which transition systems to merge with which transition systems, but
not necessarily the precise order.

No surprises for the tiebreaking configurations either:

http://ai.cs.unibas.ch/_tmp_files/sieverss/issue644-v1-dfp-tiebreaking-abp-report-issue644-base-issue644-v1-compare.html
http://ai.cs.unibas.ch/_tmp_files/sieverss/issue644-v1-dfp-tiebreaking-pba-report-issue644-base-issue644-v1-compare.html

In the first experiment (tiebreaking: order atomic before product transition
systems), memory seems to very slightly increase, but the score_average
attribute comparison is still ok. For the other one (tiebreaking: order product
before atomics), the opposite is true. In the second experiment, there are also
small coverage fluctuations (+-1). 

All in all, experiments look fine to me: differences due to different usages of
RNGs are very small overall.

I made a first implementation of the proposed design. However, currently the
"score based merge selector" resembles rather to what Álvaro had in mind than to
a general "compute scores and combine them arbitrarily" class. This is mainly
due to the fact that it is unclear how a general score based merge selector
should make use of and combine different scoring functions. But for the moment
and to have something to discuss about, this is fine in my opinion (Álvaro
certainly agrees :-) ).

I ran a first batch of experiments, to compare the new to the old
implementation. For ease of comparison, the new framework includes backwards
compatibility command line syntax (i.e. merge_linear and merge_dfp).

http://ai.cs.unibas.ch/_tmp_files/sieverss/issue644-v1-issue644-base-issue644-v1-compare.html

The results look fine:
 - the differences for configuration dfp-f50k are due to different random
bucketing (even with the same random seed) due to different numbering of states
when computing a merge (X,Y) rather than (Y,X)
 - similarly, the difference in parcprinter for dfp-b50k is due to differences
in the bisimulation, resulting from a different numbering of states
 - (rl-f50k: instances that are close to the limit before/after the change)

A second batch of experiments that compares DFP tiebreaking configurations
(ICAPS 2016) is on the way.

Pull request: https://bitbucket.org/SilvanS/fd-dev/pull-requests/17/issue644/diff
However, as the diff consists of mainly "remove old classes, add new classes",
it is probably easier to have a "regular" code review for the new classes.

To 1)

Maybe my design suggestion was missleading, but I think that the
functionality that you suggest is covered entirely by
"MergeScoringFunction": a merge scoring function assigns a value to
every pair, which is the same as "selecting" a list of pairs, but more
flexible and general.

For a simple start, I would not add the parameters that you suggest to
MergeCriterionScore, because in the default branch of the code, there
is no use case for this yet.

Regarding the overhread of computing a value for all the pairs, you are
totally right. We hope that is doesn't impact the performance. If it
does, we need to reconsider alternatives.

I do not really understand what you mean with the comment "Probably,
this is the part I like less... etc." at this place, but as it is
repeated in item 3), I'll comment below.


To 2)

Single vs Several dynamic merge strategies: this was only intented as a
first idea. What I am meaning with "several dynamic merge strategies"
is a combination of different entire merge strategies, not of different
scoring functions, which is covered by "ScoreBasedMergeSelector". Of
course, conceptually, you are right: there is no difference between a
(list containing a) single element or a list, but it would change the
command line syntax. I think these are details that can be left aside
for the moment.


To 3)

You are right, running several merge-and-shrink instances with the same
merge strategy instance would not be possible, but at the moment, the
option parser does not allow to predefine merge strategies and use them
in several merge-and-shrink heuristics anyway. Furthermore, creating a
(dynamic) merge strategy is cheap, and re-creating it should not be
harmful. Also, I am not aware of anyone using several merge-and-shrink
instances yet. If this use case should be supported, we would need to
reconsider the entire design regarding static merge strategies. I
suggest to leave this aside until this use case arises.

I wouldn't sign the statement that dynamic strategies would probably
outperform static ones. MIASM, if implemented efficiently, would
probably still be the best strategy to date. And our new strategy based
on SCCs of the CG must also be considered a static variant, since it
precomputes "variable clusters" that can then be merged in an arbitrary
order. Also linear strategies, in their current form, are static
(although I already suggestd how to make them dynamic). Hence we
definitely need to consider static strategies, and give them a proper
inteface. It does not compromise the dynamic strategies: the overall
interface for a merge strategy still is pair<int, int> get_next() (the
FTS is stored as a reference).

(Shrink strategies are stateless and will remain, of course, and I
think that with issue655, we are making them even smaller and better.)

1) Regarding MergeSelector I'd prefer the alternative interface: 
- method: void select_merge(const FTS &fts, vector<pair<int, int> > & list);

This is more general, since it allows to combine multiple criteria to select 
the merge. 
Some of the selectors might be based on scoring functions (like 
MergeScoringFunction) but 
others can be based on different ideas.  For example a LinearMergeSelector 
might filter out 
all the elements that are not compatible with a linear merge. 

MergeScoringFunction is then what I was calling MergeCriterionScore. I added 
two optional 
parameters that allow setting a threshold such that all variables having a 
value below
the threshold are selected. By default the threshold is the best value
so that only the ones with best score are kept but this allows a bit more of 
flexibility in 
the selection. 

The only drawback that comes to my mind is the overhead of always generating 
all the pairs
 when its not necessary. A secondary method: vector<pair<int, int> > & 
select_merge(const FTS &fts); 
could be used to obtain the initial list of candidates directly using the first 
criterion.
Probably, this is the part I like less... because, what happens if we want to 
run different merge and shrink processes? If we run them sequentially we could 
try to re-initialize the merge strategy every time but I'm not sure this will 
always work, specially given the assumption that merge strategies can only be 
initialized with atomic abstractions. 

I'd rather prefer merge strategies, as well as shrink strategies to be 
stateless so that they only depend on the current FTS. Then, you could have a 
method: pair<int, int> next_merge(const FTS & fts);

I know that all this makes it harder to do the "static" strategies but I'm not 
sure why should we compromise the overall design of the merge interface just to 
please some strategies that will likely be outperformed by the dynamic ones. 

2) Regarding the SingleDynamicMergeStrategy and MultipleDynamicMergeStrategy:

If you change the interface of MergeSelector, in case that the list returned by
 the MergeSelector contains more than one element, one is selected at random. 
(I was allowing for level and reverse level final tie-breaker but I
guess they can be added as an additional merge selectors so it is fine to
force a final random tie-breaker.). 

I think it should be fairly easy to adapt merge_linear_criteria to be the 
implementation 
of SeveralDynamicMergeStrategies. 

Actually, I don't really see the reason for SingleDynamicMergeStrategy to exist 
since
 it is exactly the same as SeveralDynamicMergeStrategies when only one selector 
is provided. 


3) Regarding merge strategies, what happens if we want to run different merge 
and shrink processes? If we run them sequentially we could try to re-initialize 
the merge strategy every time but I'm not sure this will always work, specially 
given the assumption that merge strategies can only be initialized with atomic 
abstractions. 

I'd rather prefer merge strategies, as well as shrink strategies to be 
stateless so that they only depend on the current FTS. Then, you could have a 
method: pair<int, int> next_merge(const FTS & fts);

I know that all this makes it harder to do the "static" strategies but I'm not 
sure why should we compromise the overall design of the merge interface just to 
please some strategies that will likely be outperformed by the dynamic ones.

Malte and I discussed a bit about how we could divide responsibilities in new
merge strategies related classes. I wrote down some design ideas we discussed.
This is a non-polished version that Malte hasn't seen yet, but I thought that
you, Álvaro, might want to have a look at the notes already to see if you
understand our ideas and to give us some feedback on how to improve or change
things (also in the light of the things you may require for your classes).

I am not sure if attaching the file or pasting the text is better, but for
quoting parts of it or referring to items from the text, I decided to paste it.
From here, the contents of the file.



New design for merge strategies. Names are of course not set in stone
but up for discussion.


==== Facilities for "static" (i.e. precomputed) merge strategies =====

class MergeTreeFactory (abstract):

- input: (atomic) FTS/task?

- output: instance of class MergeTree (see below), where leafs are
labeled with variable ids (atomic TS)

- contract: functional class, one shot

Planned instances:

- LinearMergeTreeFactory: creates a linear merge tree, depending on the
given variable order (via VariableOrderFinder)



class MergeTree:

- built via MergeTreeFactory (exclusively?)

- pure data structure class: binary tree

- method: pair<int, int> remove_left_most_siblings();
Return the children of the left-most inner node which has exactly two
leafs as successors and remove the two leafs. Label the new leaf (the
former parent of the removed siblings) with the index of the merged TS
(under the contract that a newly merged TS obtains the "next" free
index in increasing order).

- method: update(pair<int, int> merge, option move_to_right/
move_to_left/move_to_random);
The two given merge indices *must* correspond to leafs of the tree,
otherwise the tree and the factored transition system of
merge-and-shrink are asynchronous. If the nodes corresponding to the
given merge are not two sibling successors of any inner node (in which
case the merge would have been performed by the merge tree anyway and
hence nothing would need to be done), "repair" the merge tree. There
are two possibilities to do so. Let left and right be the indices given
in the merge. Replace the label of the node labeled left (or right) by
the index of the merged TS and remove the right (left) node and its
parent, replacing the parent by its single surviving child. The given
option could determine how to update the merge tree.


============= Facilities for "dynamic" merge strategies =============

class MergeSelector (abstract):
- no internal state that would depend on the current state of the
merge-and-shrink heuristic
- method: pair<int, int> select_merge(const FTS &fts);
Select a next merge, purely based on the given FTS.
- contract: functional class, no side effects

Planned instance: ScoreBasedMergeSelector (see below).



class MergeScoringFunction (abstract)

- input: FTS

- output: (upper) matrix of scores for pairs of transition systems

- alternative input/output: additionally take a subset of
indices identifying transition systems that should be considered

- a score for a pair of transition systems indicates how "good" this
potential merge is, according to this class (-infinity: worst,
+infinity: best)

Planned instance: MergeScoringDFP.




class ScoreBasedMergeSelector
- maintain a list of MergeScoringFunction

- select_merge() computes the next merge based on the scoring
functions: take the first score function from the list and compute the
scores for all potential merges. If several pairs have the same best
score, ask the next score function from the list. Repeat until only one
candidate is left (always use random tie-breaking if no more score
function can be used).


========= Interaction with the merge-and-shrink heuristic=============

class MergeStrategy:

- initialization: reference to (atomic) FTS

- method: pair<int, int> next_merge();

- contract with merge-and-shrink heuristic: FTS (given initially) will
be updated according to the selected merge (the merge obtains the "next
free" index, i.e. the next higher number available. Initially, all
numbers from 0 to #vars - 1 are taken)

This is the class that communicates with the merge-and-shrink heuristic
and which is responsible for choosing merges. Its instantiations can
make use of the helper classes defined above.


Planned instances:

- SinglePrecomputedMergeStrategy: maintains a single instance of
MergeTree (via options), constructed via merge tree factory.

    => only use case in the default branch so far: MergeLinear

    (Comment to Álvaro: to ease integration of your linear merge
    strategies, they could be "interpreted" as dynamic ones (i.e. fit
    the MergeScoringFunction class) by trying to interprete, e.g., CGGL
    as list of scoring functions that, in the order, prefers a pair
    containing "the composite", a pair where the atomic TS's variable
    is "causally linked to already merged variables", a pair where the
    atomic TS's variable is a goal variable, or finally a pair where
    the atomic TS's variable is the next variable according to Fast
    Downward's variable order.)

- SingleDynamicMergeStrategy: maintains a single instance of
MergeSelector (via options)

    => only use case in the default branch so far: MergeDFP

(- more combinations may arise in future:
    - CombinedPrecomputedDynamicMergeStrategy (maintain a single merge
    tree and a single merge selector. Instantiating classes must
    provide a way to choose which one to use at which merge decision).

    - SeveralPrecomputedMergeStrategies: list of merge trees

    - SeveralDynamicMergeStrategies: list of merge selectors

    - ...)

Regarding 1), I still do not understand how a filter interface allows
to combine, say, DFP with a linear merge strategy other than using the
latter for tiebreaking. And even there, I do not see how this works
conceptually: after performing a few non-linear merges with DFP, if we
then run into a set of potential merges ranked equal by DFP, how do we
use a linear strategy as tiebreaker? At this point, we do not have
"variables" anymore, but we have subsets of merged variables.

Regarding 2), I am not sure if a change to the merge-and-shrink main
loop is required. I still think that any existing merge strategy could
simply use other merge strategies like it desires. For "precomputed"
strategies, there would be the need to inform another merge strategy
about the actual merge that was performed. That's where my original
suggestion to have a different interface for precomputed merge
strategies stem from.

Generally, however, I like the idea of having "merge criteria". Maybe a
better design would be to have merge criteria (rather than strategies)
that return a merge, given a (sub)set of transition systems, and can be
informed about future merges. A merge strategy, when asked for a merge,
can then ask a single criterion or choose among a list, or something
else (e.g. compute a ranking on all criteria). This design would have
the advantage that the existing interface of merge strategies would not
need to be changed. Building on my original suggestion, it still may be
useful to have "dynamic" criteria and "precomputed" ones.

Going back to this discussion, I think there are two separate issues: 
1) How to combine different criteria (e.g., DFP, level, causal graph relevance, 
etc.) during a run of M&S.
2) How to extend M&S to run multiple merge strategies. 

The filter interface is a solution for (1). Here, we only have a single merge 
strategy, but it's composed of a list of merge criteria. You can have a look at 
the merge_linear_criteria class for an example. I'll integrate this in the 
current FD version soon. I'll share that repository with you so that you can 
suggest some changes.
Actually, it can even cover the case of alternating between different M&S 
strategies by adding some parameters that enable/disable some of the filters.

The solution for (2) is a separate issue that require further considerations, 
because it even requires to adapt the main loop in the M&S construction method 
(build_transition_system). It also requires some modification to the interface 
of merge and shrink strategies. My suggestions in this part are: 
   a) Change the current initialize(const std::shared_ptr<AbstractTask> task) 
for some initialize(const FactoredTransitionSystem & fts).
   b) Make a AlternatingMergeStrategy that has a list of merge strategies and 
every time that we call initialize, sets the following merge in a round-robin 
fashion.

In your suggestion, I understand that you can use tiebreaking criteria. But I
don't understand how you can combine strategies in a different way than using a
second merge strategy for tiebreaking, if the first one does not compute a
single solution already. Maybe we need some pseudocode to discuss this.

Yes, my suggestion is to do a merge strategy that consists of a list of merge 
criteria. DFP is a criterion, symmetries another, etc. 

Of course, if you need to have multiple different strategies that has to be 
handled separately. But I don't see how making the subclasses to return a 
numeric value (score) helps for this either. 

"For use DFP for a few merges, then use symmetries/MIASM or whatever, then 
again DFP etc". Well, this one actually could be handled by introducing some 
parameters in the merge_criterion base class that allow to disable a filter in 
certain conditions.

Hi Álvaro, thanks for sharing your thoughts on this issue!

I think the filter-interface is very useful for combining several merge
strategies for tiebreaking. This might well work for non-linear strategies as well. 

On the other hand, I don't think this helps when it comes to combining merge
strategies in an arbitrary way, and this is what I need to do in several cases.
I don't want to first compute a first merge strategy to exclude specific merges,
but I rather want to either rank all merges using several merge strategies, or I
want to use merge strategies in an alternating way, e.g. use DFP for a few
merges, then use symmetries/MIASM or whatever, then again DFP etc. In these
cases, the filter-interface won't work.

Hi, 

I do not have a clear opinion on the precomputed strategies. For the dynamic 
strategies, however, I think the interface assigning a value to each possible 
merge is a bit more specific than necessary. Let me suggest you a way that I 
think it's more generic. 

What I did for integrating the linear strategies that we use in the ECAI14 
paper is to have an abstract class MergeCriterion. The main part of the 
interface is a function: 

virtual void filter(const std::vector<Abstraction *> &all_abstractions, 
std::vector <int> & vars, Abstraction * abstraction);

This function takes as input: 
  - all_abstractions: set of all the transition systems. 
  - vars: the list of vars that may me merged.
  - abstraction: the abstraction that we are going to choose. 

What filter does is to remove items from vars. It may remove all but one (hence 
definitively deciding the next merge to do). But it also may remove only a 
subset. Then, we have the class LinearMergeStrategy that has a list of criteria 
and a final tie-breaking (linear, reverse or random). The idea then is that we 
can define multiple merge stragies by combining multiple criterion. 

To put an example. There are many merges that maximize the score of Merge DFP. 
Therefore all that Merge DFP must do is to filter out the ones that don't 
maximize the value. Then, we can compose it with other strategies (e.g. based 
on the causal graph).

This does not complicate the implementation with respect to the version 
selecting the item with highest value. I implemented a templated function that 
allows you to use a score for each variable in order to filter the variables 
that maximize or minimize the value. 

template<class T> void filter_best(std::vector <int> & vars, const 
std::vector<T> & criterion, 
			 bool minimize, double opt_margin=1, double opt_diff=0)  
const; 

Opt_margin and opt_diff allow to not be strict in selecting the maximum but 
letting other variables that are worse than the maximum only by a small margin. 
It should not be too difficult to modify this function so that it takes as 
input a function that computes the criterion (instead of precomputing it 
beforehand).

In summary, with this design you can still easily implemnt all the merge 
strategies based on giving a score to each merge, but it is much more easy to 
compose different criteria and implement some other strategies that do not rely 
on computing numeric values. 

Of course, the disadvantage is that, in non-linear strategies you will need to 
generate a list of pairs of abstractions to be merged (a vector<pair<int, int> 
> instead of vector<int>). This is a bit of an overhead and it should be 
measured but sincerely I don't think a quadratic factor on the number of 
variables will be the bottleneck in M&S.    

I attach the merge strategies that we were using in case that you want to take 
a look.

I think I'll give it a try. If we can come up with a somewhat preliminary design
that helps integrating tieabreaking for DFP and possibly also SCCs, that would
be great, having in mind that these strategies could be helpful both for the
work with Jörg and Alvaro and maybe also for Daniel's master's thesis.

I think I understand the difficulties, but as far as I understand the proposed
solution, I am not sure it is as clean and elegant as I would like.

Would you prefer to work on your proposed approach now, at the risk that I might
want some changes to the design later, or would you prefer to do more
pre-planning now to explore the design space, at the risk that it might take a
long time until we can find enough time for this, stalling the issue in the
meantime?

The interface to get/compute the next pair of abstractions to merge remains the
same, yes, but a precomputed merge strategy needs some data structures, while a
dynamic one does not necessarily. A precomputed strategy would compute a merge
tree once, and this merge tree would need to be updated when a merge is
performed which differs from the one the merge strategy prescribes (possible
when combining different merge strategies). A dynamic merge strategy that ranks
every pair could have a precomputed configurable order in which transition
systems are considered (as a preparation to merge the new DFP with tiebreaking).

I'm not sure I understood all the details, but the direction sounds good.

At the moment it's not really clear to me why we need separate interfaces
(conceptually, isn't "precomputed" just a special case in some sense), but
perhaps this will be clearer when we progress with the design and implementation.

This is part of meta issue567.

I would like to improve the interface that current merge strategies have, in the
light of new merge strategies I'd like to integrate, such as DFP with
tiebreaking, SCCs, or dynamic MIASM.

Currently, merge strategies implement a "get_next" method which returns two
transition system indices to be merged next. I am thinking mainly of merge
strategies which combine existing ones or use existing ones as fallback
strategies (especially all factored symmetry based strategies). This is
difficult in particular with respect to precomputed merge strategies. For
"dynamic" (= not precomputed) merge strategies, it could be useful to compute a
next pair for a given subset of transition systems only. Similarly, it could be
useful to compute a precomputed merge strategy on a subset of transition systems
only (I am mainly thinking of using linear merge strategies on a subset of
variables such as when merging an SCC).

Suggestion:
Make a difference between "MergeStrategyPrecmomputed" and "MergeStrategyDynamic"
(we can discuss names of course). Each of them should be able to be used on a
subset of transition systems of the current factored transition system. 

Assuming that all types of dynamic merge strategies need to compare every
possible merge against each other, we could implement the order in which these
candidate pairs are considered in the baseclass (in the spirit of the ordering
options of our tiebreaking-DFP strategy). Subclasses then only would need to
provide a method that computes a score for a given transition system pair.
(Things get more complicated if one wants to go over all pairs several times,
e.g. to remember specific pairs in case no pair fulfils a required condition, or
to compute scores relative to the worst and best score of all pairs. But for the
moment, only DFP would be an instance of MergeStrategyDynamic, and hence this
simple "consider all pairs" in the desired order should work.)

For precomputed merge strategies, it could be useful store an actual merge tree.
Currently, we only have linear precomputed merge strategies, and they only
return the "next variable" to merge, which makes it difficult to be used after
performing a few merges with a different (non-linear) strategy. Having
precomputed merge strategies stored in a merge tree, we could update the merge
tree whenever we perform a merge which would *not* have been performed according
to this merge tree. Of course, merging two nodes from different subtrees leaves
the question where to put the resulting node in the tree, but this could be an
option of the merge strategy (use "left", "right", or "random", for example).
MIASM (if we ever wanted to integrate it), uses such a merge tree to compute the
merge order.

Maybe it is worth discussing this also offline, what do you think?