From 2f5f439f26fac4d9b2313df7b356d0624f84d2d3 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 4 Apr 2016 17:31:22 +0200
Subject: [PATCH] re-added (naive) splitter selection heuristic

Former-commit-id: 5c5166510da415725e77624cb8b4c7dc0b02e49e
---
 src/storage/bisimulation/BisimulationDecomposition.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp
index aedd4a998..5c5b3e667 100644
--- a/src/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/BisimulationDecomposition.cpp
@@ -240,6 +240,9 @@ namespace storm {
                 ++iterations;
 
                 // Get and prepare the next splitter.
+                // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but
+                // tends to work well.
+                std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
                 Block<BlockDataType>* splitter = splitterQueue.front();
                 splitterQueue.pop_front();
                 splitter->data().setSplitter(false);