Done.

Thanks, Silvan! Can you add points 8. and 12. to our new meta issue if they are
not already covered in some way and then mark this one as resolved?

I think we may not need to discuss in person, I just had a look at the "open
action items" mentioned in msg1694.

5. is resolved with issue483
7. is resolved
8. is still an open TODO (with a comment in the code)
10. is still open (an item on our list)
11. I am not sure. I think this refers to the huge comment that used to be at
the top of abstraction.cc, but which has been removed with the integration of
the new label reduction (if there was anything interesting left, we have it in
our list)
12. is certainly still a good idea
15. is resolved

Sounds good -- I'll wait for you to ping me.

Interesting! Some of the comments I just browsed through already made it onto my
"this is strange, this should be changed" list. I don't know if the meta issue
should contain so many detailed comments or only the pointers to the associated
issues... Let's discuss this and the comments offline next week?

Interesting, I found this old issue hidden deep in the tracker.

@Silvan: I think we should go over the comments in this issue, see which of them
are useful additions to the ongoing M&S refactoring effort, mention them in the
new issue, and then mark this one as resolved. Do you want to do this, should I,
or should we do it together?

With issue268 resolved, the following additional things are now done:

- The "subdirectory" part of 1., but not the "namespace" part. I guess the
  namespace part is covered by issue64, so we can strike through point 1.
- The remaining part of 6.

The following points remain:

5., 7., 8., 10., 11., 12., 15.

With so many different points, this is more of a meta-issue than a single issue,
so I've factored out the next thing to work on (cleanup) into the new issue268.
I've nosied everyone nosied here; as always, feel free to remove your name.

The following points are already done as part of the ongoing work on issue211:

2., 3., 4. (via the new "threshold" parameter), the deletion part of 6. (the
renaming part should wait until the code is more stable, since it makes diffing
more difficult), 9., 13., 14.

15. Make m&s code pluggable. It used to be pluggable, but right now it's not
pluggable any more because the option parser depends on shrink_strategy.h. It
would be good to move this code out of the option parser and into the
merge-and-shrink code -- also to reduce compile-time dependencies.

Point 13. is already done; other similar terminology changes should be applied
to other classes though. But that's already covered in point 11., so doesn't
need a new point.

14. The code that triggers a clean-up after detecting irrelevant or unreachable
abstract states needs to be amended. Right now it's called as follows:

        ShrinkBisimulation nolimit(false, false);
        nolimit.shrink(*this, 1, true);

This number should not be 1, since that leads to very misleading output. Using
num_states should work, but we need to check if there's anything magic going on
for value 1 that we might need to adapt.

13. Terminology: The terminology in class "OperatorRegistry" should follow the
new vocabulary in the M&S IJCAI paper and the journal paper we're working on.
"LabelReducer", "original_labels", "reduced_labels" instead of
"OperatorRegistry", "operators", "canonical_operators" etc.

9. Get rid of references to QUITE_A_LOT and other powers of 10.

10. Decouple the abstraction mapping from the abstract transition system (and
delete the abstract transition systems at the end of heuristic construction;
currently "release_memory" basically does that, but it's not as clean as it
could/should be).

11. Meta-point: There is a bunch of TODOs near the start of raz_abstraction.cc,
many of which are still relevant.

12. Meta-point: Go through M&S code comments to find TODOs, HACKs etc.

8. The "peak_memory" stuff should probably be revised, maybe using actual memory
usage now that we have this facility. (That measures *globally* used memory of
course, but if we compute the delta before and after M&S construction, this
should give us the information we want, I think.)

7. Reimplement MergeAndShrinkHeuristic::compute_shrink_sizes and document how it
works.

The current implementation is almost fine except for one case, where size1 *
size2 exceeds max_abstract_states, but size1 is below balanced_size. In that
case newsize2 is smaller than necessary.

Proposed new algorithm:
- First test max_abstract_size_before_merge as currently.
- Test if product is too large as currently.
- If yes, compute balanced_size. If both are larger than balanced_size,
  first shrink second abstraction to balanced_size and leave remaining space
  for first abstraction. If exactly one is larger than balanced_size,
  shrink it to whatever is possible.

(This is identical to the current strategy except for the case mentioned above.)

6. Delete unused_* files, rename raz_X ... files to X.

[Deleted previous message with wrong running number.]

5. Find the best shrink strategy for pruning irrelevant/unreachable
states. Should be fast. Possibly create a dedicated strategy.

Numbering these for easier reference:

1. The m&s code needs its own subdirectory (merge_and_shrink) and namespace
(MergeAndShrink).

2. The Abstraction class shouldn't need to know which shrink strategies exist
(see also the friends near the top of the class definition).

3. The logic that decides how and with which target size to call shrink()
shouldn't need to handle the "has no limit" case separately; to that code, "has
no limit" should be the same as setting a gargantuan limit (say,
numeric_limits<int>::max()). More generally, if we currently have shrink
strategies that are explcitly "no-limit", we shouldn't; this should be handled
through the abstraction size parameter.

4. In relation to the previous change, we should make sure that bisimulation is
called that bisimulation (certainly the non-approximate variants) is always
called when it can help reduce the size of the current abstraction, even if no
shrinking is currently necessary. I'm not sure if the current code really
accomplishes that because the "do we need to shrink at all" test skips the
special-casing for bisimulation strategies. (Maybe this wasn't a problem in
Raz's code because there the limit was always only 1?)

This issue collects some refactorings/changes of the M&S code that should be
done after issue211 has landed.