diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index d550c510c..f22ddcc39 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -6,6 +6,8 @@ #include "src/models/sparse/Ctmc.h" #include "src/models/sparse/StandardRewardModel.h" +#include "src/storage/bisimulation/DeterministicBlockData.h" + #include "src/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -21,13 +23,13 @@ namespace storm { using namespace bisimulation; - template - BisimulationDecomposition::Options::Options(ModelType const& model, storm::logic::Formula const& formula) : Options() { + template + BisimulationDecomposition::Options::Options(ModelType const& model, storm::logic::Formula const& formula) : Options() { this->preserveSingleFormula(model, formula); } - template - BisimulationDecomposition::Options::Options(ModelType const& model, std::vector> const& formulas) : Options() { + template + BisimulationDecomposition::Options::Options(ModelType const& model, std::vector> const& formulas) : Options() { if (formulas.empty()) { this->respectedAtomicPropositions = model.getStateLabeling().getLabels(); this->keepRewards = true; @@ -40,13 +42,13 @@ namespace storm { } } - template - BisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) { + template + BisimulationDecomposition::Options::Options() : measureDrivenInitialPartition(false), phiStates(), psiStates(), respectedAtomicPropositions(), keepRewards(false), type(BisimulationType::Strong), bounded(false), buildQuotient(true) { // Intentionally left empty. } - template - void BisimulationDecomposition::Options::preserveFormula(ModelType const& model, storm::logic::Formula const& formula) { + template + void BisimulationDecomposition::Options::preserveFormula(ModelType const& model, storm::logic::Formula const& formula) { // Disable the measure driven initial partition. measureDrivenInitialPartition = false; phiStates = boost::none; @@ -62,8 +64,8 @@ namespace storm { this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas()); } - template - void BisimulationDecomposition::Options::preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula) { + template + void BisimulationDecomposition::Options::preserveSingleFormula(ModelType const& model, storm::logic::Formula const& formula) { keepRewards = formula.containsRewardOperator(); // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula. @@ -76,8 +78,8 @@ namespace storm { this->checkAndSetMeasureDrivenInitialPartition(model, formula); } - template - void BisimulationDecomposition::Options::checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula) { + template + void BisimulationDecomposition::Options::checkAndSetMeasureDrivenInitialPartition(ModelType const& model, storm::logic::Formula const& formula) { std::shared_ptr newFormula = formula.asSharedPointer(); if (formula.isProbabilityOperatorFormula()) { @@ -115,8 +117,8 @@ namespace storm { } } - template - void BisimulationDecomposition::Options::addToRespectedAtomicPropositions(std::vector> const& expressions, std::vector> const& labels) { + template + void BisimulationDecomposition::Options::addToRespectedAtomicPropositions(std::vector> const& expressions, std::vector> const& labels) { std::set labelsToRespect; for (auto const& labelFormula : labels) { labelsToRespect.insert(labelFormula->getLabel()); @@ -131,16 +133,16 @@ namespace storm { } } - template - BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, Options const& options) : model(model), backwardTransitions(model.getBackwardTransitions()), options(options), partition(), comparator(), quotient(nullptr) { + template + BisimulationDecomposition::BisimulationDecomposition(ModelType const& model, Options const& options) : model(model), backwardTransitions(model.getBackwardTransitions()), options(options), partition(), comparator(), quotient(nullptr) { // Fix the respected atomic propositions if they were not explicitly given. if (!this->options.respectedAtomicPropositions) { this->options.respectedAtomicPropositions = model.getStateLabeling().getLabels(); } } - template - void BisimulationDecomposition::computeBisimulationDecomposition() { + template + void BisimulationDecomposition::computeBisimulationDecomposition() { std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); std::chrono::high_resolution_clock::time_point initialPartitionStart = std::chrono::high_resolution_clock::now(); @@ -188,19 +190,21 @@ namespace storm { } } - template - void BisimulationDecomposition::performPartitionRefinement() { + template + void BisimulationDecomposition::performPartitionRefinement() { // Insert all blocks into the splitter queue that are initially marked as being a (potential) splitter. - std::deque splitterQueue; - std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr const& block) { if (block->isMarkedAsSplitter()) { splitterQueue.push_back(block.get()); } } ); + std::deque*> splitterQueue; + std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr> const& block) { if (block->isMarkedAsSplitter()) { splitterQueue.push_back(block.get()); } } ); // Then perform the actual splitting until there are no more splitters. + uint_fast64_t iterations = 0; while (!splitterQueue.empty()) { + ++iterations; // 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(); } ); // Get and prepare the next splitter. - Block* splitter = splitterQueue.front(); + Block* splitter = splitterQueue.front(); splitterQueue.pop_front(); splitter->unmarkAsSplitter(); @@ -208,23 +212,24 @@ namespace storm { // std::cout << "refining based on splitter " << splitter->getId() << std::endl; refinePartitionBasedOnSplitter(*splitter, splitterQueue); } + std::cout << "done within " << iterations << " iterations." << std::endl; } - template - std::shared_ptr BisimulationDecomposition::getQuotient() const { + template + std::shared_ptr BisimulationDecomposition::getQuotient() const { STORM_LOG_THROW(this->quotient != nullptr, storm::exceptions::IllegalFunctionCallException, "Unable to retrieve quotient model from bisimulation decomposition, because it was not built."); return this->quotient; } - template - void BisimulationDecomposition::splitInitialPartitionBasedOnStateRewards() { + template + void BisimulationDecomposition::splitInitialPartitionBasedOnStateRewards() { std::vector const& stateRewardVector = model.getUniqueRewardModel()->second.getStateRewardVector(); partition.split([&stateRewardVector] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return stateRewardVector[a] < stateRewardVector[b]; }); } - template - void BisimulationDecomposition::initializeLabelBasedPartition() { - partition = storm::storage::bisimulation::Partition(model.getNumberOfStates()); + template + void BisimulationDecomposition::initializeLabelBasedPartition() { + partition = storm::storage::bisimulation::Partition(model.getNumberOfStates()); for (auto const& label : options.respectedAtomicPropositions.get()) { if (label == "init") { @@ -243,8 +248,8 @@ namespace storm { // partition.print(); } - template - void BisimulationDecomposition::initializeMeasureDrivenPartition() { + template + void BisimulationDecomposition::initializeMeasureDrivenPartition() { std::pair statesWithProbability01 = this->getStatesWithProbability01(); boost::optional representativePsiState; @@ -252,7 +257,7 @@ namespace storm { representativePsiState = *options.psiStates.get().begin(); } - partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState); + partition = storm::storage::bisimulation::Partition(model.getNumberOfStates(), statesWithProbability01.first, options.bounded || options.keepRewards ? options.psiStates.get() : statesWithProbability01.second, representativePsiState); // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved. @@ -264,8 +269,8 @@ namespace storm { // partition.print(); } - template - void BisimulationDecomposition::extractDecompositionBlocks() { + template + void BisimulationDecomposition::extractDecompositionBlocks() { // Now move the states from the internal partition into their final place in the decomposition. We do so in // a way that maintains the block IDs as indices. this->blocks.resize(partition.size()); @@ -278,12 +283,12 @@ namespace storm { } } - template class BisimulationDecomposition>; - template class BisimulationDecomposition>; + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; #ifdef STORM_HAVE_CARL - template class BisimulationDecomposition>; - template class BisimulationDecomposition>; + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; + template class BisimulationDecomposition, bisimulation::DeterministicBlockData>; #endif } } diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 305638438..816dc7436 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -29,7 +29,7 @@ namespace storm { /*! * This class is the superclass of all decompositions of a sparse model into its bisimulation quotient. */ - template + template class BisimulationDecomposition : public Decomposition { public: typedef typename ModelType::ValueType ValueType; @@ -158,7 +158,7 @@ namespace storm { * @param splitter The splitter to use. * @param splitterQueue The queue into which to insert the newly discovered potential splitters. */ - virtual void refinePartitionBasedOnSplitter(bisimulation::Block const& splitter, std::deque& splitterQueue) = 0; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) = 0; /*! * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks @@ -204,7 +204,7 @@ namespace storm { Options options; // The current partition (used by partition refinement). - storm::storage::bisimulation::Partition partition; + storm::storage::bisimulation::Partition partition; // A comparator used for comparing the distances of constants. storm::utility::ConstantsComparator comparator; diff --git a/src/storage/bisimulation/Block.cpp b/src/storage/bisimulation/Block.cpp index 2de49e62a..52dafb06d 100644 --- a/src/storage/bisimulation/Block.cpp +++ b/src/storage/bisimulation/Block.cpp @@ -4,6 +4,7 @@ #include #include "src/storage/bisimulation/Partition.h" +#include "src/storage/bisimulation/DeterministicBlockData.h" #include "src/exceptions/InvalidOperationException.h" #include "src/utility/macros.h" @@ -12,136 +13,180 @@ namespace storm { namespace storage { namespace bisimulation { - Block::Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previousBlock, Block* nextBlock, std::size_t id) : nextBlock(nextBlock), previousBlock(previousBlock), beginIndex(beginIndex), endIndex(endIndex), markedAsSplitter(false), needsRefinementFlag(false), absorbing(false), id(id) { + template + Block::Block(storm::storage::sparse::state_type beginIndex, storm::storage::sparse::state_type endIndex, Block* previousBlock, Block* nextBlock, std::size_t id) : nextBlock(nextBlock), previousBlock(previousBlock), beginIndex(beginIndex), endIndex(endIndex), markedAsSplitter(false), needsRefinementFlag(false), absorbing(false), id(id), mData() { if (nextBlock != nullptr) { nextBlock->previousBlock = this; } if (previousBlock != nullptr) { previousBlock->nextBlock = this; } + data().notify(*this); STORM_LOG_ASSERT(this->beginIndex < this->endIndex, "Unable to create block of illegal size."); } - bool Block::operator==(Block const& other) const { + template + bool Block::operator==(Block const& other) const { return this == &other; } - bool Block::operator!=(Block const& other) const { + template + bool Block::operator!=(Block const& other) const { return this != &other; } - void Block::print(Partition const& partition) const { + template + void Block::print(Partition const& partition) const { std::cout << "block [" << this << "] " << this->id << " from " << this->beginIndex << " to " << this->endIndex << std::endl; } - void Block::setBeginIndex(storm::storage::sparse::state_type beginIndex) { -// std::cout << "setting beg index to " << beginIndex << " [" << this << "]" << std::endl; + template + void Block::setBeginIndex(storm::storage::sparse::state_type beginIndex) { this->beginIndex = beginIndex; + data().notify(*this); STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size."); } - void Block::setEndIndex(storm::storage::sparse::state_type endIndex) { + template + void Block::setEndIndex(storm::storage::sparse::state_type endIndex) { this->endIndex = endIndex; + data().notify(*this); STORM_LOG_ASSERT(beginIndex < endIndex, "Unable to resize block to illegal size."); } - storm::storage::sparse::state_type Block::getBeginIndex() const { + template + storm::storage::sparse::state_type Block::getBeginIndex() const { return this->beginIndex; } - storm::storage::sparse::state_type Block::getEndIndex() const { + template + storm::storage::sparse::state_type Block::getEndIndex() const { return this->endIndex; } - Block const& Block::getNextBlock() const { + template + Block const& Block::getNextBlock() const { return *this->nextBlock; } - bool Block::hasNextBlock() const { + template + bool Block::hasNextBlock() const { return this->nextBlock != nullptr; } - Block* Block::getNextBlockPointer() { + template + Block* Block::getNextBlockPointer() { return this->nextBlock; } - Block const* Block::getNextBlockPointer() const { + template + Block const* Block::getNextBlockPointer() const { return this->nextBlock; } - Block const& Block::getPreviousBlock() const { + template + Block const& Block::getPreviousBlock() const { return *this->previousBlock; } - Block* Block::getPreviousBlockPointer() { + template + Block* Block::getPreviousBlockPointer() { return this->previousBlock; } - Block const* Block::getPreviousBlockPointer() const { + template + Block const* Block::getPreviousBlockPointer() const { return this->previousBlock; } - bool Block::hasPreviousBlock() const { + template + bool Block::hasPreviousBlock() const { return this->previousBlock != nullptr; } - bool Block::check() const { + template + bool Block::check() const { STORM_LOG_ASSERT(this->beginIndex < this->endIndex, "Block has negative size."); STORM_LOG_ASSERT(!this->hasPreviousBlock() || this->getPreviousBlock().getNextBlockPointer() == this, "Illegal previous block."); STORM_LOG_ASSERT(!this->hasNextBlock() || this->getNextBlock().getPreviousBlockPointer() == this, "Illegal next block."); return true; } - std::size_t Block::getNumberOfStates() const { + template + std::size_t Block::getNumberOfStates() const { return (this->endIndex - this->beginIndex); } - bool Block::isMarkedAsSplitter() const { + template + bool Block::isMarkedAsSplitter() const { return this->markedAsSplitter; } - void Block::markAsSplitter() { + template + void Block::markAsSplitter() { this->markedAsSplitter = true; } - void Block::unmarkAsSplitter() { + template + void Block::unmarkAsSplitter() { this->markedAsSplitter = false; } - std::size_t Block::getId() const { + template + std::size_t Block::getId() const { return this->id; } - void Block::setAbsorbing(bool absorbing) { + template + void Block::setAbsorbing(bool absorbing) { this->absorbing = absorbing; } - bool Block::isAbsorbing() const { + template + bool Block::isAbsorbing() const { return this->absorbing; } - void Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) { + template + void Block::setRepresentativeState(storm::storage::sparse::state_type representativeState) { this->representativeState = representativeState; } - bool Block::hasRepresentativeState() const { + template + bool Block::hasRepresentativeState() const { return static_cast(representativeState); } - storm::storage::sparse::state_type Block::getRepresentativeState() const { + template + storm::storage::sparse::state_type Block::getRepresentativeState() const { STORM_LOG_THROW(representativeState, storm::exceptions::InvalidOperationException, "Unable to retrieve representative state for block."); return representativeState.get(); } // Retrieves whether the block is marked as a predecessor. - bool Block::needsRefinement() const { + template + bool Block::needsRefinement() const { return needsRefinementFlag; } // Marks the block as needing refinement (or not). - void Block::setNeedsRefinement(bool value) { + template + void Block::setNeedsRefinement(bool value) { needsRefinementFlag = value; } + + template + DataType& Block::data() { + return mData; + } + + template + DataType const& Block::data() const { + return mData; + } + + template class Block; + } } } \ No newline at end of file diff --git a/src/storage/bisimulation/Block.h b/src/storage/bisimulation/Block.h index 304da118a..dd504ed08 100644 --- a/src/storage/bisimulation/Block.h +++ b/src/storage/bisimulation/Block.h @@ -10,11 +10,13 @@ namespace storm { namespace storage { namespace bisimulation { // Forward-declare partition class. + template class Partition; + template class Block { public: - friend class Partition; + friend class Partition; // 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); @@ -29,7 +31,7 @@ namespace storm { bool operator!=(Block const& other) const; // Prints the block to the standard output. - void print(Partition const& partition) const; + void print(Partition const& partition) const; // Returns the beginning index of the block. storm::storage::sparse::state_type getBeginIndex() const; @@ -100,6 +102,12 @@ namespace storm { // Retrieves the representative state for this block. storm::storage::sparse::state_type getRepresentativeState() const; + // Retrieves the additional data associated with this block. + DataType& data(); + + // Retrieves the additional data associated with this block. + DataType const& data() const; + private: // Sets the beginning index of the block. void setBeginIndex(storm::storage::sparse::state_type beginIndex); @@ -130,6 +138,9 @@ namespace storm { // An optional representative state for the block. If this is set, this state is used to derive the // atomic propositions of the meta state in the quotient model. boost::optional representativeState; + + // A member that stores additional data that depends on the kind of bisimulation. + DataType mData; }; } } diff --git a/src/storage/bisimulation/DeterministicBlockData.cpp b/src/storage/bisimulation/DeterministicBlockData.cpp new file mode 100644 index 000000000..e85acf729 --- /dev/null +++ b/src/storage/bisimulation/DeterministicBlockData.cpp @@ -0,0 +1,44 @@ +#include "src/storage/bisimulation/DeterministicBlockData.h" + +namespace storm { + namespace storage { + namespace bisimulation { + + DeterministicBlockData::DeterministicBlockData() : newBeginIndex(0), newEndIndex(0) { + // Intentionally left empty. + } + + DeterministicBlockData::DeterministicBlockData(uint_fast64_t newBeginIndex, uint_fast64_t newEndIndex) : newBeginIndex(newBeginIndex), newEndIndex(newEndIndex) { + // Intentionally left empty. + } + + uint_fast64_t DeterministicBlockData::getNewBeginIndex() const { + return newBeginIndex; + } + + void DeterministicBlockData::increaseNewBeginIndex() { + ++newBeginIndex; + } + + uint_fast64_t DeterministicBlockData::getNewEndIndex() const { + return newEndIndex; + } + + void DeterministicBlockData::decreaseNewEndIndex() { + --newEndIndex; + } + + void DeterministicBlockData::increaseNewEndIndex() { + ++newEndIndex; + } + + bool DeterministicBlockData::notify(Block const& block) { + bool result = block.getBeginIndex() != this->newBeginIndex || block.getEndIndex() != this->newEndIndex; + this->newBeginIndex = block.getBeginIndex(); + this->newEndIndex = block.getEndIndex(); + return result; + } + + } + } +} diff --git a/src/storage/bisimulation/DeterministicBlockData.h b/src/storage/bisimulation/DeterministicBlockData.h new file mode 100644 index 000000000..4c02bf0ce --- /dev/null +++ b/src/storage/bisimulation/DeterministicBlockData.h @@ -0,0 +1,64 @@ +#ifndef STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_ +#define STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_ + +#include + +#include "src/storage/bisimulation/Block.h" + +namespace storm { + namespace storage { + namespace bisimulation { + class DeterministicBlockData { + public: + DeterministicBlockData(); + DeterministicBlockData(uint_fast64_t newBeginIndex, uint_fast64_t newEndIndex); + + /*! + * Retrieves the new begin index. + * + * @return The new begin index. + */ + uint_fast64_t getNewBeginIndex() const; + + /*! + * Increases the new begin index by one. + */ + void increaseNewBeginIndex(); + + /*! + * Retrieves the new end index. + * + * @return The new end index. + */ + uint_fast64_t getNewEndIndex() const; + + /*! + * Decreases the new end index. + */ + void decreaseNewEndIndex(); + + /*! + * Increases the new end index. + */ + void increaseNewEndIndex(); + + /*! + * This method needs to be called whenever the block was modified to notify the data of the change. + * + * @param block The block that this data belongs to. + * @return True iff the data changed as a consequence of notifying it. + */ + bool notify(Block const& block); + + public: + // A marker that can be used to mark a the new beginning of the block. + uint_fast64_t newBeginIndex; + + // A marker that can be used to mark a the new end of the block. + uint_fast64_t newEndIndex; + }; + } + } +} + +#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICBLOCKDATA_H_ */ diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 565dfef91..3710755a0 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -28,7 +28,7 @@ namespace storm { using namespace bisimulation; template - DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options) : BisimulationDecomposition(model, options), probabilitiesToCurrentSplitter(model.getNumberOfStates(), storm::utility::zero()), predecessorsOfCurrentSplitter(model.getNumberOfStates()) { + DeterministicModelBisimulationDecomposition::DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options) : BisimulationDecomposition(model, options), probabilitiesToCurrentSplitter(model.getNumberOfStates(), storm::utility::zero()) { STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.hasUniqueRewardModel(), storm::exceptions::IllegalFunctionCallException, "Bisimulation currently only supports models with at most one reward model."); STORM_LOG_THROW(!options.keepRewards || !model.hasRewardModel() || model.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::IllegalFunctionCallException, "Bisimulation is currently supported for models with state rewards only. Consider converting the transition rewards to state rewards (via suitable function calls)."); STORM_LOG_THROW(options.type != BisimulationType::Weak || !options.bounded, storm::exceptions::IllegalFunctionCallException, "Weak bisimulation cannot preserve bounded properties."); @@ -102,7 +102,7 @@ namespace storm { void DeterministicModelBisimulationDecomposition::initializeSilentProbabilities() { silentProbabilities.resize(this->model.getNumberOfStates(), storm::utility::zero()); for (storm::storage::sparse::state_type state = 0; state < this->model.getNumberOfStates(); ++state) { - Block const* currentBlockPtr = &this->partition.getBlock(state); + Block const* currentBlockPtr = &this->partition.getBlock(state); for (auto const& successorEntry : this->model.getRows(state)) { if (&this->partition.getBlock(successorEntry.getColumn()) == currentBlockPtr) { silentProbabilities[state] += successorEntry.getValue(); @@ -121,7 +121,7 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::initializeMeasureDrivenPartition() { - BisimulationDecomposition::initializeMeasureDrivenPartition(); + BisimulationDecomposition::initializeMeasureDrivenPartition(); if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { this->initializeWeakDtmcBisimulation(); @@ -130,7 +130,7 @@ namespace storm { template void DeterministicModelBisimulationDecomposition::initializeLabelBasedPartition() { - BisimulationDecomposition::initializeLabelBasedPartition(); + BisimulationDecomposition::initializeLabelBasedPartition(); if (this->options.type == BisimulationType::Weak && this->model.getType() == storm::models::ModelType::Dtmc) { this->initializeWeakDtmcBisimulation(); @@ -153,29 +153,20 @@ namespace storm { } template - bool DeterministicModelBisimulationDecomposition::isPredecessorOfCurrentSplitter(storm::storage::sparse::state_type const& state) const { - return this->predecessorsOfCurrentSplitter.get(state); - } - - template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitter(std::list& predecessorBlocks, std::deque& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitter(std::list*>& predecessorBlocks, std::deque*>& splitterQueue) { for (auto block : predecessorBlocks) { -// std::cout << "splitting predecessor block " << block->getId() << " of splitter" << std::endl; - this->partition.splitBlock(*block, [this] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { - bool firstIsPredecessor = isPredecessorOfCurrentSplitter(state1); - bool secondIsPredecessor = isPredecessorOfCurrentSplitter(state2); - if (firstIsPredecessor && !secondIsPredecessor) { - return true; - } else if (firstIsPredecessor && secondIsPredecessor) { - return getProbabilityToSplitter(state1) < getProbabilityToSplitter(state2); - } else { - return false; + // Depending on the actions we need to take, the block to refine changes, so we need to keep track of it. + Block* blockToRefineProbabilistically = block; + + if (block->data().getNewBeginIndex() != block->getBeginIndex()) { + // If the new begin index has shifted to a non-trivial position, we need to split the block. + if (block->data().getNewBeginIndex() != block->getEndIndex()) { + auto result = this->partition.splitBlock(*block, block->data().getNewBeginIndex()); + if (result.second) { + blockToRefineProbabilistically = block->getPreviousBlockPointer(); + } } - }, [&splitterQueue] (Block& block) { - splitterQueue.emplace_back(&block); - }); -// this->partition.print(); -// std::cout << "size: " << this->partition.size() << std::endl; + } // Remember that we have refined the block. block->setNeedsRefinement(false); @@ -184,7 +175,91 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block const& splitter, std::deque& splitterQueue) { + bool DeterministicModelBisimulationDecomposition::possiblyNeedsRefinement(bisimulation::Block const& predecessorBlock) const { + return predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing(); + } + + template + void DeterministicModelBisimulationDecomposition::increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block const& predecessorBlock, ValueType const& value) { + storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor); + + // If the position of the state is between the new begin and end index, we have not yet seen this predecessor. + if (predecessorPosition >= predecessorBlock.data().getNewBeginIndex() && predecessorPosition < predecessorBlock.data().getNewEndIndex()) { + // Then, we just set the value. + probabilitiesToCurrentSplitter[predecessor] = value; + } else { + // If the state was seen as a predecessor before, we add the value to the existing value. + probabilitiesToCurrentSplitter[predecessor] += value; + } + } + + template + void DeterministicModelBisimulationDecomposition::moveStateToNewBeginningOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock) { + this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().getNewBeginIndex())); + predecessorBlock.data().increaseNewBeginIndex(); + } + + template + void DeterministicModelBisimulationDecomposition::moveStateToNewEndOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock) { + this->partition.swapStates(predecessor, this->partition.getState(predecessorBlock.data().getNewEndIndex() - 1)); + predecessorBlock.data().decreaseNewEndIndex(); + } + + template + void DeterministicModelBisimulationDecomposition::moveStateInSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock, storm::storage::sparse::state_type currentPositionInSplitter) { + storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor); + + // If the predecessor is one of the states for which we have already explored its predecessors, we can move + // it to the new beginning of the block like for any other block. + if (predecessorPosition <= currentPositionInSplitter) { + moveStateToNewBeginningOfBlock(predecessor, predecessorBlock); + } else { + // Otherwise, we move it to the new end of the block in which we assemble all states that are predecessors + // of the splitter, but for which the predecessors still need to be explored. + moveStateToNewEndOfBlock(predecessor, predecessorBlock); + } + } + + template + void DeterministicModelBisimulationDecomposition::explorePredecessorsOfNewEndOfSplitter(bisimulation::Block& splitter) { + for (auto splitterIt = this->partition.begin() + splitter.data().getNewEndIndex(), splitterIte = this->partition.end(splitter); splitterIt != splitterIte; ++splitterIt) { + storm::storage::sparse::state_type currentState = *splitterIt; + + for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) { + storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); + Block& predecessorBlock = this->partition.getBlock(predecessor); + + // If the block does not need to be refined, we skip it. + if (!possiblyNeedsRefinement(predecessorBlock)) { + continue; + } + + // We keep track of the probability of the predecessor moving to the splitter. + increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue()); + + if (predecessorBlock != splitter) { + moveStateToNewBeginningOfBlock(predecessor, predecessorBlock); + } else { + storm::storage::sparse::state_type predecessorPosition = this->partition.getPosition(predecessor); + + // In this case, we must only move the predecessor its predecessors were already explored. + // If we have not yet explored its predecessors, it has to be to the right of the currently + // considered state and will be transferred to the beginning of the block anyway. + if (predecessorPosition < splitter.data().getNewEndIndex()) { + moveStateToNewBeginningOfBlock(predecessor, predecessorBlock); + } + } + } + + // Now that we have explored its predecessors and know that the current state is itself a predecessor of + // the splitter, we can safely move it to the beginning of the block. + moveStateToNewBeginningOfBlock(currentState, splitter); + splitter.data().increaseNewEndIndex(); + } + } + + template + void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { // The outline of the refinement is as follows. // // (0) we prepare the environment for the splitting process. @@ -194,32 +269,34 @@ namespace storm { // all predecessors of the splitter in a member bit vector. // (0) - predecessorsOfCurrentSplitter.clear(); - std::list predecessorBlocks; + std::list*> predecessorBlocks; // (1) - for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.end(splitter); splitterIt != splitterIte; ++splitterIt) { + storm::storage::sparse::state_type currentPosition = splitter.getBeginIndex(); + bool splitterIsItsOwnPredecessor = false; + for (auto splitterIt = this->partition.begin(splitter), splitterIte = this->partition.end(splitter); splitterIt != splitterIte && currentPosition < splitter.data().getNewEndIndex(); ++splitterIt, ++currentPosition) { storm::storage::sparse::state_type currentState = *splitterIt; for (auto const& predecessorEntry : this->backwardTransitions.getRow(currentState)) { storm::storage::sparse::state_type predecessor = predecessorEntry.getColumn(); - Block& predecessorBlock = this->partition.getBlock(predecessor); + Block& predecessorBlock = this->partition.getBlock(predecessor); - // If the predecessor block has just one state or is marked as being absorbing, we must not split it. - if (predecessorBlock.getNumberOfStates() <= 1 || predecessorBlock.isAbsorbing()) { + // If the block does not need to be refined, we skip it. + if (!possiblyNeedsRefinement(predecessorBlock)) { continue; } + + // We keep track of the probability of the predecessor moving to the splitter. + increaseProbabilityToSplitter(predecessor, predecessorBlock, predecessorEntry.getValue()); - // If we have not seen this predecessor before, we reset its value and mark it as a predecessor of - // the splitter. - if (!predecessorsOfCurrentSplitter.get(predecessor)) { - predecessorsOfCurrentSplitter.set(predecessor); - probabilitiesToCurrentSplitter[predecessor] = predecessorEntry.getValue(); + if (predecessorBlock != splitter) { + moveStateToNewBeginningOfBlock(predecessor, predecessorBlock); } else { - // Otherwise, we increase the probability by the current transition. - probabilitiesToCurrentSplitter[predecessor] += predecessorEntry.getValue(); + splitterIsItsOwnPredecessor = true; + moveStateInSplitter(predecessor, predecessorBlock, currentPosition); } + // Insert the block into the list of blocks to refine (if that has not already happened). if (!predecessorBlock.needsRefinement()) { predecessorBlocks.emplace_back(&predecessorBlock); predecessorBlock.setNeedsRefinement(); @@ -227,6 +304,11 @@ namespace storm { } } + // If the splitter is its own predecessor block, we need to treat the states at the end of the block. + if (splitterIsItsOwnPredecessor) { + explorePredecessorsOfNewEndOfSplitter(splitter); + } + // std::cout << "probs of splitter predecessors: " << std::endl; // for (auto state : predecessorsOfCurrentSplitter) { // std::cout << state << " [" << this->partition.getBlock(state).getId() << "]" << " -> " << probabilitiesToCurrentSplitter[state] << std::endl; @@ -283,7 +365,7 @@ namespace storm { } } - Block const& oldBlock = this->partition.getBlock(representativeState); + Block const& oldBlock = this->partition.getBlock(representativeState); // If the block is absorbing, we simply add a self-loop. if (oldBlock.isAbsorbing()) { @@ -348,7 +430,7 @@ namespace storm { // Now check which of the blocks of the partition contain at least one initial state. for (auto initialState : this->model.getInitialStates()) { - Block const& initialBlock = this->partition.getBlock(initialState); + Block const& initialBlock = this->partition.getBlock(initialState); newLabeling.addLabelToState("init", initialBlock.getId()); } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index 27b12949d..74cedebb1 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ #include "src/storage/bisimulation/BisimulationDecomposition.h" +#include "src/storage/bisimulation/DeterministicBlockData.h" namespace storm { namespace utility { @@ -14,8 +15,9 @@ namespace storm { * This class represents the decomposition of a deterministic model into its bisimulation quotient. */ template - class DeterministicModelBisimulationDecomposition : public BisimulationDecomposition { + class DeterministicModelBisimulationDecomposition : public BisimulationDecomposition { public: + typedef bisimulation::DeterministicBlockData BlockDataType; typedef typename ModelType::ValueType ValueType; typedef typename ModelType::RewardModelType RewardModelType; @@ -26,7 +28,7 @@ namespace storm { * @param model The model to decompose. * @param options The options that customize the computed bisimulation. */ - DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options = typename BisimulationDecomposition::Options()); + DeterministicModelBisimulationDecomposition(ModelType const& model, typename BisimulationDecomposition::Options const& options = typename BisimulationDecomposition::Options()); protected: virtual std::pair getStatesWithProbability01() override; @@ -37,10 +39,10 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block const& splitter, std::deque& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; private: - virtual void refinePredecessorBlocksOfSplitter(std::list& predecessorBlocks, std::deque& splitterQueue); + virtual void refinePredecessorBlocksOfSplitter(std::list*>& predecessorBlocks, std::deque*>& splitterQueue); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -67,16 +69,29 @@ namespace storm { // Retrieves whether the given state is silent. bool isSilent(storm::storage::sparse::state_type const& state) const; - // Retrieves whether the given state is a predecessor of the current splitter. - bool isPredecessorOfCurrentSplitter(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; + + // Moves the given state to the new begin index of the given block and increases the new begin. + void moveStateToNewBeginningOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock); + + // Moves the given state to the new end index of the given block and decreases the new end. + void moveStateToNewEndOfBlock(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock); + + // Moves the given state to the new begin or new end of the block, depending on where the predecessor is located. + void moveStateInSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block& predecessorBlock, storm::storage::sparse::state_type currentPositionInSplitter); + + // Increases the probability of moving to the current splitter for the given state. + void increaseProbabilityToSplitter(storm::storage::sparse::state_type predecessor, bisimulation::Block const& predecessorBlock, ValueType const& value); + + // Explores the predecessors of the states that were identified as predecessors themselves that have not yet + // been explored. + void explorePredecessorsOfNewEndOfSplitter(bisimulation::Block& splitter); // 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; - // A bit vector storing the predecessors of the current splitter. - storm::storage::BitVector predecessorsOfCurrentSplitter; - // A vector mapping each state to its silent probability. std::vector silentProbabilities; }; diff --git a/src/storage/bisimulation/Partition.cpp b/src/storage/bisimulation/Partition.cpp index bbe45fc0a..9597935dc 100644 --- a/src/storage/bisimulation/Partition.cpp +++ b/src/storage/bisimulation/Partition.cpp @@ -2,14 +2,17 @@ #include +#include "src/storage/bisimulation/DeterministicBlockData.h" + #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace storage { namespace bisimulation { - Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) { - blocks.emplace_back(new Block(0, numberOfStates, nullptr, nullptr, blocks.size())); + template + Partition::Partition(std::size_t numberOfStates) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) { + blocks.emplace_back(new Block(0, numberOfStates, nullptr, nullptr, blocks.size())); // Set up the different parts of the internal structure. for (storm::storage::sparse::state_type state = 0; state < numberOfStates; ++state) { @@ -19,13 +22,14 @@ namespace storm { } } - Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) { + template + Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, boost::optional representativeProb1State) : stateToBlockMapping(numberOfStates), states(numberOfStates), positions(numberOfStates) { storm::storage::sparse::state_type position = 0; - Block* firstBlock = nullptr; - Block* secondBlock = nullptr; - Block* thirdBlock = nullptr; + Block* firstBlock = nullptr; + Block* secondBlock = nullptr; + Block* thirdBlock = nullptr; if (!prob0States.empty()) { - blocks.emplace_back(new Block(0, prob0States.getNumberOfSetBits(), nullptr, nullptr, blocks.size())); + blocks.emplace_back(new Block(0, prob0States.getNumberOfSetBits(), nullptr, nullptr, blocks.size())); firstBlock = blocks.front().get(); for (auto state : prob0States) { @@ -39,7 +43,7 @@ namespace storm { } if (!prob1States.empty()) { - blocks.emplace_back(new Block(position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, blocks.size())); + blocks.emplace_back(new Block(position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, blocks.size())); secondBlock = blocks[1].get(); for (auto state : prob1States) { @@ -55,7 +59,7 @@ namespace storm { storm::storage::BitVector otherStates = ~(prob0States | prob1States); if (!otherStates.empty()) { - blocks.emplace_back(new Block(position, numberOfStates, secondBlock, nullptr, blocks.size())); + blocks.emplace_back(new Block(position, numberOfStates, secondBlock, nullptr, blocks.size())); thirdBlock = blocks[2].get(); for (auto state : otherStates) { @@ -68,12 +72,14 @@ namespace storm { } } - void Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { + template + void Partition::swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { std::swap(this->states[this->positions[state1]], this->states[this->positions[state2]]); std::swap(this->positions[state1], this->positions[state2]); } - void Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { + template + void Partition::swapStatesAtPositions(storm::storage::sparse::state_type position1, storm::storage::sparse::state_type position2) { storm::storage::sparse::state_type state1 = this->states[position1]; storm::storage::sparse::state_type state2 = this->states[position2]; @@ -82,64 +88,96 @@ namespace storm { this->positions[state2] = position1; } - storm::storage::sparse::state_type const& Partition::getPosition(storm::storage::sparse::state_type state) const { + template + storm::storage::sparse::state_type const& Partition::getPosition(storm::storage::sparse::state_type state) const { return this->positions[state]; } - void Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { + template + void Partition::setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position) { this->positions[state] = position; } - storm::storage::sparse::state_type const& Partition::getState(storm::storage::sparse::state_type position) const { + template + storm::storage::sparse::state_type const& Partition::getState(storm::storage::sparse::state_type position) const { return this->states[position]; } - void Partition::mapStatesToBlock(Block& block, std::vector::iterator first, std::vector::iterator last) { + template + void Partition::mapStatesToBlock(Block& block, std::vector::iterator first, std::vector::iterator last) { for (; first != last; ++first) { this->stateToBlockMapping[*first] = █ } } - void Partition::mapStatesToPositions(Block const& block) { + 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; } } - Block& Partition::getBlock(storm::storage::sparse::state_type state) { + template + Block& Partition::getBlock(storm::storage::sparse::state_type state) { return *this->stateToBlockMapping[state]; } - Block const& Partition::getBlock(storm::storage::sparse::state_type state) const { + template + Block const& Partition::getBlock(storm::storage::sparse::state_type state) const { return *this->stateToBlockMapping[state]; } - std::vector::iterator Partition::begin(Block const& block) { + template + std::vector::iterator Partition::begin(Block const& block) { auto it = this->states.begin(); std::advance(it, block.getBeginIndex()); return it; } - std::vector::const_iterator Partition::begin(Block const& block) const { + template + std::vector::const_iterator Partition::begin(Block const& block) const { auto it = this->states.begin(); std::advance(it, block.getBeginIndex()); return it; } - std::vector::iterator Partition::end(Block const& block) { + template + std::vector::iterator Partition::end(Block const& block) { auto it = this->states.begin(); std::advance(it, block.getEndIndex()); return it; } - std::vector::const_iterator Partition::end(Block const& block) const { + template + std::vector::const_iterator Partition::end(Block const& block) const { auto it = this->states.begin(); std::advance(it, block.getEndIndex()); return it; } - std::pair>::iterator, bool> Partition::splitBlock(Block& block, storm::storage::sparse::state_type position) { + template + std::vector::iterator Partition::begin() { + return this->states.begin(); + } + + template + std::vector::const_iterator Partition::begin() const { + return this->states.begin(); + } + + template + std::vector::iterator Partition::end() { + return this->states.end(); + } + + template + std::vector::const_iterator Partition::end() const { + return this->states.end(); + } + + 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.getId() << " at pos " << position << " (was " << block.getBeginIndex() << " to " << block.getEndIndex() << ")" << std::endl; @@ -153,7 +191,7 @@ namespace storm { } // Actually create the new block. - blocks.emplace_back(new Block(block.getBeginIndex(), position, block.getPreviousBlockPointer(), &block, blocks.size())); + blocks.emplace_back(new Block(block.getBeginIndex(), position, block.getPreviousBlockPointer(), &block, blocks.size())); auto newBlockIt = std::prev(blocks.end()); // Resize the current block appropriately. @@ -170,7 +208,8 @@ namespace storm { return std::make_pair(newBlockIt, true); } - bool Partition::splitBlock(Block& block, std::function const& less, std::function const& newBlockCallback) { + template + bool Partition::splitBlock(Block& block, std::function const& less, std::function&)> const& newBlockCallback) { // std::cout << "sorting the block [" << block.getId() << "]" << std::endl; // 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); @@ -213,7 +252,15 @@ namespace storm { return wasSplit; } - bool Partition::split(std::function const& less, std::function const& newBlockCallback) { + // Splits the block by sorting the states according to the given function and then identifying the split + // points. + template + bool Partition::splitBlock(Block& block, std::function const& less) { + return this->splitBlock(block, less, [] (Block& block) {}); + } + + template + bool Partition::split(std::function const& less, std::function&)> const& newBlockCallback) { bool result = false; // Since the underlying storage of the blocks may change during iteration, we remember the current size // and iterate over indices. This assumes that new blocks will be added at the end of the blocks vector. @@ -224,26 +271,35 @@ namespace storm { return result; } - void Partition::splitStates(Block& block, storm::storage::BitVector const& states) { + template + bool Partition::split(std::function const& less) { + return this->split(less, [] (Block& block) {}); + } + + template + void Partition::splitStates(Block& block, storm::storage::BitVector const& states) { this->splitBlock(block, [&states] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return states.get(a) && !states.get(b); }); } - void Partition::splitStates(storm::storage::BitVector const& states) { + template + void Partition::splitStates(storm::storage::BitVector const& states) { this->split([&states] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return states.get(a) && !states.get(b); }); } - void Partition::sortBlock(Block const& block) { + template + void Partition::sortBlock(Block const& block) { std::sort(this->begin(block), this->end(block), [] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return a < b; }); mapStatesToPositions(block); } - Block& Partition::insertBlock(Block& block) { + template + Block& Partition::insertBlock(Block& block) { // Find the beginning of the new block. storm::storage::sparse::state_type begin = block.hasPreviousBlock() ? block.getPreviousBlock().getEndIndex() : 0; // Actually insert the new block. - blocks.emplace_back(new Block(begin, block.getBeginIndex(), block.getPreviousBlockPointer(), &block, blocks.size())); - Block& newBlock = *blocks.back(); + blocks.emplace_back(new Block(begin, block.getBeginIndex(), block.getPreviousBlockPointer(), &block, blocks.size())); + Block& newBlock = *blocks.back(); // Update the mapping of the states in the newly created block. for (auto it = this->begin(newBlock), ite = this->end(newBlock); it != ite; ++it) { @@ -253,15 +309,18 @@ namespace storm { return newBlock; } - std::vector> const& Partition::getBlocks() const { + template + std::vector>> const& Partition::getBlocks() const { return this->blocks; } - std::vector>& Partition::getBlocks() { + template + std::vector>>& Partition::getBlocks() { return this->blocks; } - bool Partition::check() const { + template + bool Partition::check() const { for (uint_fast64_t state = 0; state < this->positions.size(); ++state) { STORM_LOG_ASSERT(this->states[this->positions[state]] == state, "Position mapping corrupted."); } @@ -274,7 +333,8 @@ namespace storm { return true; } - void Partition::print() const { + template + void Partition::print() const { for (auto const& block : this->blocks) { block->print(*this); } @@ -295,10 +355,13 @@ namespace storm { STORM_LOG_ASSERT(this->check(), "Partition corrupted."); } - std::size_t Partition::size() const { + template + std::size_t Partition::size() const { return blocks.size(); } + template class Partition; + } } } \ No newline at end of file diff --git a/src/storage/bisimulation/Partition.h b/src/storage/bisimulation/Partition.h index 0fdffa4f6..056377ad9 100644 --- a/src/storage/bisimulation/Partition.h +++ b/src/storage/bisimulation/Partition.h @@ -12,6 +12,7 @@ namespace storm { namespace storage { namespace bisimulation { + template class Partition { public: /*! @@ -49,20 +50,27 @@ namespace storm { // Splits the block at the given position and inserts a new block after the current one holding the rest // of the states. - std::pair>::iterator, bool> splitBlock(Block& block, storm::storage::sparse::state_type position); + std::pair>>::iterator, bool> splitBlock(Block& block, storm::storage::sparse::state_type position); // 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 = [] (Block&) {}); + bool splitBlock(Block& block, std::function const& less, std::function&)> const& newBlockCallback); + // Splits the block by sorting the states according to the given function and then identifying the split + // points. + bool splitBlock(Block& block, std::function const& less); + // Splits all blocks by using the sorting-based splitting. The callback is called for all newly created // blocks. - bool split(std::function const& less, std::function const& newBlockCallback = [] (Block&) {}); + bool split(std::function const& less, std::function&)> const& newBlockCallback); + + // Splits all blocks by using the sorting-based splitting. + bool split(std::function const& less); // Splits the block such that the resulting blocks contain only states in the given set or none at all. // If the block is split, the given block will contain the states *not* in the given set and the newly // created block will contain the states *in* the given set. - void splitStates(Block& block, storm::storage::BitVector const& states); + void splitStates(Block& block, storm::storage::BitVector const& states); /*! * Splits all blocks of the partition such that afterwards all blocks contain only states within the given @@ -71,37 +79,49 @@ namespace storm { void splitStates(storm::storage::BitVector const& states); // Sorts the block based on the state indices. - void sortBlock(Block const& block); + void sortBlock(Block const& block); // Retrieves the blocks of the partition. - std::vector> const& getBlocks() const; + std::vector>> const& getBlocks() const; // Retrieves the blocks of the partition. - std::vector>& getBlocks(); + std::vector>>& getBlocks(); // Checks the partition for internal consistency. bool check() const; // Returns an iterator to the beginning of the states of the given block. - std::vector::iterator begin(Block const& block); + std::vector::iterator begin(Block const& block); // Returns an iterator to the beginning of the states of the given block. - std::vector::const_iterator begin(Block const& block) const; + std::vector::const_iterator begin(Block const& block) const; // Returns an iterator to the beginning of the states of the given block. - std::vector::iterator end(Block const& block); + std::vector::iterator end(Block const& block); // Returns an iterator to the beginning of the states of the given block. - std::vector::const_iterator end(Block const& block) const; + std::vector::const_iterator end(Block const& block) const; + + // Returns an iterator to the beginning of the states in the partition. + std::vector::iterator begin(); + + // Returns an iterator to the beginning of the states in the partition. + std::vector::const_iterator begin() const; + + // Returns an iterator to the end of the states in the partition. + std::vector::iterator end(); + + // Returns an iterator to the end of the states in the partition. + std::vector::const_iterator end() const; // Swaps the positions of the two given states. void swapStates(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2); // Retrieves the block of the given state. - Block& getBlock(storm::storage::sparse::state_type state); + Block& getBlock(storm::storage::sparse::state_type state); // Retrieves the block of the given state. - Block const& getBlock(storm::storage::sparse::state_type state) const; + Block const& getBlock(storm::storage::sparse::state_type state) const; // Retrieves the position of the given state. storm::storage::sparse::state_type const& getPosition(storm::storage::sparse::state_type state) const; @@ -110,10 +130,10 @@ namespace storm { storm::storage::sparse::state_type const& getState(storm::storage::sparse::state_type position) const; // Updates the block mapping for the given range of states to the specified block. - void mapStatesToBlock(Block& block, std::vector::iterator first, std::vector::iterator last); + void mapStatesToBlock(Block& block, std::vector::iterator first, std::vector::iterator last); // Update the state to position for the states in the given block. - void mapStatesToPositions(Block const& block); + void mapStatesToPositions(Block const& block); private: // FIXME: necessary? @@ -123,17 +143,17 @@ namespace storm { // FIXME: necessary? // Inserts a block before the given block. The new block will cover all states between the beginning // of the given block and the end of the previous block. - Block& insertBlock(Block& block); + Block& insertBlock(Block& block); // FIXME: necessary? // Sets the position of the given state. void setPosition(storm::storage::sparse::state_type state, storm::storage::sparse::state_type position); // The of blocks in the partition. - std::vector> blocks; + std::vector>> blocks; // A mapping of states to their blocks. - std::vector stateToBlockMapping; + std::vector*> stateToBlockMapping; // A vector containing all the states. It is ordered in a way such that the blocks only need to define // their start/end indices.