From 29597e014fad341ae43cf0e42be5146aea0d8179 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 30 Oct 2015 16:58:09 +0100 Subject: [PATCH] more work on reimplementation of weak bisim Former-commit-id: 5bdd8ea139cee1f8222828347d1a04967b411e4b --- .../BisimulationDecomposition.cpp | 3 + src/storage/bisimulation/Block.h | 2 +- ...ministicModelBisimulationDecomposition.cpp | 219 ++++++++++++++++-- ...erministicModelBisimulationDecomposition.h | 28 ++- src/storage/bisimulation/Partition.cpp | 88 +++++-- src/storage/bisimulation/Partition.h | 12 + 6 files changed, 308 insertions(+), 44 deletions(-) diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 79d154b78..e42b56228 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -160,6 +160,9 @@ namespace storm { this->performPartitionRefinement(); std::chrono::high_resolution_clock::duration refinementTime = std::chrono::high_resolution_clock::now() - refinementStart; + std::cout << "final partition: " << std::endl; + this->partition.print(); + std::chrono::high_resolution_clock::time_point extractionStart = std::chrono::high_resolution_clock::now(); this->extractDecompositionBlocks(); std::chrono::high_resolution_clock::duration extractionTime = std::chrono::high_resolution_clock::now() - extractionStart; diff --git a/src/storage/bisimulation/Block.h b/src/storage/bisimulation/Block.h index acb736eec..f9f46051f 100644 --- a/src/storage/bisimulation/Block.h +++ b/src/storage/bisimulation/Block.h @@ -20,7 +20,7 @@ namespace storm { // Creates a new block with the given begin and end. Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previous, Block* next, std::size_t id); - + Block() = default; Block(Block const& other) = default; Block& operator=(Block const& other) = default; diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index ac2128327..58296b254 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -4,7 +4,7 @@ #include #include #include -#include +#include #include "src/adapters/CarlAdapter.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -45,10 +45,12 @@ namespace storm { stateStack.reserve(this->model.getNumberOfStates()); storm::storage::BitVector nondivergentStates(this->model.getNumberOfStates()); - for (auto const& blockPtr : this->partition.getBlocks()) { + uint_fast64_t currentSize = this->partition.size(); + for (uint_fast64_t blockIndex = 0; blockIndex < currentSize; ++blockIndex) { + auto& block = *this->partition.getBlocks()[blockIndex]; nondivergentStates.clear(); - for (auto stateIt = this->partition.begin(*blockPtr), stateIte = this->partition.end(*blockPtr); stateIt != stateIte; ++stateIt) { + for (auto stateIt = this->partition.begin(block), stateIte = this->partition.end(block); stateIt != stateIte; ++stateIt) { if (nondivergentStates.get(*stateIt)) { continue; } @@ -59,7 +61,7 @@ namespace storm { for (auto const& successor : this->model.getRows(*stateIt)) { // If there is such a transition, then we can mark all states in the current block that can // reach the state as non-divergent. - if (this->partition.getBlock(successor.getColumn()) != *blockPtr) { + if (this->partition.getBlock(successor.getColumn()) != block) { isDirectlyNonDivergent = true; break; } @@ -74,7 +76,7 @@ namespace storm { nondivergentStates.set(currentState); for (auto const& predecessor : this->backwardTransitions.getRow(currentState)) { - if (this->partition.getBlock(predecessor.getColumn()) == *blockPtr && !nondivergentStates.get(predecessor.getColumn())) { + if (this->partition.getBlock(predecessor.getColumn()) == block && !nondivergentStates.get(predecessor.getColumn())) { stateStack.push_back(predecessor.getColumn()); } } @@ -82,18 +84,17 @@ namespace storm { } } - - if (nondivergentStates.getNumberOfSetBits() > 0 && nondivergentStates.getNumberOfSetBits() != blockPtr->getNumberOfStates()) { + if (!nondivergentStates.empty() && nondivergentStates.getNumberOfSetBits() != block.getNumberOfStates()) { // After performing the split, the current block will contain the divergent states only. - this->partition.splitStates(*blockPtr, nondivergentStates); + this->partition.splitStates(block, nondivergentStates); // Since the remaining states in the block are divergent, we can mark the block as absorbing. // This also guarantees that the self-loop will be added to the state of the quotient // representing this block of states. - blockPtr->data().setAbsorbing(true); - } else if (nondivergentStates.getNumberOfSetBits() == 0) { + block.data().setAbsorbing(true); + } else if (nondivergentStates.empty()) { // If there are only diverging states in the block, we need to make it absorbing. - blockPtr->data().setAbsorbing(true); + block.data().setAbsorbing(true); } } } @@ -147,13 +148,18 @@ namespace storm { return this->comparator.isOne(silentProbabilities[state]); } + template + bool DeterministicModelBisimulationDecomposition::hasNonZeroSilentProbability(storm::storage::sparse::state_type const& state) const { + return !this->comparator.isZero(silentProbabilities[state]); + } + template typename DeterministicModelBisimulationDecomposition::ValueType DeterministicModelBisimulationDecomposition::getSilentProbability(storm::storage::sparse::state_type const& state) const { return silentProbabilities[state]; } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitter(std::list*>& predecessorBlocks, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { for (auto block : predecessorBlocks) { // Depending on the actions we need to take, the block to refine changes, so we need to keep track of it. Block* blockToRefineProbabilistically = block; @@ -161,9 +167,8 @@ namespace storm { bool split = false; // If the new begin index has shifted to a non-trivial position, we need to split the block. if (block->getBeginIndex() != block->data().marker1() && block->getEndIndex() != block->data().marker1()) { - auto result = this->partition.splitBlock(*block, block->data().marker1()); - STORM_LOG_ASSERT(result.second, "Expected to split block, but that did not happen."); split = true; + this->partition.splitBlock(*block, block->data().marker1()); blockToRefineProbabilistically = block->getPreviousBlockPointer(); } @@ -243,7 +248,7 @@ namespace storm { this->partition.swapStatesAtPositions(predecessorPosition, currentPositionInSplitter + elementsToSkip + 1); } - // Since we had to move an already explored state to the right of the current position, + // Since we had to move an already explored state to the right of the current position, ++elementsToSkip; predecessorBlock.data().incrementMarker1(); predecessorBlock.data().incrementMarker2(); @@ -266,7 +271,7 @@ namespace storm { // We keep track of the probability of the predecessor moving to the splitter. increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue()); - + // Only move the state if it has not been seen as a predecessor before. storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor); if (predecessorPosition >= predecessorBlock.data().marker1()) { @@ -279,6 +284,169 @@ namespace storm { splitter.data().setMarker2(splitter.getBeginIndex()); } + template + void DeterministicModelBisimulationDecomposition::updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(bisimulation::Block& block) { + // For all states that do not have a successor in the block itself, we need to set the silent probability to 0. + std::for_each(silentProbabilities.begin() + block.data().marker1(), silentProbabilities.begin() + block.getEndIndex(), [] (ValueType& val) { val = storm::utility::zero(); } ); + + // For all states that do have a successor in the block, we set the silent probability to the probability + // stored in the vector of probabilities going to the splitter. + auto it = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.getBeginIndex(), probabilitiesToCurrentSplitter.begin() + block.getBeginIndex())); + auto ite = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.data().marker1(), probabilitiesToCurrentSplitter.begin() + block.data().marker1())); + std::for_each(it, ite, [] (boost::tuple const& tuple) { boost::get<0>(tuple) = boost::get<1>(tuple); } ); + } + + template + void DeterministicModelBisimulationDecomposition::updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block& block) { + for (auto stateIt = this->partition.begin(block), stateIte = this->partition.end(block); stateIt != stateIte; ++stateIt) { + if (hasNonZeroSilentProbability(*stateIt)) { + ValueType newSilentProbability = storm::utility::zero(); + for (auto const& successorEntry : this->model.getTransitionMatrix().getRow(*stateIt)) { + if (this->partition.getBlock(successorEntry.getColumn()) == block) { + newSilentProbability += successorEntry.getValue(); + } + } + silentProbabilities[*stateIt] = newSilentProbability; + } + } + } + + template + void DeterministicModelBisimulationDecomposition::computeConditionalProbabilitiesForNonSilentStates(bisimulation::Block& block) { + auto it = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.getBeginIndex(), probabilitiesToCurrentSplitter.begin() + block.getBeginIndex())); + auto ite = boost::make_zip_iterator(boost::make_tuple(silentProbabilities.begin() + block.data().marker1(), probabilitiesToCurrentSplitter.begin() + block.data().marker1())); + std::for_each(it, ite, [this] (boost::tuple const& tuple) { + if (!this->comparator.isZero(boost::get<0>(tuple))) { + boost::get<1>(tuple) /= storm::utility::one() - boost::get<0>(tuple); + } + } ); + } + + template + std::vector DeterministicModelBisimulationDecomposition::computeNonSilentBlocks(bisimulation::Block& block) { + auto less = [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return probabilitiesToCurrentSplitter[state1] < probabilitiesToCurrentSplitter[state2]; }; + this->partition.sortRange(block.getBeginIndex(), block.data().marker1(), less); + return this->partition.computeRangesOfEqualValue(block.getBeginIndex(), block.data().marker1(), less); + } + + template + std::vector DeterministicModelBisimulationDecomposition::computeWeakStateLabelingBasedOnNonSilentBlocks(bisimulation::Block const& block, std::vector const& nonSilentBlockIndices) { + // Now that we have the split points of the non-silent states, we perform a backward search from + // each non-silent state and label the predecessors with the class of the non-silent state. + std::vector stateLabels(block.getNumberOfStates(), storm::storage::BitVector(nonSilentBlockIndices.size() - 1)); + std::cout << "creating " << block.getNumberOfStates() << " labels " << std::endl; + + std::vector stateStack; + stateStack.reserve(block.getNumberOfStates()); + for (uint_fast64_t stateClassIndex = 0; stateClassIndex < nonSilentBlockIndices.size() - 1; ++stateClassIndex) { + for (auto stateIt = this->partition.begin() + nonSilentBlockIndices[stateClassIndex], stateIte = this->partition.begin() + nonSilentBlockIndices[stateClassIndex + 1]; stateIt != stateIte; ++stateIt) { + std::cout << "moving backward from state " << *stateIt << std::endl; + + stateStack.push_back(*stateIt); + stateLabels[this->partition.getPosition(*stateIt) - block.getBeginIndex()].set(stateClassIndex); + while (!stateStack.empty()) { + storm::storage::sparse::state_type currentState = stateStack.back(); + stateStack.pop_back(); + + for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) { + storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); + + std::cout << " found pred " << predecessor << " with value " << predecessorEntry.getValue() << std::endl; + if (this->comparator.isZero(predecessorEntry.getValue())) { + continue; + } + + // Only if the state is in the same block, is a silent state and it has not yet been + // labeled with the current label. + std::cout << "pred is at " << this->partition.getPosition(predecessor) << std::endl; + std::cout << "begin of block " << block.getBeginIndex() << std::endl; + std::cout << "accessing index " << (this->partition.getPosition(predecessor) - block.getBeginIndex()) << " of " << stateLabels.size() << std::endl; + std::cout << predecessor << " is in the same block as " << block.getId() << " ? " << (this->partition.getBlock(predecessor) == block) << std::endl; +// std::cout << isSilent(predecessor) << ", " << stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].get(stateClassIndex) << std::endl; + if (this->partition.getBlock(predecessor) == block && isSilent(predecessor) && !stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].get(stateClassIndex)) { + std::cout << "assigning label " << stateClassIndex << std::endl; + stateStack.push_back(predecessor); + stateLabels[this->partition.getPosition(predecessor) - block.getBeginIndex()].set(stateClassIndex); + } + } + } + } + } + + return stateLabels; + } + + template + void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue) { + computeConditionalProbabilitiesForNonSilentStates(block); + // First, we need to compute a labeling of the states that expresses which of the non-silent blocks they can reach. + std::vector nonSilentBlockIndices = computeNonSilentBlocks(block); + std::cout << "indices: " << std::endl; + for (auto el : nonSilentBlockIndices) { + std::cout << el << std::endl; + } + + for (int ind = 0; ind < nonSilentBlockIndices.size() - 1; ++ind) { + for (int inner = nonSilentBlockIndices[ind]; inner < nonSilentBlockIndices[ind + 1]; ++inner) { + std::cout << this->partition.getState(inner) << " is in class " << ind << std::endl; + } + } + + std::vector weakStateLabels = computeWeakStateLabelingBasedOnNonSilentBlocks(block, nonSilentBlockIndices); + + std::cout << "labels: " << std::endl; + for (auto el : weakStateLabels) { + std::cout << el << std::endl; + } + + // Then split the block according to this labeling. + // CAUTION: that this assumes that the positions of the states in the partition are not update until after + // the sorting is over. Otherwise, this interferes with the data used in the sorting process. + storm::storage::sparse::state_type originalBlockIndex = block.getBeginIndex(); + auto result = this->partition.splitBlock(block, + [&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { + std::cout << "comparing states " << state1 << " and " << state2 << std::endl; + std::cout << (this->partition.getPosition(state1) - originalBlockIndex) << " and " << (this->partition.getPosition(state2) - originalBlockIndex) << std::endl; + std::cout << "size: " << weakStateLabels.size() << std::endl; + std::cout << "begin is " << block.getBeginIndex() << std::endl; + std::cout << "orig begin " << originalBlockIndex << std::endl; + return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex]; + }, + [this, &splitterQueue] (bisimulation::Block& block) { + updateSilentProbabilitiesBasedOnTransitions(block); + + // Insert the new block as a splitter. + block.data().setSplitter(); + splitterQueue.emplace_back(&block); + }); + + // If the block was split, we also update the silent probabilities of the + if (result) { + updateSilentProbabilitiesBasedOnTransitions(block); + + // Insert the new block as a splitter. + block.data().setSplitter(); + splitterQueue.emplace_back(&block); + } else { + block.resetMarkers(); + } + } + + template + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + for (auto block : predecessorBlocks) { + std::cout << "found predecessor block " << block->getId() << std::endl; + if (*block != splitter) { + refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); + } else { + // If the block to split is the splitter itself, we must not do any splitting here. + block->resetMarkers(); + } + + block->data().setNeedsRefinement(false); + } + } + template void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { // The outline of the refinement is as follows. @@ -297,10 +465,11 @@ namespace storm { // Finally, we use the information obtained in the first part for the actual splitting process in which all // predecessor blocks of the splitter are split based on the probabilities computed earlier. - // (1) - std::list*> predecessorBlocks; + std::cout << "current partition is" << std::endl; + this->partition.print(); + std::cout << "refining using splitter " << splitter.getId() << std::endl; - // (2) + std::list*> predecessorBlocks; storm::storage::sparse::state_type currentPosition = splitter.getBeginIndex(); bool splitterIsPredecessorBlock = false; for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.end(splitter); splitterIt != splitterIte; ++splitterIt, ++currentPosition) { @@ -330,7 +499,7 @@ namespace storm { splitterIsPredecessorBlock = true; moveStateInSplitter(predecessor, predecessorBlock, currentPosition, elementsToSkip); } - + // Insert the block into the list of blocks to refine (if that has not already happened). if (!predecessorBlock.data().needsRefinement()) { predecessorBlocks.emplace_back(&predecessorBlock); @@ -352,9 +521,15 @@ namespace storm { // Finally, we split the block based on the precomputed probabilities and the chosen bisimulation type. if (this->options.type == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) { - refinePredecessorBlocksOfSplitter(predecessorBlocks, splitterQueue); + refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue); } else { - assert(false); + // If the splitter is a predecessor of we can use the computed probabilities to update the silent + // probabilities. + if (splitterIsPredecessorBlock) { + updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(splitter); + } + + refinePredecessorBlocksOfSplitterWeak(splitter, predecessorBlocks, splitterQueue); } } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index 0a5153786..4f0c5dd76 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -42,7 +42,7 @@ namespace storm { virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; private: - virtual void refinePredecessorBlocksOfSplitter(std::list*>& predecessorBlocks, std::deque*>& splitterQueue); + virtual void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -69,6 +69,9 @@ namespace storm { // Retrieves whether the given state is silent. bool isSilent(storm::storage::sparse::state_type const& state) const; + // Retrieves whether the given state has a non-zero silent probability. + bool hasNonZeroSilentProbability(storm::storage::sparse::state_type const& state) const; + // Retrieves whether the given predecessor of the splitters possibly needs refinement. bool possiblyNeedsRefinement(bisimulation::Block const& predecessorBlock) const; @@ -87,6 +90,29 @@ namespace storm { // Explores the remaining predecessors of the splitter. void exploreRemainingStatesOfSplitter(bisimulation::Block& splitter); + // Updates the silent probabilities of the states in the block based on the probabilities of going to the splitter. + void updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(bisimulation::Block& block); + + // Updates the silent probabilities of the states in the block based on a forward exploration of the transitions + // of the states. + void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block& block); + + // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. + void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + + // Refines the given block wrt to weak bisimulation in DTMCs. + void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue); + + // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed + // for weak bisimulation (on DTMCs). + void computeConditionalProbabilitiesForNonSilentStates(bisimulation::Block& block); + + // Computes the (indices of the) blocks of non-silent states within the block. + std::vector computeNonSilentBlocks(bisimulation::Block& block); + + // Computes a labeling for all states of the block that identifies in which block they need to end up. + std::vector computeWeakStateLabelingBasedOnNonSilentBlocks(bisimulation::Block const& block, std::vector const& nonSilentBlockIndices); + // A vector that holds the probabilities of states going into the splitter. This is used by the method that // refines a block based on probabilities. std::vector probabilitiesToCurrentSplitter; diff --git a/src/storage/bisimulation/Partition.cpp b/src/storage/bisimulation/Partition.cpp index d14034f53..ff432fa11 100644 --- a/src/storage/bisimulation/Partition.cpp +++ b/src/storage/bisimulation/Partition.cpp @@ -107,13 +107,18 @@ namespace storm { } template - void Partition::mapStatesToPositions(Block const& block) { - storm::storage::sparse::state_type position = block.getBeginIndex(); - for (auto stateIt = this->begin(block), stateIte = this->end(block); stateIt != stateIte; ++stateIt, ++position) { - this->positions[*stateIt] = position; + void Partition::mapStatesToPositions(std::vector::const_iterator first, std::vector::const_iterator last) { + storm::storage::sparse::state_type position = std::distance(this->states.cbegin(), first); + for (; first != last; ++first, ++position) { + this->positions[*first] = position; } } + template + void Partition::mapStatesToPositions(Block const& block) { + mapStatesToPositions(this->begin(block), this->end(block)); + } + template Block& Partition::getBlock(storm::storage::sparse::state_type state) { return *this->stateToBlockMapping[state]; @@ -172,10 +177,42 @@ namespace storm { return this->states.end(); } + template + void Partition::sortRange(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, std::function const& less, bool updatePositions) { + std::sort(this->states.begin() + beginIndex, this->states.begin() + endIndex, less); + if (updatePositions) { + mapStatesToPositions(this->states.begin() + beginIndex, this->states.begin() + endIndex); + } + } + + template + void Partition::sortBlock(Block& block, std::function const& less, bool updatePositions) { + sortRange(block.getBeginIndex(), block.getEndIndex(), less, updatePositions); + } + + template + std::vector Partition::computeRangesOfEqualValue(uint_fast64_t startIndex, uint_fast64_t endIndex, std::function const& less) { + auto it = this->states.cbegin() + startIndex; + auto ite = this->states.cbegin() + endIndex; + + std::vector::const_iterator upperBound; + std::vector result; + result.push_back(startIndex); + do { + upperBound = std::upper_bound(it, ite, *it, less); + result.push_back(std::distance(this->states.cbegin(), upperBound)); + it = upperBound; + } while (upperBound != ite); + + return result; + } + template std::pair>>::iterator, bool> Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { STORM_LOG_THROW(position >= block.getBeginIndex() && position <= block.getEndIndex(), storm::exceptions::InvalidArgumentException, "Cannot split block at illegal position."); + std::cout << "splitting block " << block.getId() << " at pos " << position << std::endl; + // In case one of the resulting blocks would be empty, we simply return the current block and do not create // a new one. if (position == block.getBeginIndex() || position == block.getEndIndex()) { @@ -199,27 +236,38 @@ namespace storm { template bool Partition::splitBlock(Block& block, std::function const& less, std::function&)> const& newBlockCallback) { - // Sort the range of the block such that all states that have the label are moved to the front. - std::sort(this->begin(block), this->end(block), less); + // Sort the block, but leave the positions untouched. + this->sortBlock(block, less, false); - // Update the positions vector. - mapStatesToPositions(block); + auto originalBegin = block.getBeginIndex(); + auto originalEnd = block.getEndIndex(); + + std::cout << "sorted block:" << std::endl; + for (auto stateIt = this->begin(block), stateIte = this->end(block); stateIt != stateIte; ++stateIt) { + std::cout << *stateIt << std::endl; + } + + auto it = this->states.cbegin() + block.getBeginIndex(); + auto ite = this->states.cbegin() + block.getEndIndex(); + std::cout << "splitting between " << block.getBeginIndex() << " and " << block.getEndIndex() << std::endl; - // Now we can check whether the block needs to be split, which is the case iff the changed function returns - // true for the first and last element of the remaining state range. - storm::storage::sparse::state_type begin = block.getBeginIndex(); - storm::storage::sparse::state_type end = block.getEndIndex() - 1; bool wasSplit = false; - while (less(states[begin], states[end])) { - wasSplit = true; - - auto range = std::equal_range(states.begin() + begin, states.begin() + end, states[begin], less); - begin = std::distance(states.begin(), range.second); - auto result = this->splitBlock(block, begin); - if (result.second) { + std::vector::const_iterator upperBound; + do { + std::cout << "it (" << *it << ") less than ite-1 (" << *(ite-1) << "? " << less(*it, *(ite - 1)) << std::endl; + upperBound = std::upper_bound(it, ite, *it, less); + std::cout << "upper bound is " << std::distance(this->states.cbegin(), upperBound); + if (upperBound != ite) { + wasSplit = true; + auto result = this->splitBlock(block, std::distance(this->states.cbegin(), upperBound)); newBlockCallback(**result.first); } - } + it = upperBound; + } while (upperBound != ite); + + // Finally, repair the positions mapping. + mapStatesToPositions(this->states.begin() + originalBegin, this->states.begin() + originalEnd); + return wasSplit; } diff --git a/src/storage/bisimulation/Partition.h b/src/storage/bisimulation/Partition.h index 5cb45b7e7..b78ae62bb 100644 --- a/src/storage/bisimulation/Partition.h +++ b/src/storage/bisimulation/Partition.h @@ -52,6 +52,15 @@ namespace storm { // of the states. std::pair>>::iterator, bool> splitBlock(Block& block, storm::storage::sparse::state_type position); + // Sorts the given range of the partitition according to the given order. + void sortRange(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, std::function const& less, bool updatePositions = true); + + // Sorts the block according to the given order. + void sortBlock(Block& block, std::function const& less, bool updatePositions = true); + + // Computes the start indices of equal ranges within the given range wrt. to the given less function. + std::vector computeRangesOfEqualValue(uint_fast64_t startIndex, uint_fast64_t endIndex, std::function const& less); + // Splits the block by sorting the states according to the given function and then identifying the split // points. The callback function is called for every newly created block. bool splitBlock(Block& block, std::function const& less, std::function&)> const& newBlockCallback); @@ -134,6 +143,9 @@ namespace storm { // Update the state to position for the states in the given block. void mapStatesToPositions(Block const& block); + + // Update the state to position for the states in the given range. + void mapStatesToPositions(std::vector::const_iterator first, std::vector::const_iterator last); // Swaps the positions of the two states given by their positions. void swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2);