(This was part of meta issue432.)

Resolved.

Feel free to close.

Done. Unless there is anything else to do, this can be closed already.

Works for me. It would perhaps be nice if it could be easy to add it to other
places for debugging (e.g. if it's a simple function call
"report_peak_memory_delta" that could in principle be called from many places).

I implemented the delta output. There is only one drawback of taking out the
estimated memory usage of transition systems that I can see: we do not have any
memory statistics of single transition systems anymore. On the other hand, what
matters is the total memory usage of all transition systems (and everything else
related to merge-and-shrink), so I think this is fine.

Do you think one output of peak memory delta per merge-and-shrink iteration is
fine? I put it after the merge step.

Yes, peak memory is the only thing that can actually be measured. We must be
aware that there are many things that can make this inaccurate (memory
fragmentation, memory sometimes being requested from the OS in chunks of 1 MB or
more, memory that has already been allocated but not used), but at least we get
real data.

We want to replace all the estimated memory stuff with actual memory 
measurements. Malte, you once suggested to compute the delta of memory usage
before and after (or during) the merge-and-shrink construction. Did you mean the
existing "peak memory" mechanism we have? This probably works because before
starting the merge-and-shrink computation, not a lot of memory should have been
allocated, right?