From 754e168aceb150d0a45a869beac05d35ac483708 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 22 Oct 2014 12:51:27 +0200
Subject: [PATCH] Bugfix for bisimulation.

Former-commit-id: da93a5d4db51a3e06e05ca81428451ab1803685a
---
 ...icModelStrongBisimulationDecomposition.cpp | 29 +++++--------------
 1 file changed, 7 insertions(+), 22 deletions(-)

diff --git a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
index ea58b778c..1c11a8107 100644
--- a/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelStrongBisimulationDecomposition.cpp
@@ -23,6 +23,7 @@ namespace storm {
             if (prev != nullptr) {
                 prev->next = this;
             }
+            STORM_LOG_ASSERT(begin < end, "Unable to create block of illegal size.");
         }
         
         template<typename ValueType>
@@ -48,11 +49,13 @@ namespace storm {
         void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setBegin(storm::storage::sparse::state_type begin) {
             this->begin = begin;
             this->markedPosition = begin;
+            STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
         }
         
         template<typename ValueType>
         void DeterministicModelStrongBisimulationDecomposition<ValueType>::Block::setEnd(storm::storage::sparse::state_type end) {
             this->end = end;
+            STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size.");
         }
         
         template<typename ValueType>
@@ -401,35 +404,16 @@ namespace storm {
                 return block;
             }
             
-            // We only split off the smaller of the two resulting blocks so we don't have to update large parts of the
-            // block mapping.
-            bool insertAfterCurrent = false;
-            if ((block.getBegin() + position) > ((block.getEnd() - block.getBegin()) / 2)) {
-                // If the splitting position is far in the back, we create the new block after the one we are splitting.
-                insertAfterCurrent = true;
-            }
-            
             // Actually create the new block and insert it at the correct position.
-            typename std::list<Block>::iterator selfIt;
-            if (insertAfterCurrent) {
-                selfIt = this->blocks.emplace(block.hasNextBlock() ? block.getNextIterator() : this->blocks.end(), position, block.getEnd(), &block, block.getNextBlockPointer(), block.getLabelPtr());
-            } else {
-                selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
-            }
+            typename std::list<Block>::iterator selfIt = this->blocks.emplace(block.getIterator(), block.getBegin(), position, block.getPreviousBlockPointer(), &block, block.getLabelPtr());
             selfIt->setIterator(selfIt);
             Block& newBlock = *selfIt;
             
             // Resize the current block appropriately.
-            if (insertAfterCurrent) {
-                block.setEnd(position);
-            } else {
-                block.setBegin(position);
-            }
+            block.setBegin(position);
             
             // Update the mapping of the states in the newly created block.
-            for (auto it = this->getBegin(newBlock), ite = this->getEnd(newBlock); it != ite; ++it) {
-                stateToBlockMapping[it->first] = &newBlock;
-            }
+            this->updateBlockMapping(newBlock, this->getBegin(newBlock), this->getEnd(newBlock));
             
             return newBlock;
         }
@@ -729,6 +713,7 @@ namespace storm {
             typename std::vector<std::pair<storm::storage::sparse::state_type, ValueType>>::const_iterator end = partition.getEnd(block) - 1;
             storm::storage::sparse::state_type currentIndex = block.getBegin();
             
+            
             // Now we can check whether the block needs to be split, which is the case iff the probabilities for the
             // first and the last state are different.
             while (!comparator.isEqual(begin->second, end->second)) {