From 4b8f2e7a0b507dcc17a65380d6a28158bd8ee4c0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 4 Dec 2014 11:53:42 +0100
Subject: [PATCH] Next splitter is now chosen more deterministically.

Former-commit-id: 7f92208d1cf480803eb24e671bcd054593a41d7f
---
 src/storage/DeterministicModelBisimulationDecomposition.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
index c16e21032..28a958cd5 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -757,7 +757,7 @@ namespace storm {
             // Then perform the actual splitting until there are no more splitters.
             while (!splitterQueue.empty()) {
                 // Optionally: sort the splitter queue according to some criterion (here: prefer small splitters).
-                std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } );
+                std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates() || (b1->getNumberOfStates() == b2->getNumberOfStates() && b1->getId() < b2->getId()); } );
 
                 // Get and prepare the next splitter.
                 Block* splitter = splitterQueue.front();