From a333d29d1663a877fd0980d5ecc562213463a9b9 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sat, 22 Oct 2016 17:31:02 +0200 Subject: [PATCH] Hard coded heuristic to gain performance Former-commit-id: d0d869bb3e08535bdfa5c56ec2e1e4eb42395e81 --- src/builder/DftExplorationHeuristic.cpp | 84 +++++++++++-------- src/builder/DftExplorationHeuristic.h | 71 ++++++++++++---- src/builder/ExplicitDFTModelBuilderApprox.cpp | 71 ++++++++-------- src/builder/ExplicitDFTModelBuilderApprox.h | 15 ++-- src/storage/dft/DFTState.cpp | 8 +- src/storage/dft/DFTState.h | 23 +---- 6 files changed, 150 insertions(+), 122 deletions(-) diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index e14c34dee..4bc72ccc1 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -3,7 +3,6 @@ #include "src/utility/macros.h" #include "src/utility/constants.h" #include "src/exceptions/NotImplementedException.h" -#include "src/storage/dft/DFTState.h" #include @@ -11,74 +10,87 @@ namespace storm { namespace builder { template - DFTExplorationHeuristic::DFTExplorationHeuristic() : skip(true), depth(std::numeric_limits::max()), rate(storm::utility::zero()), exitRate(storm::utility::zero()) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(std::numeric_limits::max()), rate(storm::utility::zero()), exitRate(storm::utility::zero()) { // Intentionally left empty } template - void DFTExplorationHeuristic::setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) { + void DFTExplorationHeuristic::updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) { this->depth = std::min(this->depth, depth); this->rate = std::max(this->rate, rate); this->exitRate = std::max(this->exitRate, exitRate); } template - bool DFTExplorationHeuristic::isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const { - if (!skip) { - return false; - } - switch (heuristic) { - case ApproximationHeuristic::NONE: - return false; - case ApproximationHeuristic::DEPTH: - return depth > approximationThreshold; - case ApproximationHeuristic::RATERATIO: - return getRateRatio() < approximationThreshold; - default: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic not known."); - } + DFTExplorationHeuristicNone::DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + template + bool DFTExplorationHeuristicNone::isSkip(double approximationThreshold) const { + return false; + } + + template + bool DFTExplorationHeuristicNone::operator<(DFTExplorationHeuristicNone const& other) const { + // Just use memory address for comparing + // TODO Matthias: better idea? + return this > &other; + } + + template + DFTExplorationHeuristicDepth::DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + template + bool DFTExplorationHeuristicDepth::isSkip(double approximationThreshold) const { + return !this->expand && this->depth > approximationThreshold; + } + + template + bool DFTExplorationHeuristicDepth::operator<(DFTExplorationHeuristicDepth const& other) const { + return this->depth > other.depth; } template - void DFTExplorationHeuristic::setNotSkip() { - skip = false; + DFTExplorationHeuristicRateRatio::DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty } template - size_t DFTExplorationHeuristic::getDepth() const { - return depth; + bool DFTExplorationHeuristicRateRatio::isSkip(double approximationThreshold) const { + return !this->expand && this->getRateRatio() < approximationThreshold; } template - bool DFTExplorationHeuristic::compare(DFTExplorationHeuristic other, ApproximationHeuristic heuristic) { - switch (heuristic) { - case ApproximationHeuristic::NONE: - // Just use memory address for comparing - // TODO Matthias: better idea? - return this > &other; - case ApproximationHeuristic::DEPTH: - return this->depth > other.depth; - case ApproximationHeuristic::RATERATIO: - return this->getRateRatio() < other.getRateRatio(); - default: - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic not known."); - } + bool DFTExplorationHeuristicRateRatio::operator<(DFTExplorationHeuristicRateRatio const& other) const { + return this->getRateRatio() < other.getRateRatio(); } + template<> - double DFTExplorationHeuristic::getRateRatio() const { + double DFTExplorationHeuristicRateRatio::getRateRatio() const { return rate/exitRate; } template<> - double DFTExplorationHeuristic::getRateRatio() const { + double DFTExplorationHeuristicRateRatio::getRateRatio() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work."); } + + // Instantiate templates. template class DFTExplorationHeuristic; + template class DFTExplorationHeuristicNone; + template class DFTExplorationHeuristicDepth; + template class DFTExplorationHeuristicRateRatio; #ifdef STORM_HAVE_CARL template class DFTExplorationHeuristic; + template class DFTExplorationHeuristicNone; + template class DFTExplorationHeuristicDepth; + template class DFTExplorationHeuristicRateRatio; #endif } } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 3fd3d72a8..8f12d2ec1 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -2,16 +2,9 @@ #define STORM_BUILDER_DFTEXPLORATIONHEURISTIC_H_ #include -#include namespace storm { - // Forward declaration - namespace storage { - template - class DFTState; - } - namespace builder { /*! @@ -19,32 +12,74 @@ namespace storm { */ enum class ApproximationHeuristic { NONE, DEPTH, RATERATIO }; + + /*! + * General super class for appoximation heuristics. + */ template class DFTExplorationHeuristic { public: - DFTExplorationHeuristic(); - - void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate); - - bool isSkip(double approximationThreshold, ApproximationHeuristic heuristic) const; + DFTExplorationHeuristic(size_t id); - void setNotSkip(); + void updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate); - size_t getDepth() const; + virtual bool isSkip(double approximationThreshold) const = 0; - bool compare(DFTExplorationHeuristic other, ApproximationHeuristic heuristic); + void markExpand() { + expand = true; + } - private: + size_t getId() const { + return id; + } - double getRateRatio() const; + size_t getDepth() const { + return depth; + } - bool skip; + protected: + size_t id; + bool expand; size_t depth; ValueType rate; ValueType exitRate; }; + + template + class DFTExplorationHeuristicNone : public DFTExplorationHeuristic { + public: + DFTExplorationHeuristicNone(size_t id); + + bool isSkip(double approximationThreshold) const override; + + bool operator<(DFTExplorationHeuristicNone const& other) const; + }; + + template + class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic { + public: + DFTExplorationHeuristicDepth(size_t id); + + bool isSkip(double approximationThreshold) const override; + + bool operator<(DFTExplorationHeuristicDepth const& other) const; + }; + + template + class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic { + public: + DFTExplorationHeuristicRateRatio(size_t id); + + bool isSkip(double approximationThreshold) const override; + + bool operator<(DFTExplorationHeuristicRateRatio const& other) const; + + private: + double getRateRatio() const; + }; + } } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 268ec03dc..5595a5f49 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -31,8 +31,8 @@ namespace storm { generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), - explorationQueue([this](StateType idA, StateType idB) { - return isPriorityGreater(idA, idB); + explorationQueue([this](ExplorationHeuristicPointer a, ExplorationHeuristicPointer b) { + return *a < *b; }) { // Intentionally left empty. @@ -76,7 +76,7 @@ namespace storm { initialStateIndex = stateStorage.initialStateIndices[0]; STORM_LOG_TRACE("Initial state: " << initialStateIndex); // Initialize heuristic values for inital state - statesNotExplored.at(initialStateIndex)->setHeuristicValues(0, storm::utility::zero(), storm::utility::zero()); + statesNotExplored.at(initialStateIndex).second->updateHeuristicValues(0, storm::utility::zero(), storm::utility::zero()); } else { initializeNextIteration(); } @@ -128,8 +128,8 @@ namespace storm { // Push skipped states to explore queue // TODO Matthias: remove for (auto const& skippedState : skippedStates) { - statesNotExplored[skippedState.second->getId()] = skippedState.second; - explorationQueue.push(skippedState.second->getId()); + statesNotExplored[skippedState.second.first->getId()] = skippedState.second; + explorationQueue.push(skippedState.second.second); } // Initialize matrix builder again @@ -157,7 +157,7 @@ namespace storm { matrixBuilder.mappingOffset = nrStates; STORM_LOG_TRACE("# expanded states: " << nrExpandedStates); StateType skippedIndex = nrExpandedStates; - std::map skippedStatesNew; + std::map> skippedStatesNew; for (size_t id = 0; id < matrixBuilder.stateRemapping.size(); ++id) { StateType index = matrixBuilder.stateRemapping[id]; auto itFind = skippedStates.find(index); @@ -204,7 +204,7 @@ namespace storm { auto itFind = skippedStates.find(itEntry->getColumn()); if (itFind != skippedStates.end()) { // Set id for skipped states as we remap it later - matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second->getId(), itEntry->getValue()); + matrixBuilder.addTransition(matrixBuilder.mappingOffset + itFind->second.first->getId(), itEntry->getValue()); } else { // Set newly remapped index for expanded states matrixBuilder.addTransition(indexRemapping[itEntry->getColumn()], itEntry->getValue()); @@ -228,10 +228,12 @@ namespace storm { // TODO Matthias: do not empty queue every time but break before while (!explorationQueue.empty()) { // Get the first state in the queue - StateType currentId = explorationQueue.popTop(); + ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); + StateType currentId = currentExplorationHeuristic->getId(); auto itFind = statesNotExplored.find(currentId); STORM_LOG_ASSERT(itFind != statesNotExplored.end(), "Id " << currentId << " not found"); - DFTStatePointer currentState = itFind->second; + DFTStatePointer currentState = itFind->second.first; + STORM_LOG_ASSERT(currentExplorationHeuristic == itFind->second.second, "Exploration heuristics do not match"); STORM_LOG_ASSERT(currentState->getId() == currentId, "Ids do not match"); // Remove it from the list of not explored states statesNotExplored.erase(itFind); @@ -254,7 +256,7 @@ namespace storm { bool fixQueue = false; generator.load(currentState); - if (currentState->isSkip(approximationThreshold, heuristic)) { + if (currentExplorationHeuristic->isSkip(approximationThreshold)) { // Skip the current state ++nrSkippedStates; STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); @@ -263,7 +265,7 @@ namespace storm { // TODO Matthias: what to do when there is no unique target state? matrixBuilder.addTransition(failedStateId, storm::utility::zero()); // Remember skipped state - skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = currentState; + skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic); matrixBuilder.finishRow(); } else { // Explore the current state @@ -282,7 +284,13 @@ namespace storm { // Set heuristic values for reached states auto iter = statesNotExplored.find(stateProbabilityPair.first); if (iter != statesNotExplored.end()) { - iter->second->setHeuristicValues(currentState, stateProbabilityPair.second, choice.getTotalMass()); + // Update heuristic values + DFTStatePointer state = iter->second.first; + if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->nrFailableDependencies() > 0 || (state->nrFailableDependencies() == 0 && state->nrFailableBEs() == 0)) { + // Do not skip absorbing state or if reached by dependencies + iter->second.second->markExpand(); + } + iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); fixQueue = true; } } @@ -421,12 +429,13 @@ namespace storm { auto matrixEntry = matrix.getRow(it->first, 0).begin(); STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); // Get the lower bound by considering the failure of all possible BEs + DFTStatePointer state = it->second.first; ValueType newRate = storm::utility::zero(); - for (size_t index = 0; index < it->second->nrFailableBEs(); ++index) { - newRate += it->second->getFailableBERate(index); + for (size_t index = 0; index < state->nrFailableBEs(); ++index) { + newRate += state->getFailableBERate(index); } - for (size_t index = 0; index < it->second->nrNotFailableBEs(); ++index) { - newRate += it->second->getNotFailableBERate(index); + for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { + newRate += state->getNotFailableBERate(index); } matrixEntry->setValue(newRate); } @@ -441,12 +450,13 @@ namespace storm { // Get the upper bound by considering the failure of all BEs // The used formula for the rate is 1/( 1/a + 1/b + ...) // TODO Matthias: improve by using closed formula for AND of all BEs + DFTStatePointer state = it->second.first; ValueType newRate = storm::utility::zero(); - for (size_t index = 0; index < it->second->nrFailableBEs(); ++index) { - newRate += storm::utility::one() / it->second->getFailableBERate(index); + for (size_t index = 0; index < state->nrFailableBEs(); ++index) { + newRate += storm::utility::one() / state->getFailableBERate(index); } - for (size_t index = 0; index < it->second->nrNotFailableBEs(); ++index) { - newRate += storm::utility::one() / it->second->getNotFailableBERate(index); + for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { + newRate += storm::utility::one() / state->getNotFailableBERate(index); } newRate = storm::utility::one() / newRate; matrixEntry->setValue(newRate); @@ -473,14 +483,14 @@ namespace storm { // Check if state is pseudo state // If state is explored already the possible pseudo state was already constructed auto iter = statesNotExplored.find(stateId); - if (iter != statesNotExplored.end() && iter->second->isPseudoState()) { + if (iter != statesNotExplored.end() && iter->second.first->isPseudoState()) { // Create pseudo state now - STORM_LOG_ASSERT(iter->second->getId() == stateId, "Ids do not match."); - STORM_LOG_ASSERT(iter->second->status() == state->status(), "Pseudo states do not coincide."); + STORM_LOG_ASSERT(iter->second.first->getId() == stateId, "Ids do not match."); + STORM_LOG_ASSERT(iter->second.first->status() == state->status(), "Pseudo states do not coincide."); state->setId(stateId); // Update mapping to map to concrete state now - statesNotExplored[stateId] = state; - // TODO Matthias: copy explorationHeuristic + // TODO Matthias: just change pointer? + statesNotExplored[stateId] = std::make_pair(state, iter->second.second); // We do not push the new state on the exploration queue as the pseudo state was already pushed STORM_LOG_TRACE("Created pseudo state " << dft.getStateString(state)); } @@ -493,8 +503,9 @@ namespace storm { stateId = stateStorage.stateToId.findOrAdd(state->status(), state->getId()); STORM_LOG_ASSERT(stateId == state->getId(), "Ids do not match."); // Insert state as not yet explored - statesNotExplored[stateId] = state; - explorationQueue.push(stateId); + ExplorationHeuristicPointer heuristic = std::make_shared(stateId); + statesNotExplored[stateId] = std::make_pair(state, heuristic); + explorationQueue.push(heuristic); // Reserve one slot for the new state in the remapping matrixBuilder.stateRemapping.push_back(0); STORM_LOG_TRACE("New " << (state->isPseudoState() ? "pseudo" : "concrete") << " state: " << dft.getStateString(state)); @@ -511,12 +522,6 @@ namespace storm { modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian); } - template - bool ExplicitDFTModelBuilderApprox::isPriorityGreater(StateType idA, StateType idB) const { - return statesNotExplored.at(idA)->comparePriority(statesNotExplored.at(idB), heuristic); - } - - // Explicitly instantiate the class. template class ExplicitDFTModelBuilderApprox; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 74798e889..4238194eb 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -26,11 +26,10 @@ namespace storm { template class ExplicitDFTModelBuilderApprox { - using DFTElementPointer = std::shared_ptr>; - using DFTElementCPointer = std::shared_ptr const>; - using DFTGatePointer = std::shared_ptr>; using DFTStatePointer = std::shared_ptr>; - using DFTRestrictionPointer = std::shared_ptr>; + // TODO Matthias: make choosable + using ExplorationHeuristic = DFTExplorationHeuristicNone; + using ExplorationHeuristicPointer = std::shared_ptr; // A structure holding the individual components of a model. @@ -294,16 +293,16 @@ namespace storm { storm::storage::sparse::StateStorage stateStorage; // A priority queue of states that still need to be explored. - storm::storage::DynamicPriorityQueue, std::function> explorationQueue; + storm::storage::DynamicPriorityQueue, std::function> explorationQueue; - // A mapping of not yet explored states from the id to the state object. - std::map statesNotExplored; + // A mapping of not yet explored states from the id to the tuple (state object, heuristic values). + std::map> statesNotExplored; // Holds all skipped states which were not yet expanded. More concretely it is a mapping from matrix indices // to the corresponding skipped states. // Notice that we need an ordered map here to easily iterate in increasing order over state ids. // TODO remove again - std::map skippedStates; + std::map> skippedStates; }; } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index f6bb692a7..70ff18122 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -6,7 +6,7 @@ namespace storm { namespace storage { template - DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo), exploreHeuristic() { + DFTState::DFTState(DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(dft.stateVectorSize()), mId(id), mPseudoState(false), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // TODO Matthias: use construct() // Initialize uses @@ -37,7 +37,7 @@ namespace storm { } template - DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo), exploreHeuristic() { + DFTState::DFTState(storm::storage::BitVector const& status, DFT const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mPseudoState(true), mDft(dft), mStateGenerationInfo(stateGenerationInfo) { // Intentionally left empty } @@ -85,9 +85,7 @@ namespace storm { template std::shared_ptr> DFTState::copy() const { - std::shared_ptr> stateCopy = std::make_shared>(*this); - stateCopy->exploreHeuristic = storm::builder::DFTExplorationHeuristic(); - return stateCopy; + return std::make_shared>(*this); } template diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index eb3164516..207eecac3 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -34,8 +34,7 @@ namespace storm { bool mValid = true; const DFT& mDft; const DFTStateGenerationInfo& mStateGenerationInfo; - storm::builder::DFTExplorationHeuristic exploreHeuristic; - + public: /** * Construct the initial state. @@ -123,26 +122,6 @@ namespace storm { return mPseudoState; } - void setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) { - exploreHeuristic.setHeuristicValues(depth, rate, exitRate); - } - - void setHeuristicValues(std::shared_ptr> oldState, ValueType rate, ValueType exitRate) { - if (hasFailed(mDft.getTopLevelIndex()) || isFailsafe(mDft.getTopLevelIndex()) || nrFailableDependencies() > 0 || (nrFailableDependencies() == 0 && nrFailableBEs() == 0)) { - // Do not skip absorbing state or if reached by dependencies - exploreHeuristic.setNotSkip(); - } - exploreHeuristic.setHeuristicValues(oldState->exploreHeuristic.getDepth() + 1, rate, exitRate); - } - - bool isSkip(double approximationThreshold, storm::builder::ApproximationHeuristic heuristic) { - return exploreHeuristic.isSkip(approximationThreshold, heuristic); - } - - bool comparePriority(std::shared_ptr const& other, storm::builder::ApproximationHeuristic heuristic) { - return this->exploreHeuristic.compare(other->exploreHeuristic, heuristic); - } - storm::storage::BitVector const& status() const { return mStatus; }