In today's meeting, we were looking for issues where nothing happened in a long time and which we would therefore like to triage. In this case, I don't think linear merge strategies are that interesting any more since the existence of non-linear ones. Please speak up if you think differently.

As it currently is implemented, you can basically call normalize and compute
distances as long as you want, because both functions immediately return if
nothing has to be done. Of course, this incurs the function call overhead, but
this should be okay.

I would definitely not make a difference between using imperfect shrinking or
only perfect shrinking, this is why we have parameters.

What I have been doing in my current non-linear merge strategies is do
normalize, compute distances and reduce labels whenever requires/reasonable. So
I'd put label reduction on the same level as normalizing and computing distances.

I have checked again and is not only label reduction but also normalization and shrinking. 
The current loop is something like
while not finished:
   a1, a2 = merge_strategy()
   reduce_labels, normalize and compute_distances (for both a1 and a2)
   shrink_before_merge(a1, a2)
   a3 = new_abstraction (a1, a2)

Basically, I think that we could distinguish between two types of shrink_strategies, 
depending on whether they take as input a maximum number of abstract states. 
For those that don't, the loop could easily be:
while not finished:
   a1, a2 = merge_strategy()
   a3 = new_abstraction (a1, a2)
   reduce_labels, normalize and compute_distances (only a3)
   shrink(a3)

Advantages: 
  a) We don't repeat the calls to normalize, 
    compute_distances and shrink for atomic abstractions
    Though this is an small overhead anyway....
  b) All the abstractions in the pool are normalized and shrinked.
     The merge strategy can take into account that information

Disadvantages:
 a) We have to distinguish which type of shrink strategy
    are we using and adapt the loop. (or mantain a parameter)
 b) With non-linear merge strategies, there could be more
    shrinking if we postpone the shrink thanks to label reduction? Not sure about this.

> The M&S main loop should be refactored anyway at some point, so the best thing
> in my opinion is to keep everything else as it is and modify the main loop by
> having another call to labels->reduce, with potential dummy arguments.

I think this is a good solution for the moment, but then please add some
documentation to labels->reduce that states which arguments need to be provided
under which circumstances.

I have some hopes that with some nicer data structures to make label reduction
more efficient, we can get rid of the various variants like TWO_ABSTRACTIONS and
always do the complete fixpoint iteration.

The overall result would still be dependent on variable orders or something
similar, but I wouldn't mind having a fixed strategy if we can come up with
something that works alright across the board experimentally.

Maybe it would be a good idea to write down the various steps for the
merge-and-shrink refactoring and decide on a good order to look into them?

I see the point, but the labels->reduce() method also takes the set of all
abstractions as an argument, right?

The easiest way for now should be to simply provide a dummy pair and to make
sure via the options parsing that the TWO_ABSTRACTIONS label reduction method
cannot be used in conjunction with your merge strategy. I would avoid having two
separate methods.

The M&S main loop should be refactored anyway at some point, so the best thing
in my opinion is to keep everything else as it is and modify the main loop by
having another call to labels->reduce, with potential dummy arguments.

While integrating the new merge strategies I have detected a couple of issues 
regarding the order of the operations in the M&S loop.

Some of our merge criteria counts the number of transitions in the abstractions, 
so they need to have all the abstractions normalized and label reduction 
applied. I think it makes sense to apply label reduction as soon as possible, 
because the ideal is to always have all the abstractions normalized with respect 
to the smallest possible set of labels.

The problem here is that I cannot just move label reduction just after the 
creation of the new abstraction. This is because label reduction takes as input 
the two abstractions that are going to be merged, though they are only used by 
the TWO_ABSTRACTIONS label reduction. I am not sure if this type of label 
reduction is relevant in practice.

One possible way to solve this is to have two different methods for label 
reduction reduce_before_merge_strategy and reduce_after_merge_strategy and apply 
each label reduction method in a different moment. 

What do you think about this?

Issue created to add new linear merge strategies. The new strategies are based 
in a list of criteria, instead of the variable_order_finder. This makes them 
more flexible and they could be even extended to non-linear strategies (we 
implemented them before knowing about the new label reduction so we didn't think 
of that) 

With the appropiate criteria, the new strategies may imitate the old linear 
strategies, so they could even replace the old ones if we check that there are 
no significant performance issues.  Nevertheless, I am including them in a 
separate file merge_linear_criteria.h.