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 @@ -48,11 +49,13 @@ namespace storm { void DeterministicModelStrongBisimulationDecomposition::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 void DeterministicModelStrongBisimulationDecomposition::Block::setEnd(storm::storage::sparse::state_type end) { this->end = end; + STORM_LOG_ASSERT(begin < end, "Unable to resize block to illegal size."); } template @@ -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::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::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>::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)) {