Implement red-black trees for Lumping (bisimulation)

[ivan.zapreev]

Implement red-black trees for Lumping (bisimulation) and integrate them along with the splay-trees.

Holger Hermanns wrote:

I have some results in my thesis in which I compare the O(m lg n)
algorithm (that uses splay tree), the O(m lg2 n) algorithm (that
uses red-black tree), and Peter Buchholz's implementation of an
O(mn) algorithm. For large state spaces the difference between the
red-black and the O(mn) algorithm was about a factor of 500 while
the different between red-black and splay was around 7%	(red-black
is faster). Buchholz reference is P. Buchholz. Efficient computation
of equivalent and reduced representations for stochastic automaton.
International Journal of Computer Systems Science & Engineering,
15(2):93–103, 2000.

David Jansen's letter:

Derisavi describes in section 3.4 an experiment where he compared 
the lumping algorithms for an example system with up to 2 million 
states and 30 million transitions. It turns out that the lumping 
algorithm with splay trees is about 6% to 9% slower than the 
algorithm with red-black trees. Derisavi gives as reason that most 
trees are very small, so the constant factors are dominating the 
time complexity. Derisavi concludes: "Therefore, it is preferable to
use the red-black tree implementation in practice."

So, we might add another task to the optimizations to be done: 
namely change the implementation from splay trees to red-black 
trees. 

[ivan.zapreev]

The experiments done by Varun Agravala indicate that the results are not good. The implementation turns out to be less efficient. The main reason seems to be because the algorithms for read-black trees are much harder to implement in the efficient way. In case of splay trees it is much simpler and this is why we have the difference.