From 4a6f53031e01069f68789c205ff70b77f56c504d Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 18 Oct 2016 14:42:52 +0200 Subject: [PATCH 01/28] Choose different approximation heuristics Former-commit-id: e9ddae066b005a67e839a1f31405dd72d7790d0e --- src/builder/DftExplorationHeuristic.cpp | 57 +++++++++---------- src/builder/DftExplorationHeuristic.h | 9 ++- src/builder/ExplicitDFTModelBuilderApprox.cpp | 15 +++-- src/builder/ExplicitDFTModelBuilderApprox.h | 4 +- src/modelchecker/dft/DFTModelChecker.cpp | 4 +- src/storage/dft/DFTState.h | 6 +- 6 files changed, 48 insertions(+), 47 deletions(-) diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index 727c29c37..e14c34dee 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -15,6 +15,13 @@ namespace storm { // Intentionally left empty } + template + void DFTExplorationHeuristic::setHeuristicValues(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) { @@ -26,8 +33,9 @@ namespace storm { case ApproximationHeuristic::DEPTH: return depth > approximationThreshold; case ApproximationHeuristic::RATERATIO: - // TODO Matthias: implement - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work."); + return getRateRatio() < approximationThreshold; + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic not known."); } } @@ -36,52 +44,41 @@ namespace storm { skip = false; } - template size_t DFTExplorationHeuristic::getDepth() const { return depth; } template - void DFTExplorationHeuristic::setHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) { - this->depth = depth; - this->rate = rate; - this->exitRate = exitRate; - } - - template - double DFTExplorationHeuristic::getPriority() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); + 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."); + } } template<> - double DFTExplorationHeuristic::getPriority() const { - // TODO Matthias: change according to heuristic - //return rate/exitRate; - return depth; + double DFTExplorationHeuristic::getRateRatio() const { + return rate/exitRate; } template<> - double DFTExplorationHeuristic::getPriority() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); - /*std::cout << (rate / exitRate) << " < " << threshold << ": " << (number < threshold) << std::endl; - std::map mapping; - storm::RationalFunction eval(number.evaluate(mapping)); - std::cout << "Evaluated: " << eval << std::endl; - return eval < threshold;*/ - } - - template - bool compareDepth(std::shared_ptr> stateA, std::shared_ptr> stateB) { - return stateA->getPriority() > stateB->getPriority(); + double DFTExplorationHeuristic::getRateRatio() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work."); } template class DFTExplorationHeuristic; - template bool compareDepth(std::shared_ptr>, std::shared_ptr>); #ifdef STORM_HAVE_CARL template class DFTExplorationHeuristic; - template bool compareDepth(std::shared_ptr>, std::shared_ptr>); #endif } } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index a9958443a..3fd3d72a8 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -33,19 +33,18 @@ namespace storm { size_t getDepth() const; - double getPriority() const; - + bool compare(DFTExplorationHeuristic other, ApproximationHeuristic heuristic); + private: + double getRateRatio() const; + bool skip; size_t depth; ValueType rate; ValueType exitRate; }; - - template - bool compareDepth(std::shared_ptr> stateA, std::shared_ptr> stateB); } } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index cb04f3135..5acf60980 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -39,10 +39,10 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationThreshold) { + void ExplicitDFTModelBuilderApprox::buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold) { STORM_LOG_TRACE("Generating DFT state space"); - if (firstTime) { + if (iteration < 1) { // Initialize modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE); @@ -80,6 +80,14 @@ namespace storm { initializeNextIteration(); } + switch (heuristic) { + case storm::builder::ApproximationHeuristic::DEPTH: + approximationThreshold = iteration; + break; + case storm::builder::ApproximationHeuristic::RATERATIO: + approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; + break; + } exploreStateSpace(approximationThreshold); size_t stateSize = stateStorage.getNumberOfStates() + (mergeFailedStates ? 1 : 0); @@ -486,8 +494,7 @@ namespace storm { template bool ExplicitDFTModelBuilderApprox::isPriorityGreater(StateType idA, StateType idB) const { - // TODO Matthias: compare directly and according to heuristic - return storm::builder::compareDepth(statesNotExplored.at(idA), statesNotExplored.at(idB)); + return statesNotExplored.at(idA)->comparePriority(statesNotExplored.at(idB), heuristic); } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 5e841fddc..74798e889 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -159,10 +159,10 @@ namespace storm { * Build model from DFT. * * @param labelOpts Options for labeling. - * @param firstTime Flag indicating if the model is built for the first time or rebuilt. + * @param iteration Current number of iteration. * @param approximationThreshold Threshold determining when to skip exploring states. */ - void buildModel(LabelOptions const& labelOpts, bool firstTime, double approximationThreshold = 0.0); + void buildModel(LabelOptions const& labelOpts, size_t iteration, double approximationThreshold = 0.0); /*! * Get the built model. diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index 717ace4c3..1fa1ca245 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -150,7 +150,6 @@ namespace storm { // Comparator for checking the error of the approximation storm::utility::ConstantsComparator comparator; // Build approximate Markov Automata for lower and upper bound - double currentApproximationError = approximationError; approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); std::chrono::high_resolution_clock::time_point explorationStart; std::shared_ptr> model; @@ -163,8 +162,7 @@ namespace storm { explorationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_INFO("Building model..."); // TODO Matthias refine model using existing model and MC results - currentApproximationError = pow(0.1, iteration) * approximationError; - builder.buildModel(labeloptions, iteration < 1, iteration); + builder.buildModel(labeloptions, iteration, approximationError); // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one? diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index b2fb803da..eb3164516 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -139,10 +139,10 @@ namespace storm { return exploreHeuristic.isSkip(approximationThreshold, heuristic); } - double getPriority() const { - return exploreHeuristic.getPriority(); + 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; } From 1bfd9747957838406ddb033ac093ad99d0793902 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 18 Oct 2016 15:58:43 +0200 Subject: [PATCH 02/28] Minor fixes Former-commit-id: 9344ebe5aac6a410ae5e84b4230037401c2946f3 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 19 +++++++++++++++---- src/generator/DftNextStateGenerator.cpp | 4 ---- src/modelchecker/dft/DFTModelChecker.cpp | 2 +- 3 files changed, 16 insertions(+), 9 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 5acf60980..fda689be7 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -75,12 +75,16 @@ namespace storm { STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed."); 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()); } else { initializeNextIteration(); } switch (heuristic) { + case storm::builder::ApproximationHeuristic::NONE: + // Do not change anything + break; case storm::builder::ApproximationHeuristic::DEPTH: approximationThreshold = iteration; break; @@ -246,6 +250,7 @@ namespace storm { matrixBuilder.newRowGroup(); // Try to explore the next state + bool fixQueue = false; generator.load(currentState); if (currentState->isSkip(approximationThreshold, heuristic)) { @@ -270,15 +275,21 @@ namespace storm { for (auto const& stateProbabilityPair : choice) { // Set transition to state id + offset. This helps in only remapping all previously skipped states. matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second); - // TODO Matthias: set heuristic values here + // Set heuristic values for reached states + auto iter = statesNotExplored.find(stateProbabilityPair.first); + if (iter != statesNotExplored.end()) { + iter->second->setHeuristicValues(currentState, stateProbabilityPair.second, choice.getTotalMass()); + fixQueue = true; + } } matrixBuilder.finishRow(); } } // Update priority queue - // TODO Matthias: only when necessary - explorationQueue.fix(); + if (fixQueue) { + explorationQueue.fix(); + } } // end exploration } diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp index e61e8e331..69fca22b4 100644 --- a/src/generator/DftNextStateGenerator.cpp +++ b/src/generator/DftNextStateGenerator.cpp @@ -20,7 +20,6 @@ namespace storm { template std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); - initialState->setHeuristicValues(0, storm::utility::zero(), storm::utility::zero()); // Register initial state StateType id = stateToIdCallback(initialState); @@ -158,10 +157,8 @@ namespace storm { ValueType remainingProbability = storm::utility::one() - probability; choice.addProbability(unsuccessfulStateId, remainingProbability); STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability); - unsuccessfulState->setHeuristicValues(state, remainingProbability, storm::utility::one()); } result.addChoice(std::move(choice)); - newState->setHeuristicValues(state, probability, storm::utility::one()); } else { // Failure is due to "normal" BE failure // Set failure rate according to activation @@ -174,7 +171,6 @@ namespace storm { STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0."); choice.addProbability(newStateId, rate); STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate); - newState->setHeuristicValues(state, rate, choice.getTotalMass()); } ++currentFailable; diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index 1fa1ca245..cadc37ac7 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -204,7 +204,7 @@ namespace storm { if (approximationError >= 0.0) { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, true); + builder.buildModel(labeloptions, 0); model = builder.getModel(); } else { storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC); From ec8b5a23f2e8b7176762a0fa328f8e0db9ddfe39 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 20 Oct 2016 16:57:28 +0200 Subject: [PATCH 03/28] Fixed compile issues with under Linux Former-commit-id: 17f4d895ec52241f653fc9a175d4609c88d71a94 --- src/builder/DftSmtBuilder.cpp | 2 +- src/storm-dyftee.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/builder/DftSmtBuilder.cpp b/src/builder/DftSmtBuilder.cpp index 1d60b2c74..c1226531c 100644 --- a/src/builder/DftSmtBuilder.cpp +++ b/src/builder/DftSmtBuilder.cpp @@ -1,4 +1,4 @@ -#include "src/builder/DFTSMTBuilder.h" +#include "src/builder/DftSmtBuilder.h" #include "src/exceptions/NotImplementedException.h" namespace storm { diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp index 51061050e..fb0c0b1e6 100644 --- a/src/storm-dyftee.cpp +++ b/src/storm-dyftee.cpp @@ -117,6 +117,7 @@ int main(const int argc, const char** argv) { parametric = generalSettings.isParametricSet(); #endif +#ifdef STORM_HAVE_Z3 if (dftSettings.solveWithSMT()) { // Solve with SMT if (parametric) { @@ -127,6 +128,7 @@ int main(const int argc, const char** argv) { storm::utility::cleanUp(); return 0; } +#endif // Set min or max bool minimal = true; From a624292ecea60e9983ef677b97c76accabc3a0a9 Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 21 Oct 2016 18:28:01 +0200 Subject: [PATCH 04/28] Output no states Former-commit-id: d1548bb3fba7fe2ecbf4f20dc79eb61f4f9369f5 --- src/builder/ExplicitDFTModelBuilder.cpp | 1 + src/builder/ExplicitDFTModelBuilderApprox.cpp | 12 ++++++++++-- src/modelchecker/dft/DFTModelChecker.cpp | 5 ++++- 3 files changed, 15 insertions(+), 3 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index 9481e3392..4a2f56b5f 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -58,6 +58,7 @@ namespace storm { STORM_LOG_ASSERT(mStates.getValue(pseudoStatePair.second) >= OFFSET_PSEUDO_STATE, "State is no pseudo state."); STORM_LOG_TRACE("Create pseudo state from bit vector " << pseudoStatePair.second); DFTStatePointer pseudoState = std::make_shared>(pseudoStatePair.second, mDft, *mStateGenerationInfo, newIndex); + pseudoState->construct(); STORM_LOG_ASSERT(pseudoStatePair.second == pseudoState->status(), "Pseudo states do not coincide."); STORM_LOG_TRACE("Explore pseudo state " << mDft.getStateString(pseudoState) << " with id " << pseudoState->getId()); auto exploreResult = exploreStates(pseudoState, rowOffset, transitionMatrixBuilder, tmpMarkovianStates, modelComponents.exitRates); diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index fda689be7..268ec03dc 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -106,8 +106,7 @@ namespace storm { STORM_LOG_TRACE("State remapping: " << matrixBuilder.stateRemapping); STORM_LOG_TRACE("Markovian states: " << modelComponents.markovianStates); - STORM_LOG_DEBUG("Generated " << stateSize << " states"); - STORM_LOG_DEBUG("Skipped " << skippedStates.size() << " states"); + STORM_LOG_DEBUG("Model has " << stateSize << " states"); STORM_LOG_DEBUG("Model is " << (generator.isDeterministicModel() ? "deterministic" : "non-deterministic")); // Build transition matrix @@ -224,6 +223,8 @@ namespace storm { template void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { + size_t nrExpandedStates = 0; + size_t nrSkippedStates = 0; // TODO Matthias: do not empty queue every time but break before while (!explorationQueue.empty()) { // Get the first state in the queue @@ -255,6 +256,7 @@ namespace storm { if (currentState->isSkip(approximationThreshold, heuristic)) { // Skip the current state + ++nrSkippedStates; STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); setMarkovian(true); // Add transition to target state with temporary value 0 @@ -265,6 +267,7 @@ namespace storm { matrixBuilder.finishRow(); } else { // Explore the current state + ++nrExpandedStates; storm::generator::StateBehavior behavior = generator.expand(std::bind(&ExplicitDFTModelBuilderApprox::getOrAddStateIndex, this, std::placeholders::_1)); STORM_LOG_ASSERT(!behavior.empty(), "Behavior is empty."); setMarkovian(behavior.begin()->isMarkovian()); @@ -273,6 +276,7 @@ namespace storm { for (auto const& choice : behavior) { // Add the probabilistic behavior to the matrix. for (auto const& stateProbabilityPair : choice) { + STORM_LOG_ASSERT(!storm::utility::isZero(stateProbabilityPair.second), "Probability zero."); // Set transition to state id + offset. This helps in only remapping all previously skipped states. matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second); // Set heuristic values for reached states @@ -291,6 +295,10 @@ namespace storm { explorationQueue.fix(); } } // end exploration + + STORM_LOG_INFO("Expanded " << nrExpandedStates << " states"); + STORM_LOG_INFO("Skipped " << nrSkippedStates << " states"); + STORM_LOG_ASSERT(nrSkippedStates == skippedStates.size(), "Nr skipped states is wrong"); } template diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index cadc37ac7..f19943f2f 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -169,6 +169,9 @@ namespace storm { // Build model for lower bound STORM_LOG_INFO("Getting model for lower bound..."); model = builder.getModelApproximation(true); + // We only output the info from the lower bound as the info for the upper bound is the same + STORM_LOG_INFO("No. states: " << model->getNumberOfStates()); + STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); explorationTime += std::chrono::high_resolution_clock::now() - explorationStart; // Check lower bound std::unique_ptr result = checkModel(model, formula); @@ -201,7 +204,7 @@ namespace storm { STORM_LOG_INFO("Building Model..."); std::shared_ptr> model; // TODO Matthias: use only one builder if everything works again - if (approximationError >= 0.0) { + if (storm::settings::getModule().isApproximationErrorSet()) { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula builder.buildModel(labeloptions, 0); From a333d29d1663a877fd0980d5ecc562213463a9b9 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sat, 22 Oct 2016 17:31:02 +0200 Subject: [PATCH 05/28] 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; } From 82a3964e5dab0c6d9d0404a0efa08c576bb0a554 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sat, 22 Oct 2016 18:30:26 +0200 Subject: [PATCH 06/28] Only fix queue when needed Former-commit-id: 50231c4554e3bf6cdeeb7b6de37778fa3faedb3a --- src/builder/DftExplorationHeuristic.cpp | 71 +++++-------------- src/builder/DftExplorationHeuristic.h | 66 +++++++++++++---- src/builder/ExplicitDFTModelBuilderApprox.cpp | 3 +- 3 files changed, 73 insertions(+), 67 deletions(-) diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index 4bc72ccc1..3b9c2e110 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -14,69 +14,34 @@ namespace storm { // Intentionally left empty } - template - 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 - DFTExplorationHeuristicNone::DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { - // Intentionally left empty + template<> + bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, double rate, double exitRate) { + bool update = false; + if (this->rate < rate) { + this->rate = rate; + update = true; + } + if (this->exitRate < exitRate) { + this->exitRate = exitRate; + update = true; + } + return update; } - template - bool DFTExplorationHeuristicNone::isSkip(double approximationThreshold) const { + template<> + bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, storm::RationalFunction rate, storm::RationalFunction exitRate) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); 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 - DFTExplorationHeuristicRateRatio::DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic(id) { - // Intentionally left empty - } - - template - bool DFTExplorationHeuristicRateRatio::isSkip(double approximationThreshold) const { - return !this->expand && this->getRateRatio() < approximationThreshold; - } - - template - bool DFTExplorationHeuristicRateRatio::operator<(DFTExplorationHeuristicRateRatio const& other) const { - return this->getRateRatio() < other.getRateRatio(); - } - - template<> - double DFTExplorationHeuristicRateRatio::getRateRatio() const { + double DFTExplorationHeuristicRateRatio::getPriority() const { return rate/exitRate; } template<> - double DFTExplorationHeuristicRateRatio::getRateRatio() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work."); + double DFTExplorationHeuristicRateRatio::getPriority() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 8f12d2ec1..2b4fc5047 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -22,7 +22,9 @@ namespace storm { public: DFTExplorationHeuristic(size_t id); - void updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate); + virtual bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) = 0; + + virtual double getPriority() const = 0; virtual bool isSkip(double approximationThreshold) const = 0; @@ -50,34 +52,74 @@ namespace storm { template class DFTExplorationHeuristicNone : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicNone(size_t id); + DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override { + return false; + } + + double getPriority() const override { + return this->id; + } - bool isSkip(double approximationThreshold) const override; + bool isSkip(double approximationThreshold) const override { + return false; + } - bool operator<(DFTExplorationHeuristicNone const& other) const; + bool operator<(DFTExplorationHeuristicNone const& other) const { + return this->id > other.id; + } }; template class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicDepth(size_t id); + DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override { + if (depth < this->depth) { + this->depth = depth; + return true; + } + return false; + } + - bool isSkip(double approximationThreshold) const override; + double getPriority() const override { + return this->depth; + } + + bool isSkip(double approximationThreshold) const override { + return !this->expand && this->depth > approximationThreshold; + } - bool operator<(DFTExplorationHeuristicDepth const& other) const; + bool operator<(DFTExplorationHeuristicDepth const& other) const { + return this->depth > other.depth; + } }; template class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicRateRatio(size_t id); + DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } - bool isSkip(double approximationThreshold) const override; + bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override; - bool operator<(DFTExplorationHeuristicRateRatio const& other) const; + double getPriority() const override; - private: - double getRateRatio() const; + bool isSkip(double approximationThreshold) const override { + return !this->expand && this->getPriority() < approximationThreshold; + } + + bool operator<(DFTExplorationHeuristicRateRatio const& other) const { + return this->getPriority() < other.getPriority(); + } }; } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 5595a5f49..ed7c1500d 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -290,8 +290,7 @@ namespace storm { // 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; + fixQueue = iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); } } matrixBuilder.finishRow(); From d1d77ff4df3b5d79a3ba956c61f17763012226d3 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 24 Oct 2016 15:20:03 +0200 Subject: [PATCH 07/28] Changed deque to vector in bisimulation to gain performance boost Former-commit-id: 5db8e917b47000312198ad2e94773bec86912ebd --- .../BisimulationDecomposition.cpp | 16 +++++------ .../bisimulation/BisimulationDecomposition.h | 8 +++--- ...ministicModelBisimulationDecomposition.cpp | 28 +++++++++---------- ...erministicModelBisimulationDecomposition.h | 10 +++---- ...ministicModelBisimulationDecomposition.cpp | 14 +++++----- ...erministicModelBisimulationDecomposition.h | 8 +++--- 6 files changed, 42 insertions(+), 42 deletions(-) diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index 4b31551f9..33d4cffcc 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -230,25 +230,25 @@ namespace storm { template void BisimulationDecomposition::performPartitionRefinement() { - // Insert all blocks into the splitter queue as a (potential) splitter. - std::deque*> splitterQueue; - std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr> const& block) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } ); + // Insert all blocks into the splitter vector as a (potential) splitter. + std::vector*> splitterVector; + std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr> const& block) { block->data().setSplitter(); splitterVector.push_back(block.get()); } ); // Then perform the actual splitting until there are no more splitters. uint_fast64_t iterations = 0; - while (!splitterQueue.empty()) { + while (!splitterVector.empty()) { ++iterations; // Get and prepare the next splitter. // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but // tends to work well. - std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); - Block* splitter = splitterQueue.front(); - splitterQueue.pop_front(); + std::sort(splitterVector.begin(), splitterVector.end(), [] (Block const* b1, Block const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); } ); + Block* splitter = splitterVector.back(); + splitterVector.pop_back(); splitter->data().setSplitter(false); // Now refine the partition using the current splitter. - refinePartitionBasedOnSplitter(*splitter, splitterQueue); + refinePartitionBasedOnSplitter(*splitter, splitterVector); } } diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 6d86f2df9..df951bce3 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -1,7 +1,7 @@ #ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ #define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ -#include +#include #include "src/settings/SettingsManager.h" #include "src/settings/modules/BisimulationSettings.h" @@ -219,12 +219,12 @@ namespace storm { /*! * Refines the partition by considering the given splitter. All blocks that become potential splitters - * because of this refinement, are marked as splitters and inserted into the splitter queue. + * because of this refinement, are marked as splitters and inserted into the splitter vector. * * @param splitter The splitter to use. - * @param splitterQueue The queue into which to insert the newly discovered potential splitters. + * @param splitterVector The vector into which to insert the newly discovered potential splitters. */ - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) = 0; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) = 0; /*! * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index e968c98cd..dcc12fbfb 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -157,7 +157,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterVector) { for (auto block : predecessorBlocks) { STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter"); @@ -176,15 +176,15 @@ namespace storm { [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return this->comparator.isLess(getProbabilityToSplitter(state1), getProbabilityToSplitter(state2)); }, - [&splitterQueue] (Block& block) { - splitterQueue.emplace_back(&block); block.data().setSplitter(); + [&splitterVector] (Block& block) { + splitterVector.emplace_back(&block); block.data().setSplitter(); }); - // If the predecessor block was split, we need to insert it into the splitter queue if it is not already + // If the predecessor block was split, we need to insert it into the splitter vector if it is not already // marked as a splitter. if (split && !blockToRefineProbabilistically->data().splitter()) { - splitterQueue.emplace_back(blockToRefineProbabilistically); + splitterVector.emplace_back(blockToRefineProbabilistically); blockToRefineProbabilistically->data().setSplitter(); } @@ -378,7 +378,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::vector*>& splitterVector) { // First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities // for all non-silent states. computeConditionalProbabilitiesForNonSilentStates(block); @@ -395,12 +395,12 @@ namespace storm { [&weakStateLabels,&block,originalBlockIndex,this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { return weakStateLabels[this->partition.getPosition(state1) - originalBlockIndex] < weakStateLabels[this->partition.getPosition(state2) - originalBlockIndex]; }, - [this, &splitterQueue] (bisimulation::Block& block) { + [this, &splitterVector] (bisimulation::Block& block) { updateSilentProbabilitiesBasedOnTransitions(block); // Insert the new block as a splitter. block.data().setSplitter(); - splitterQueue.emplace_back(&block); + splitterVector.emplace_back(&block); }); // If the block was split, we also update the silent probabilities. @@ -410,16 +410,16 @@ namespace storm { if (!block.data().splitter()) { // Insert the new block as a splitter. block.data().setSplitter(); - splitterQueue.emplace_back(&block); + splitterVector.emplace_back(&block); } } } template - void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterVector) { for (auto block : predecessorBlocks) { if (*block != splitter) { - refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); + refinePredecessorBlockOfSplitterWeak(*block, splitterVector); } else { // If the block to split is the splitter itself, we must not do any splitting here. } @@ -439,7 +439,7 @@ namespace storm { } template - void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) { STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId()); // The outline of the refinement is as follows. @@ -513,7 +513,7 @@ namespace storm { if (this->options.getType() == BisimulationType::Strong || this->model.getType() == storm::models::ModelType::Ctmc) { // In the case of CTMCs and weak bisimulation, we still call the "splitStrong" method, but we already have // taken care of not adding the splitter to the predecessor blocks, so this is safe. - refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterQueue); + refinePredecessorBlocksOfSplitterStrong(predecessorBlocks, splitterVector); } else { // If the splitter is a predecessor of we can use the computed probabilities to update the silent // probabilities. @@ -521,7 +521,7 @@ namespace storm { updateSilentProbabilitiesBasedOnProbabilitiesToSplitter(splitter); } - refinePredecessorBlocksOfSplitterWeak(splitter, predecessorBlocks, splitterQueue); + refinePredecessorBlocksOfSplitterWeak(splitter, predecessorBlocks, splitterVector); } } diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index b9f2a2a5a..b460dfa5d 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -39,11 +39,11 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) override; private: // Refines the predecessor blocks wrt. strong bisimulation. - void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::deque*>& splitterQueue); + void refinePredecessorBlocksOfSplitterStrong(std::list*> const& predecessorBlocks, std::vector*>& splitterVector); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -99,10 +99,10 @@ namespace storm { 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); + void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block& splitter, std::list*> const& predecessorBlocks, std::vector*>& splitterVector); // Refines the given block wrt to weak bisimulation in DTMCs. - void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::deque*>& splitterQueue); + void refinePredecessorBlockOfSplitterWeak(bisimulation::Block& block, std::vector*>& splitterVector); // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed // for weak bisimulation (on DTMCs). @@ -127,4 +127,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 2e7d54113..fe53c6602 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -198,7 +198,7 @@ namespace storm { } template - void NondeterministicModelBisimulationDecomposition::updateQuotientDistributionsOfPredecessors(Block const& newBlock, Block const& oldBlock, std::deque*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition::updateQuotientDistributionsOfPredecessors(Block const& newBlock, Block const& oldBlock, std::vector*>& splitterVector) { uint_fast64_t lastState = 0; bool lastStateInitialized = false; @@ -220,7 +220,7 @@ namespace storm { // If the predecessor block is not marked as to-refined, we do so now. if (!predecessorBlock.data().splitter()) { predecessorBlock.data().setSplitter(); - splitterQueue.push_back(&predecessorBlock); + splitterVector.push_back(&predecessorBlock); } if (lastStateInitialized) { @@ -332,7 +332,7 @@ namespace storm { } template - bool NondeterministicModelBisimulationDecomposition::splitBlockAccordingToCurrentQuotientDistributions(Block& block, std::deque*>& splitterQueue) { + bool NondeterministicModelBisimulationDecomposition::splitBlockAccordingToCurrentQuotientDistributions(Block& block, std::vector*>& splitterVector) { std::list*> newBlocks; bool split = this->partition.splitBlock(block, [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { @@ -340,7 +340,7 @@ namespace storm { // std::cout << state1 << " is " << (!result ? "not" : "") << " smaller than " << state2 << std::endl; return result; }, - [this, &block, &splitterQueue, &newBlocks] (Block& newBlock) { + [this, &block, &splitterVector, &newBlocks] (Block& newBlock) { newBlocks.push_back(&newBlock); // this->checkBlockStable(newBlock); @@ -357,7 +357,7 @@ namespace storm { // defer updating the quotient distributions until *after* all splits, because // it otherwise influences the subsequent splits! for (auto el : newBlocks) { - this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue); + this->updateQuotientDistributionsOfPredecessors(*el, block, splitterVector); } // this->checkQuotientDistributions(); @@ -405,14 +405,14 @@ namespace storm { } template - void NondeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition::refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) { if (!possiblyNeedsRefinement(splitter)) { return; } STORM_LOG_TRACE("Refining block " << splitter.getId()); - splitBlockAccordingToCurrentQuotientDistributions(splitter, splitterQueue); + splitBlockAccordingToCurrentQuotientDistributions(splitter, splitterVector); } template class NondeterministicModelBisimulationDecomposition>; diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h index 18a6e8e58..38feaf36a 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -37,7 +37,7 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::deque*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block& splitter, std::vector*>& splitterVector) override; virtual void initialize() override; @@ -52,7 +52,7 @@ namespace storm { bool possiblyNeedsRefinement(bisimulation::Block const& block) const; // Splits the given block according to the current quotient distributions. - bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block& block, std::deque*>& splitterQueue); + bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block& block, std::vector*>& splitterVector); // Retrieves whether the quotient distributions of state 1 are considered to be less than the ones of state 2. bool quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const; @@ -62,7 +62,7 @@ namespace storm { // Updates the quotient distributions of the predecessors of the new block by taking the probability mass // away from the old block. - void updateQuotientDistributionsOfPredecessors(bisimulation::Block const& newBlock, bisimulation::Block const& oldBlock, std::deque*>& splitterQueue); + void updateQuotientDistributionsOfPredecessors(bisimulation::Block const& newBlock, bisimulation::Block const& oldBlock, std::vector*>& splitterVector); bool checkQuotientDistributions() const; bool checkBlockStable(bisimulation::Block const& newBlock) const; @@ -81,4 +81,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ From 8d38358c115dda77d55c001c2f8178c2f52aebbb Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 24 Oct 2016 17:28:56 +0200 Subject: [PATCH 08/28] Use BucketPriorityQueue instead of DynamicPriorityQueue Former-commit-id: 7a22ef5b1671b4a33319e4cc6c98bff2e473aa77 --- src/builder/DftExplorationHeuristic.cpp | 22 +- src/builder/DftExplorationHeuristic.h | 12 +- src/builder/ExplicitDFTModelBuilderApprox.cpp | 55 +++-- src/builder/ExplicitDFTModelBuilderApprox.h | 9 +- src/storage/BucketPriorityQueue.cpp | 191 ++++++++++++++++++ src/storage/BucketPriorityQueue.h | 70 +++++++ 6 files changed, 320 insertions(+), 39 deletions(-) create mode 100644 src/storage/BucketPriorityQueue.cpp create mode 100644 src/storage/BucketPriorityQueue.h diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index 3b9c2e110..dbd64088b 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -4,28 +4,20 @@ #include "src/utility/constants.h" #include "src/exceptions/NotImplementedException.h" -#include - namespace storm { namespace builder { template - 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 + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(depth) { + STORM_LOG_ASSERT(storm::utility::zero() < exitRate, "Exit rate is 0"); + rateRatio = rate/exitRate; } template<> bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, double rate, double exitRate) { - bool update = false; - if (this->rate < rate) { - this->rate = rate; - update = true; - } - if (this->exitRate < exitRate) { - this->exitRate = exitRate; - update = true; - } - return update; + STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0"); + rateRatio += rate/exitRate; + return true; } template<> @@ -36,7 +28,7 @@ namespace storm { template<> double DFTExplorationHeuristicRateRatio::getPriority() const { - return rate/exitRate; + return rateRatio; } template<> diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 2b4fc5047..d23c673fc 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -20,7 +20,7 @@ namespace storm { class DFTExplorationHeuristic { public: - DFTExplorationHeuristic(size_t id); + DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate); virtual bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) = 0; @@ -44,15 +44,13 @@ namespace storm { size_t id; bool expand; size_t depth; - ValueType rate; - ValueType exitRate; - + ValueType rateRatio; }; template class DFTExplorationHeuristicNone : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { + DFTExplorationHeuristicNone(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { // Intentionally left empty } @@ -76,7 +74,7 @@ namespace storm { template class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic(id) { + DFTExplorationHeuristicDepth(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { // Intentionally left empty } @@ -105,7 +103,7 @@ namespace storm { template class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicRateRatio(size_t id) : DFTExplorationHeuristic(id) { + DFTExplorationHeuristicRateRatio(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { // Intentionally left empty } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index ed7c1500d..07863bb01 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -31,11 +31,13 @@ namespace storm { generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates), matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), - explorationQueue([this](ExplorationHeuristicPointer a, ExplorationHeuristicPointer b) { - return *a < *b; - }) + // TODO Matthias: make choosable + //explorationQueue(dft.nrElements(), 0, 1) + explorationQueue(41, 0, 1.0/20) { // Intentionally left empty. + // TODO Matthias: remove again + heuristic = storm::builder::ApproximationHeuristic::RATERATIO; } template @@ -76,7 +78,11 @@ namespace storm { initialStateIndex = stateStorage.initialStateIndices[0]; STORM_LOG_TRACE("Initial state: " << initialStateIndex); // Initialize heuristic values for inital state - statesNotExplored.at(initialStateIndex).second->updateHeuristicValues(0, storm::utility::zero(), storm::utility::zero()); + STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); + ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex, 0, storm::utility::zero(), storm::utility::one()); + heuristic->markExpand(); + statesNotExplored[initialStateIndex].second = heuristic; + explorationQueue.push(heuristic); } else { initializeNextIteration(); } @@ -84,6 +90,7 @@ namespace storm { switch (heuristic) { case storm::builder::ApproximationHeuristic::NONE: // Do not change anything + approximationThreshold = 0; break; case storm::builder::ApproximationHeuristic::DEPTH: approximationThreshold = iteration; @@ -225,8 +232,12 @@ namespace storm { void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { size_t nrExpandedStates = 0; size_t nrSkippedStates = 0; + size_t fix = 0; // TODO Matthias: do not empty queue every time but break before while (!explorationQueue.empty()) { + explorationQueue.fix(); + //explorationQueue.print(std::cout); + //printNotExplored(); // Get the first state in the queue ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); StateType currentId = currentExplorationHeuristic->getId(); @@ -253,7 +264,6 @@ namespace storm { matrixBuilder.newRowGroup(); // Try to explore the next state - bool fixQueue = false; generator.load(currentState); if (currentExplorationHeuristic->isSkip(approximationThreshold)) { @@ -286,22 +296,31 @@ namespace storm { if (iter != statesNotExplored.end()) { // Update heuristic values DFTStatePointer state = iter->second.first; + if (!iter->second.second) { + // Initialize heuristic values + ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); + iter->second.second = heuristic; + explorationQueue.push(heuristic); + } else { + double oldPriority = iter->second.second->getPriority(); + if (iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass())) { + // Update priority queue + ++fix; + explorationQueue.update(iter->second.second, oldPriority); + } + } 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(); + // TODO Matthias give highest priority to ensure expanding before all skipped } - fixQueue = iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); } } matrixBuilder.finishRow(); } } - - // Update priority queue - if (fixQueue) { - explorationQueue.fix(); - } } // end exploration + std::cout << "Fixed queue " << fix << " times" << std::endl; STORM_LOG_INFO("Expanded " << nrExpandedStates << " states"); STORM_LOG_INFO("Skipped " << nrSkippedStates << " states"); @@ -502,9 +521,8 @@ 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 - ExplorationHeuristicPointer heuristic = std::make_shared(stateId); - statesNotExplored[stateId] = std::make_pair(state, heuristic); - explorationQueue.push(heuristic); + ExplorationHeuristicPointer nullHeuristic; + statesNotExplored[stateId] = std::make_pair(state, nullHeuristic); // 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)); @@ -521,6 +539,15 @@ namespace storm { modelComponents.markovianStates.set(matrixBuilder.getCurrentRowGroup() - 1, markovian); } + template + void ExplicitDFTModelBuilderApprox::printNotExplored() const { + std::cout << "states not explored:" << std::endl; + for (auto it : statesNotExplored) { + std::cout << it.first << " -> " << dft.getStateString(it.second.first) << std::endl; + } + } + + // Explicitly instantiate the class. template class ExplicitDFTModelBuilderApprox; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 4238194eb..e23a8e819 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -10,7 +10,7 @@ #include "src/storage/sparse/StateStorage.h" #include "src/storage/dft/DFT.h" #include "src/storage/dft/SymmetricUnits.h" -#include "src/storage/DynamicPriorityQueue.h" +#include "src/storage/BucketPriorityQueue.h" #include #include #include @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicNone; + using ExplorationHeuristic = DFTExplorationHeuristicRateRatio; using ExplorationHeuristicPointer = std::shared_ptr; @@ -240,6 +240,8 @@ namespace storm { */ bool isPriorityGreater(StateType idA, StateType idB) const; + void printNotExplored() const; + /*! * Create the model model from the model components. * @@ -293,7 +295,8 @@ 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::BucketPriorityQueue explorationQueue; + //storm::storage::DynamicPriorityQueue, std::function> explorationQueue; // A mapping of not yet explored states from the id to the tuple (state object, heuristic values). std::map> statesNotExplored; diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp new file mode 100644 index 000000000..e87e25506 --- /dev/null +++ b/src/storage/BucketPriorityQueue.cpp @@ -0,0 +1,191 @@ +#include "src/storage/BucketPriorityQueue.h" +#include "src/utility/macros.h" +#include "src/adapters/CarlAdapter.h" + +namespace storm { + namespace storage { + + template + BucketPriorityQueue::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket) : buckets(nrBuckets), currentBucket(nrBuckets), lowerValue(lowerValue), stepPerBucket(stepPerBucket), nrUnsortedItems(0) { + compare = ([this](HeuristicPointer a, HeuristicPointer b) { + return *a < *b; + }); + } + + template + void BucketPriorityQueue::fix() { + if (currentBucket < buckets.size() && nrUnsortedItems > 0) { + // Fix current bucket + std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + nrUnsortedItems = 0; + } + } + + template + bool BucketPriorityQueue::empty() const { + return currentBucket == buckets.size(); + } + + template + std::size_t BucketPriorityQueue::size() const { + size_t size = 0; + for (size_t i = currentBucket; currentBucket < buckets.size(); ++i) { + size += buckets[i].size(); + } + STORM_LOG_ASSERT(size == heuristicMapping.size(), "Sizes to not coincide"); + return size; + } + + template + typename BucketPriorityQueue::HeuristicPointer const& BucketPriorityQueue::top() const { + STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); + STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); + return buckets[currentBucket].front(); + } + + template + void BucketPriorityQueue::push(HeuristicPointer const& item) { + size_t bucket = getBucket(item->getPriority()); + if (bucket < currentBucket) { + setMappingBucket(currentBucket); + currentBucket = bucket; + nrUnsortedItems = 0; + } + buckets[bucket].push_back(item); + if (bucket == currentBucket) { + // Insert in first bucket + if (AUTOSORT) { + std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + } else { + ++nrUnsortedItems; + } + } + // Set mapping + heuristicMapping[item->getId()] = std::make_pair(bucket, buckets[bucket].size() - 1); + } + + template + void BucketPriorityQueue::update(HeuristicPointer const& item, double oldPriority) { + size_t newBucket = getBucket(item->getPriority()); + size_t oldBucket = getBucket(oldPriority); + + if (oldBucket == newBucket) { + if (currentBucket < newBucket) { + // No change as the bucket is not sorted yet + } else { + if (AUTOSORT) { + // Sort first bucket + fix(); + } else { + ++nrUnsortedItems; + } + } + } else { + // Move to new bucket + STORM_LOG_ASSERT(newBucket < oldBucket, "Will update to higher bucket"); + if (newBucket < currentBucket) { + setMappingBucket(currentBucket); + currentBucket = newBucket; + nrUnsortedItems = 0; + } + // Remove old entry by swap-and-pop + if (buckets[oldBucket].size() >= 2) { + size_t oldIndex = heuristicMapping.at(item->getId()).second; + std::iter_swap(buckets[oldBucket].begin() + oldIndex, buckets[oldBucket].end() - 1); + // Set mapping for swapped item + heuristicMapping[buckets[oldBucket][oldIndex]->getId()] = std::make_pair(oldBucket, oldIndex); + } + buckets[oldBucket].pop_back(); + // Insert new element + buckets[newBucket].push_back(item); + if (newBucket == currentBucket) { + if (AUTOSORT) { + // Sort in first bucket + std::push_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + } else { + ++nrUnsortedItems; + } + } + // Set mapping + heuristicMapping[item->getId()] = std::make_pair(newBucket, buckets[newBucket].size() - 1); + } + } + + + template + void BucketPriorityQueue::pop() { + STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); + STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); + std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + // Remove from mapping + heuristicMapping.erase(buckets[currentBucket].back()->getId()); + buckets[currentBucket].pop_back(); + if (buckets[currentBucket].empty()) { + // Find next bucket with elements + for ( ; currentBucket < buckets.size(); ++currentBucket) { + if (!buckets[currentBucket].empty()) { + nrUnsortedItems = buckets[currentBucket].size(); + if (AUTOSORT) { + fix(); + } + break; + } + } + } + } + + template + typename BucketPriorityQueue::HeuristicPointer BucketPriorityQueue::popTop() { + HeuristicPointer item = top(); + pop(); + return item; + } + + template + size_t BucketPriorityQueue::getBucket(double priority) const { + STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low"); + size_t newBucket = (priority - lowerValue) / stepPerBucket; + if (HIGHER) { + newBucket = buckets.size()-1 - newBucket; + } + //std::cout << "get Bucket: " << priority << ", " << newBucket << ", " << ((priority - lowerValue) / stepPerBucket) << std::endl; + STORM_LOG_ASSERT(newBucket < buckets.size(), "Priority " << priority << " is too high"); + return newBucket; + } + + template + void BucketPriorityQueue::setMappingBucket(size_t bucket) { + if (bucket < buckets.size()) { + for (size_t index = 0; index < buckets[bucket].size(); ++index) { + heuristicMapping[buckets[bucket][index]->getId()] = std::make_pair(bucket, index); + } + } + } + + template + void BucketPriorityQueue::print(std::ostream& out) const { + out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and step per bucket: " << stepPerBucket << std::endl; + out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems << " unsorted items" << std::endl; + for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { + if (!buckets[bucket].empty()) { + out << "Bucket " << bucket << " (" << (HIGHER ? buckets.size() -1 - bucket * stepPerBucket : bucket * stepPerBucket) << "):" << std::endl; + for (HeuristicPointer heuristic : buckets[bucket]) { + out << "\t" << heuristic->getId() << ": " << heuristic->getPriority() << std::endl; + } + } + } + out << "Mapping:" << std::endl; + for (auto it : heuristicMapping) { + out << it.first << " -> " << it.second.first << ", " << it.second.second << std::endl; + } + } + + + // Template instantiations + template class BucketPriorityQueue; + +#ifdef STORM_HAVE_CARL + template class BucketPriorityQueue; +#endif + } +} diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h new file mode 100644 index 000000000..a08bfbd3b --- /dev/null +++ b/src/storage/BucketPriorityQueue.h @@ -0,0 +1,70 @@ +#ifndef STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ +#define STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ + +#include "src/builder/DftExplorationHeuristic.h" +#include +#include +#include +#include + +namespace storm { + namespace storage { + + template + class BucketPriorityQueue { + + using HeuristicPointer = std::shared_ptr>; + + public: + explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket); + + void fix(); + + bool empty() const; + + std::size_t size() const; + + HeuristicPointer const& top() const; + + void push(HeuristicPointer const& item); + + void update(HeuristicPointer const& item, double oldPriority); + + void pop(); + + HeuristicPointer popTop(); + + void print(std::ostream& out) const; + + private: + + size_t getBucket(double priority) const; + + void setMappingBucket(size_t bucket); + + // List of buckets + std::vector> buckets; + + // Index of first bucket which contains items + size_t currentBucket; + + // Mapping from id to (bucket, index in bucket) + std::unordered_map> heuristicMapping; + + std::function compare; + + double lowerValue; + + double stepPerBucket; + + size_t nrUnsortedItems; + + const bool HIGHER = true; + + const bool AUTOSORT = false; + }; + + } +} + +#endif // STORM_STORAGE_BUCKETPRIORITYQUEUE_H_ From ef7d4ac87b564cdc62096c96b658b29524924563 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 24 Oct 2016 17:29:14 +0200 Subject: [PATCH 09/28] Do not sort BEs anymore Former-commit-id: 1789ad3644a4dbbb3b58764831e4d5f5b0147aa2 --- src/storage/dft/DFTState.cpp | 14 +------------- src/storage/dft/DFTState.h | 5 ----- 2 files changed, 1 insertion(+), 18 deletions(-) diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 70ff18122..0b2ff7ee8 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -32,8 +32,6 @@ namespace storm { STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Id not found."); mCurrentlyNotFailableBE.erase(it); } - - sortFailableBEs(); } template @@ -69,8 +67,7 @@ namespace storm { STORM_LOG_TRACE("Spare " << index << " uses " << useId); } } - sortFailableBEs(); - + // Initialize failable dependencies for (size_t dependencyId : mDft.getDependencies()) { std::shared_ptr const> dependency = mDft.getDependency(dependencyId); @@ -324,7 +321,6 @@ namespace storm { propagateActivation(uses(elem)); } } - sortFailableBEs(); } template @@ -422,14 +418,6 @@ namespace storm { } return changed; } - - template - void DFTState::sortFailableBEs() { - std::sort(mCurrentlyFailableBE.begin( ), mCurrentlyFailableBE.end( ), [&](size_t const& lhs, size_t const& rhs) { - // Sort decreasing - return getBERate(rhs, true) < getBERate(lhs, true); - }); - } // Explicitly instantiate the class. diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 207eecac3..4ff36d1ab 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -313,11 +313,6 @@ namespace storm { */ ValueType getBERate(size_t id, bool considerPassive) const; - /*! - * Sort failable BEs in decreasing order of their active failure rate. - */ - void sortFailableBEs(); - }; } From 815bbf10abd7c5cdc2d30a476f0f8d7ab6a6c908 Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 24 Oct 2016 18:27:27 +0200 Subject: [PATCH 10/28] Remove map and use linear search in BucketPriorityQueue Former-commit-id: 3fc131facb4ad1a582ba3245292b5a3443343c35 --- src/storage/BucketPriorityQueue.cpp | 34 ++++++++--------------------- src/storage/BucketPriorityQueue.h | 5 ----- 2 files changed, 9 insertions(+), 30 deletions(-) diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp index e87e25506..bc3ca8780 100644 --- a/src/storage/BucketPriorityQueue.cpp +++ b/src/storage/BucketPriorityQueue.cpp @@ -32,7 +32,6 @@ namespace storm { for (size_t i = currentBucket; currentBucket < buckets.size(); ++i) { size += buckets[i].size(); } - STORM_LOG_ASSERT(size == heuristicMapping.size(), "Sizes to not coincide"); return size; } @@ -47,7 +46,6 @@ namespace storm { void BucketPriorityQueue::push(HeuristicPointer const& item) { size_t bucket = getBucket(item->getPriority()); if (bucket < currentBucket) { - setMappingBucket(currentBucket); currentBucket = bucket; nrUnsortedItems = 0; } @@ -60,8 +58,6 @@ namespace storm { ++nrUnsortedItems; } } - // Set mapping - heuristicMapping[item->getId()] = std::make_pair(bucket, buckets[bucket].size() - 1); } template @@ -84,16 +80,21 @@ namespace storm { // Move to new bucket STORM_LOG_ASSERT(newBucket < oldBucket, "Will update to higher bucket"); if (newBucket < currentBucket) { - setMappingBucket(currentBucket); currentBucket = newBucket; nrUnsortedItems = 0; } // Remove old entry by swap-and-pop if (buckets[oldBucket].size() >= 2) { - size_t oldIndex = heuristicMapping.at(item->getId()).second; + // Find old index by linear search + // Notice: using a map to rememeber index was not efficient + size_t oldIndex = 0; + for ( ; oldIndex < buckets[oldBucket].size(); ++oldIndex) { + if (buckets[oldBucket][oldIndex]->getId() == item->getId()) { + break; + } + } + STORM_LOG_ASSERT(oldIndex < buckets[oldBucket].size(), "Id " << item->getId() << " not found"); std::iter_swap(buckets[oldBucket].begin() + oldIndex, buckets[oldBucket].end() - 1); - // Set mapping for swapped item - heuristicMapping[buckets[oldBucket][oldIndex]->getId()] = std::make_pair(oldBucket, oldIndex); } buckets[oldBucket].pop_back(); // Insert new element @@ -106,8 +107,6 @@ namespace storm { ++nrUnsortedItems; } } - // Set mapping - heuristicMapping[item->getId()] = std::make_pair(newBucket, buckets[newBucket].size() - 1); } } @@ -117,8 +116,6 @@ namespace storm { STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); - // Remove from mapping - heuristicMapping.erase(buckets[currentBucket].back()->getId()); buckets[currentBucket].pop_back(); if (buckets[currentBucket].empty()) { // Find next bucket with elements @@ -153,15 +150,6 @@ namespace storm { return newBucket; } - template - void BucketPriorityQueue::setMappingBucket(size_t bucket) { - if (bucket < buckets.size()) { - for (size_t index = 0; index < buckets[bucket].size(); ++index) { - heuristicMapping[buckets[bucket][index]->getId()] = std::make_pair(bucket, index); - } - } - } - template void BucketPriorityQueue::print(std::ostream& out) const { out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and step per bucket: " << stepPerBucket << std::endl; @@ -174,10 +162,6 @@ namespace storm { } } } - out << "Mapping:" << std::endl; - for (auto it : heuristicMapping) { - out << it.first << " -> " << it.second.first << ", " << it.second.second << std::endl; - } } diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index a08bfbd3b..2e36e3cb6 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -40,17 +40,12 @@ namespace storm { size_t getBucket(double priority) const; - void setMappingBucket(size_t bucket); - // List of buckets std::vector> buckets; // Index of first bucket which contains items size_t currentBucket; - // Mapping from id to (bucket, index in bucket) - std::unordered_map> heuristicMapping; - std::function compare; double lowerValue; From 945447e7e01b176f8eab01e41ae961a1ed8e449e Mon Sep 17 00:00:00 2001 From: Mavo Date: Mon, 24 Oct 2016 18:41:07 +0200 Subject: [PATCH 11/28] Use DFS as default Former-commit-id: 34f9e80d1bd25c18085ca6f89beb5c163644ccdd --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 8 ++++---- src/builder/ExplicitDFTModelBuilderApprox.h | 2 +- src/storage/BucketPriorityQueue.cpp | 2 +- src/storage/BucketPriorityQueue.h | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 07863bb01..78272238c 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -32,12 +32,12 @@ namespace storm { matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), // TODO Matthias: make choosable - //explorationQueue(dft.nrElements(), 0, 1) - explorationQueue(41, 0, 1.0/20) + explorationQueue(dft.nrElements()+1, 0, 1) + //explorationQueue(141, 0, 0.02) { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::RATERATIO; + heuristic = storm::builder::ApproximationHeuristic::NONE; } template @@ -90,7 +90,7 @@ namespace storm { switch (heuristic) { case storm::builder::ApproximationHeuristic::NONE: // Do not change anything - approximationThreshold = 0; + approximationThreshold = dft.nrElements()+10; break; case storm::builder::ApproximationHeuristic::DEPTH: approximationThreshold = iteration; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index e23a8e819..1f779e44f 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicRateRatio; + using ExplorationHeuristic = DFTExplorationHeuristicDepth; using ExplorationHeuristicPointer = std::shared_ptr; diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp index bc3ca8780..fe1ca95b5 100644 --- a/src/storage/BucketPriorityQueue.cpp +++ b/src/storage/BucketPriorityQueue.cpp @@ -16,7 +16,7 @@ namespace storm { void BucketPriorityQueue::fix() { if (currentBucket < buckets.size() && nrUnsortedItems > 0) { // Fix current bucket - std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + //std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); nrUnsortedItems = 0; } } diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index 2e36e3cb6..3d3c2d35d 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket); From 8b78ed234068f118c45eb23fe45b74e614f7e4e9 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 25 Oct 2016 00:24:53 +0200 Subject: [PATCH 12/28] Renamed rateratio to probability Former-commit-id: 6d07985b1d63af7c94245926a8ac5dddb560cade --- src/builder/DftExplorationHeuristic.cpp | 25 ++++++---- src/builder/DftExplorationHeuristic.h | 46 +++++++++++++------ src/builder/ExplicitDFTModelBuilderApprox.cpp | 13 +++--- src/settings/modules/DFTSettings.cpp | 6 +-- 4 files changed, 57 insertions(+), 33 deletions(-) diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index dbd64088b..75556a06f 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -8,31 +8,36 @@ namespace storm { namespace builder { template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(depth) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(0), probability(storm::utility::zero()) { + // Intentionally left empty + } + + template + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(predecessor.depth + 1) { STORM_LOG_ASSERT(storm::utility::zero() < exitRate, "Exit rate is 0"); - rateRatio = rate/exitRate; + probability = predecessor.probability * rate/exitRate; } template<> - bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, double rate, double exitRate) { + bool DFTExplorationHeuristicProbability::updateHeuristicValues(DFTExplorationHeuristic const& predecessor, double rate, double exitRate) { STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0"); - rateRatio += rate/exitRate; + probability += predecessor.getProbability() * rate/exitRate; return true; } template<> - bool DFTExplorationHeuristicRateRatio::updateHeuristicValues(size_t depth, storm::RationalFunction rate, storm::RationalFunction exitRate) { + bool DFTExplorationHeuristicProbability::updateHeuristicValues(DFTExplorationHeuristic const& predecessor, storm::RationalFunction rate, storm::RationalFunction exitRate) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); return false; } template<> - double DFTExplorationHeuristicRateRatio::getPriority() const { - return rateRatio; + double DFTExplorationHeuristicProbability::getPriority() const { + return probability; } template<> - double DFTExplorationHeuristicRateRatio::getPriority() const { + double DFTExplorationHeuristicProbability::getPriority() const { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); } @@ -41,13 +46,13 @@ namespace storm { template class DFTExplorationHeuristic; template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; - template class DFTExplorationHeuristicRateRatio; + template class DFTExplorationHeuristicProbability; #ifdef STORM_HAVE_CARL template class DFTExplorationHeuristic; template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; - template class DFTExplorationHeuristicRateRatio; + template class DFTExplorationHeuristicProbability; #endif } } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index d23c673fc..f24d7defb 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -10,7 +10,7 @@ namespace storm { /*! * Enum representing the heuristic used for deciding which states to expand. */ - enum class ApproximationHeuristic { NONE, DEPTH, RATERATIO }; + enum class ApproximationHeuristic { NONE, DEPTH, PROBABILITY }; /*! @@ -20,9 +20,11 @@ namespace storm { class DFTExplorationHeuristic { public: - DFTExplorationHeuristic(size_t id, size_t depth, ValueType rate, ValueType exitRate); + DFTExplorationHeuristic(size_t id); - virtual bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) = 0; + DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate); + + virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0; virtual double getPriority() const = 0; @@ -40,21 +42,29 @@ namespace storm { return depth; } + ValueType getProbability() const { + return probability; + } + protected: size_t id; bool expand; size_t depth; - ValueType rateRatio; + ValueType probability; }; template class DFTExplorationHeuristicNone : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicNone(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { + DFTExplorationHeuristicNone(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } - bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override { + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override { return false; } @@ -74,13 +84,17 @@ namespace storm { template class DFTExplorationHeuristicDepth : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicDepth(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { + DFTExplorationHeuristicDepth(size_t id) : DFTExplorationHeuristic(id) { // Intentionally left empty } - bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override { - if (depth < this->depth) { - this->depth = depth; + DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + // Intentionally left empty + } + + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override { + if (predecessor.getDepth() < this->depth) { + this->depth = predecessor.getDepth(); return true; } return false; @@ -101,13 +115,17 @@ namespace storm { }; template - class DFTExplorationHeuristicRateRatio : public DFTExplorationHeuristic { + class DFTExplorationHeuristicProbability : public DFTExplorationHeuristic { public: - DFTExplorationHeuristicRateRatio(size_t id, size_t depth, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, depth, rate, exitRate) { + DFTExplorationHeuristicProbability(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } - bool updateHeuristicValues(size_t depth, ValueType rate, ValueType exitRate) override; + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override; double getPriority() const override; @@ -115,7 +133,7 @@ namespace storm { return !this->expand && this->getPriority() < approximationThreshold; } - bool operator<(DFTExplorationHeuristicRateRatio const& other) const { + bool operator<(DFTExplorationHeuristicProbability const& other) const { return this->getPriority() < other.getPriority(); } }; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 78272238c..6b35344cd 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -37,7 +37,7 @@ namespace storm { { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::NONE; + heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; } template @@ -79,7 +79,7 @@ namespace storm { STORM_LOG_TRACE("Initial state: " << initialStateIndex); // Initialize heuristic values for inital state STORM_LOG_ASSERT(!statesNotExplored.at(initialStateIndex).second, "Heuristic for initial state is already initialized"); - ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex, 0, storm::utility::zero(), storm::utility::one()); + ExplorationHeuristicPointer heuristic = std::make_shared(initialStateIndex); heuristic->markExpand(); statesNotExplored[initialStateIndex].second = heuristic; explorationQueue.push(heuristic); @@ -95,8 +95,9 @@ namespace storm { case storm::builder::ApproximationHeuristic::DEPTH: approximationThreshold = iteration; break; - case storm::builder::ApproximationHeuristic::RATERATIO: - approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; + case storm::builder::ApproximationHeuristic::PROBABILITY: + //approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; + approximationThreshold = 10 * std::pow(2, iteration); break; } exploreStateSpace(approximationThreshold); @@ -298,12 +299,12 @@ namespace storm { DFTStatePointer state = iter->second.first; if (!iter->second.second) { // Initialize heuristic values - ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass()); + ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); iter->second.second = heuristic; explorationQueue.push(heuristic); } else { double oldPriority = iter->second.second->getPriority(); - if (iter->second.second->updateHeuristicValues(currentExplorationHeuristic->getDepth() + 1, stateProbabilityPair.second, choice.getTotalMass())) { + if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) { // Update priority queue ++fix; explorationQueue.update(iter->second.second, oldPriority); diff --git a/src/settings/modules/DFTSettings.cpp b/src/settings/modules/DFTSettings.cpp index 0dcb49f1d..ab707b5a4 100644 --- a/src/settings/modules/DFTSettings.cpp +++ b/src/settings/modules/DFTSettings.cpp @@ -40,7 +40,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorIncluding(0.0)).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, rateratio}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator({"depth", "rateratio"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleGreaterValidatorExcluding(0.0)).build()).build()); @@ -87,8 +87,8 @@ namespace storm { std::string heuristicAsString = this->getOption(approximationHeuristicOptionName).getArgumentByName("heuristic").getValueAsString(); if (heuristicAsString == "depth") { return storm::builder::ApproximationHeuristic::DEPTH; - } else if (heuristicAsString == "rateratio") { - return storm::builder::ApproximationHeuristic::RATERATIO; + } else if (heuristicAsString == "probability") { + return storm::builder::ApproximationHeuristic::PROBABILITY; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); } From 20b00e8f1dcff6e72df2c6011b5b4622f7046870 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 25 Oct 2016 00:25:35 +0200 Subject: [PATCH 13/28] Propagate dont care to currently not failable BEs Former-commit-id: 1fcb15f4ec045d244e1397b4fbe2100435ea9557 --- src/storage/dft/DFTState.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 0b2ff7ee8..369bed3f7 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -200,8 +200,13 @@ namespace storm { template void DFTState::beNoLongerFailable(size_t id) { auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id); - if(it != mCurrentlyFailableBE.end()) { + if (it != mCurrentlyFailableBE.end()) { mCurrentlyFailableBE.erase(it); + } else { + it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id); + if (it != mCurrentlyNotFailableBE.end()) { + mCurrentlyNotFailableBE.erase(it); + } } } @@ -253,7 +258,7 @@ namespace storm { ValueType DFTState::getNotFailableBERate(size_t index) const { STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid."); STORM_LOG_ASSERT(storm::utility::isZero(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) || - (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail"); + (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail in state: " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); // Use active failure rate as passive failure rate is 0. return getBERate(mCurrentlyNotFailableBE[index], false); } From 0d9cdd6ef882fbe21b5db8e9b1ee6d85a02bd767 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 25 Oct 2016 13:47:06 +0200 Subject: [PATCH 14/28] Use Heuristic None Former-commit-id: 63f78f3db06074f322326d9169deed15256b8304 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 6b35344cd..7de1e0bb4 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -33,11 +33,11 @@ namespace storm { stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), // TODO Matthias: make choosable explorationQueue(dft.nrElements()+1, 0, 1) - //explorationQueue(141, 0, 0.02) + //explorationQueue(1001, 0, 0.001) { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; + heuristic = storm::builder::ApproximationHeuristic::NONE; } template @@ -97,7 +97,7 @@ namespace storm { break; case storm::builder::ApproximationHeuristic::PROBABILITY: //approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; - approximationThreshold = 10 * std::pow(2, iteration); + approximationThreshold = iteration;//10 * std::pow(2, iteration); break; } exploreStateSpace(approximationThreshold); @@ -267,6 +267,7 @@ namespace storm { // Try to explore the next state generator.load(currentState); + //if (nrExpandedStates > approximationThreshold) { if (currentExplorationHeuristic->isSkip(approximationThreshold)) { // Skip the current state ++nrSkippedStates; From 58f870729307fb4df9612b292187ea711403a589 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 25 Oct 2016 23:19:41 +0200 Subject: [PATCH 15/28] Tighter over-approximation Former-commit-id: 824e74f88df07a49ab306b2599fd82f9ced47366 --- src/builder/DftExplorationHeuristic.cpp | 21 ++- src/builder/DftExplorationHeuristic.h | 55 +++++++- src/builder/ExplicitDFTModelBuilderApprox.cpp | 124 +++++++++++------- src/builder/ExplicitDFTModelBuilderApprox.h | 22 +++- src/modelchecker/dft/DFTModelChecker.cpp | 1 + src/storage/BucketPriorityQueue.cpp | 23 +++- src/storage/BucketPriorityQueue.h | 5 +- src/storage/dft/DFTState.cpp | 8 +- 8 files changed, 196 insertions(+), 63 deletions(-) diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index 75556a06f..db26fc60d 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -8,16 +8,22 @@ namespace storm { namespace builder { template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), depth(0), probability(storm::utility::zero()) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { // Intentionally left empty } template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), depth(predecessor.depth + 1) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : id(id), expand(false), lowerBound(lowerBound), upperBound(upperBound), depth(predecessor.depth + 1) { STORM_LOG_ASSERT(storm::utility::zero() < exitRate, "Exit rate is 0"); probability = predecessor.probability * rate/exitRate; } + template + void DFTExplorationHeuristic::setBounds(ValueType lowerBound, ValueType upperBound) { + this->lowerBound = lowerBound; + this->upperBound = upperBound; + } + template<> bool DFTExplorationHeuristicProbability::updateHeuristicValues(DFTExplorationHeuristic const& predecessor, double rate, double exitRate) { STORM_LOG_ASSERT(exitRate > 0, "Exit rate is 0"); @@ -41,18 +47,29 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic rate ration does not work for rational functions."); } + template<> + double DFTExplorationHeuristicBoundDifference::getPriority() const { + return upperBound / lowerBound; + } + + template<> + double DFTExplorationHeuristicBoundDifference::getPriority() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Heuristic bound difference does not work for rational functions."); + } // Instantiate templates. template class DFTExplorationHeuristic; template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; template class DFTExplorationHeuristicProbability; + template class DFTExplorationHeuristicBoundDifference; #ifdef STORM_HAVE_CARL template class DFTExplorationHeuristic; template class DFTExplorationHeuristicNone; template class DFTExplorationHeuristicDepth; template class DFTExplorationHeuristicProbability; + template class DFTExplorationHeuristicBoundDifference; #endif } } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index f24d7defb..12f178f25 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -22,7 +22,9 @@ namespace storm { public: DFTExplorationHeuristic(size_t id); - DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate); + DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound); + + void setBounds(ValueType lowerBound, ValueType upperBound); virtual bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) = 0; @@ -38,6 +40,10 @@ namespace storm { return id; } + bool isExpand() { + return expand; + } + size_t getDepth() const { return depth; } @@ -46,9 +52,19 @@ namespace storm { return probability; } + ValueType getLowerBound() const { + return lowerBound; + } + + ValueType getUpperBound() const { + return upperBound; + } + protected: size_t id; bool expand; + ValueType lowerBound; + ValueType upperBound; size_t depth; ValueType probability; }; @@ -60,7 +76,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { // Intentionally left empty } @@ -88,7 +104,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { // Intentionally left empty } @@ -121,7 +137,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { + DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { // Intentionally left empty } @@ -138,6 +154,37 @@ namespace storm { } }; + template + class DFTExplorationHeuristicBoundDifference : public DFTExplorationHeuristic { + public: + DFTExplorationHeuristicBoundDifference(size_t id) : DFTExplorationHeuristic(id) { + // Intentionally left empty + } + + DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + // Intentionally left empty + } + + bool updateHeuristicValues(DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) override { + return false; + } + + double getPriority() const override; + + bool isSkip(double approximationThreshold) const override { + return !this->expand && this->getPriority() < approximationThreshold; + } + + bool operator<(DFTExplorationHeuristicBoundDifference const& other) const { + return this->getPriority() < other.getPriority(); + } + + private: + ValueType lowerBound; + ValueType upperBound; + }; + + } } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 7de1e0bb4..0328cf055 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -3,6 +3,7 @@ #include #include #include +#include "src/utility/bitoperations.h" #include #include "src/settings/modules/DFTSettings.h" #include "src/settings/SettingsManager.h" @@ -32,12 +33,12 @@ namespace storm { matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), // TODO Matthias: make choosable - explorationQueue(dft.nrElements()+1, 0, 1) - //explorationQueue(1001, 0, 0.001) + //explorationQueue(dft.nrElements()+1, 0, 1) + explorationQueue(1001, 0, 0.001) { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::NONE; + heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; } template @@ -256,6 +257,9 @@ namespace storm { if (currentState->isPseudoState()) { // Create concrete state from pseudo state currentState->construct(); + ValueType lowerBound = getLowerBound(currentState); + ValueType upperBound = getUpperBound(currentState); + currentExplorationHeuristic->setBounds(lowerBound, upperBound); } STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); @@ -267,8 +271,8 @@ namespace storm { // Try to explore the next state generator.load(currentState); - //if (nrExpandedStates > approximationThreshold) { - if (currentExplorationHeuristic->isSkip(approximationThreshold)) { + if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { + //if (currentExplorationHeuristic->isSkip(approximationThreshold)) { // Skip the current state ++nrSkippedStates; STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); @@ -299,11 +303,24 @@ namespace storm { // Update heuristic values DFTStatePointer state = iter->second.first; if (!iter->second.second) { + ValueType lowerBound; + ValueType upperBound; + if (state->isPseudoState()) { + lowerBound = storm::utility::infinity(); + upperBound = storm::utility::infinity(); + } else { + lowerBound = getLowerBound(state); + upperBound = getUpperBound(state); + } // Initialize heuristic values - ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); + ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass(), lowerBound, upperBound); iter->second.second = heuristic; + 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(); + } explorationQueue.push(heuristic); - } else { + } else if (!iter->second.second->isExpand()) { double oldPriority = iter->second.second->getPriority(); if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) { // Update priority queue @@ -311,11 +328,6 @@ namespace storm { explorationQueue.update(iter->second.second, oldPriority); } } - 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(); - // TODO Matthias give highest priority to ensure expanding before all skipped - } } } matrixBuilder.finishRow(); @@ -383,11 +395,7 @@ namespace storm { template std::shared_ptr> ExplicitDFTModelBuilderApprox::getModelApproximation(bool lowerBound) { // TODO Matthias: handle case with no skipped states - if (lowerBound) { - changeMatrixLowerBound(modelComponents.transitionMatrix); - } else { - changeMatrixUpperBound(modelComponents.transitionMatrix); - } + changeMatrixBound(modelComponents.transitionMatrix, lowerBound); return createModel(true); } @@ -443,44 +451,72 @@ namespace storm { } template - void ExplicitDFTModelBuilderApprox::changeMatrixLowerBound(storm::storage::SparseMatrix & matrix) const { + void ExplicitDFTModelBuilderApprox::changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const { // Set lower bound for skipped states for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { 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 < state->nrFailableBEs(); ++index) { - newRate += state->getFailableBERate(index); - } - for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { - newRate += state->getNotFailableBERate(index); + STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); + if (lowerBound) { + matrixEntry->setValue(it->second.second->getLowerBound()); + } else { + matrixEntry->setValue(it->second.second->getUpperBound()); } - matrixEntry->setValue(newRate); } } template - void ExplicitDFTModelBuilderApprox::changeMatrixUpperBound(storm::storage::SparseMatrix & matrix) const { - // Set uppper bound for skipped states - for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { - auto matrixEntry = matrix.getRow(it->first, 0).begin(); - STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); - // 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 < state->nrFailableBEs(); ++index) { - newRate += storm::utility::one() / state->getFailableBERate(index); - } - for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { - newRate += storm::utility::one() / state->getNotFailableBERate(index); + ValueType ExplicitDFTModelBuilderApprox::getLowerBound(DFTStatePointer const& state) const { + // Get the lower bound by considering the failure of all possible BEs + ValueType lowerBound = storm::utility::zero(); + for (size_t index = 0; index < state->nrFailableBEs(); ++index) { + lowerBound += state->getFailableBERate(index); + } + for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { + lowerBound += state->getNotFailableBERate(index); + } + return lowerBound; + } + + template + ValueType ExplicitDFTModelBuilderApprox::getUpperBound(DFTStatePointer const& state) const { + // 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 + ValueType upperBound = storm::utility::zero(); + + // Get all possible rates + std::vector rates(state->nrFailableBEs() + state->nrNotFailableBEs()); + for (size_t index = 0; index < state->nrFailableBEs(); ++index) { + rates[index] = state->getFailableBERate(index); + } + for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { + rates[index + state->nrFailableBEs()] = state->getNotFailableBERate(index); + } + + // TODO Matthias: works only for <64 BEs! + for (size_t i = 1; i < 4 && i <= rates.size(); ++i) { + size_t permutation = smallestIntWithNBitsSet(static_cast(i)); + ValueType sum = storm::utility::zero(); + do { + ValueType permResult = storm::utility::zero(); + for(size_t j = 0; j < rates.size(); ++j) { + if(permutation & (1 << j)) { + permResult += rates[j]; + } + } + permutation = nextBitPermutation(permutation); + STORM_LOG_ASSERT(!storm::utility::isZero(permResult), "PermResult is 0"); + sum += storm::utility::one() / permResult; + } while(permutation < (1 << rates.size()) && permutation != 0); + if (i % 2 == 0) { + upperBound -= sum; + } else { + upperBound += sum; } - newRate = storm::utility::one() / newRate; - matrixEntry->setValue(newRate); } + STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "UpperBound is 0"); + return storm::utility::one() / upperBound; } template diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 1f779e44f..446bed6ad 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicDepth; + using ExplorationHeuristic = DFTExplorationHeuristicProbability; using ExplorationHeuristicPointer = std::shared_ptr; @@ -217,18 +217,26 @@ namespace storm { void setMarkovian(bool markovian); /** - * Change matrix to reflect the lower approximation bound. + * Change matrix to reflect the lower or upper approximation bound. * - * @param matrix Matrix to change. The change are reflected here. + * @param matrix Matrix to change. The change are reflected here. + * @param lowerBound Flag indicating if the lower bound should be used. Otherwise the upper bound is used. */ - void changeMatrixLowerBound(storm::storage::SparseMatrix & matrix) const; + void changeMatrixBound(storm::storage::SparseMatrix & matrix, bool lowerBound) const; /*! - * Change matrix to reflect the upper approximation bound. + * Get lower bound approximation for state. * - * @param matrix Matrix to change. The change are reflected here. + * @return Lower bound approximation. */ - void changeMatrixUpperBound(storm::storage::SparseMatrix & matrix) const; + ValueType getLowerBound(DFTStatePointer const& state) const; + + /*! + * Get upper bound approximation for state. + * + * @return Upper bound approximation. + */ + ValueType getUpperBound(DFTStatePointer const& state) const; /*! * Compares the priority of two states. diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index f19943f2f..59d85f5c2 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -255,6 +255,7 @@ namespace storm { template<> bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError) { + STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN."); return upperBound - lowerBound <= approximationError * (lowerBound + upperBound) / 2; } diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp index fe1ca95b5..eb174cce0 100644 --- a/src/storage/BucketPriorityQueue.cpp +++ b/src/storage/BucketPriorityQueue.cpp @@ -16,19 +16,19 @@ namespace storm { void BucketPriorityQueue::fix() { if (currentBucket < buckets.size() && nrUnsortedItems > 0) { // Fix current bucket - //std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); + std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); nrUnsortedItems = 0; } } template bool BucketPriorityQueue::empty() const { - return currentBucket == buckets.size(); + return currentBucket == buckets.size() && immediateBucket.empty(); } template std::size_t BucketPriorityQueue::size() const { - size_t size = 0; + size_t size = immediateBucket.size(); for (size_t i = currentBucket; currentBucket < buckets.size(); ++i) { size += buckets[i].size(); } @@ -37,6 +37,9 @@ namespace storm { template typename BucketPriorityQueue::HeuristicPointer const& BucketPriorityQueue::top() const { + if (!immediateBucket.empty()) { + return immediateBucket.back(); + } STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); return buckets[currentBucket].front(); @@ -44,6 +47,10 @@ namespace storm { template void BucketPriorityQueue::push(HeuristicPointer const& item) { + if (item->isExpand()) { + immediateBucket.push_back(item); + return; + } size_t bucket = getBucket(item->getPriority()); if (bucket < currentBucket) { currentBucket = bucket; @@ -62,6 +69,7 @@ namespace storm { template void BucketPriorityQueue::update(HeuristicPointer const& item, double oldPriority) { + STORM_LOG_ASSERT(!item->isExpand(), "Item is marked for expansion"); size_t newBucket = getBucket(item->getPriority()); size_t oldBucket = getBucket(oldPriority); @@ -113,6 +121,10 @@ namespace storm { template void BucketPriorityQueue::pop() { + if (!immediateBucket.empty()) { + immediateBucket.pop_back(); + return; + } STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); @@ -153,6 +165,11 @@ namespace storm { template void BucketPriorityQueue::print(std::ostream& out) const { out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and step per bucket: " << stepPerBucket << std::endl; + out << "Immediate bucket: "; + for (HeuristicPointer heuristic : immediateBucket) { + out << heuristic->getId() << ", "; + } + out << std::endl; out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems << " unsorted items" << std::endl; for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { if (!buckets[bucket].empty()) { diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index 3d3c2d35d..253b34e19 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket); @@ -43,6 +43,9 @@ namespace storm { // List of buckets std::vector> buckets; + // Bucket containing all items which should be considered immediately + std::vector immediateBucket; + // Index of first bucket which contains items size_t currentBucket; diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 369bed3f7..b9381598f 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -18,7 +18,9 @@ namespace storm { } for (auto elem : mDft.getBasicElements()) { - mCurrentlyNotFailableBE.push_back(elem->id()); + if (!storm::utility::isZero(elem->activeFailureRate())) { + mCurrentlyNotFailableBE.push_back(elem->id()); + } } // Initialize activation @@ -242,8 +244,10 @@ namespace storm { ValueType DFTState::getBERate(size_t id, bool considerPassive) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); if (considerPassive && mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { + STORM_LOG_ASSERT(!storm::utility::isZero(mDft.getBasicElement(id)->passiveFailureRate()), "Failure rate of BE " << mDft.getBasicElement(id)->id() << " is 0 in state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); return mDft.getBasicElement(id)->passiveFailureRate(); } else { + STORM_LOG_ASSERT(!storm::utility::isZero(mDft.getBasicElement(id)->activeFailureRate()), "Failure rate of BE " << mDft.getBasicElement(id)->id() << " is 0 in state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); return mDft.getBasicElement(id)->activeFailureRate(); } } @@ -257,7 +261,7 @@ namespace storm { template ValueType DFTState::getNotFailableBERate(size_t index) const { STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid."); - STORM_LOG_ASSERT(storm::utility::isZero(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) || + STORM_LOG_ASSERT(isPseudoState() || storm::utility::isZero(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) || (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail in state: " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); // Use active failure rate as passive failure rate is 0. return getBERate(mCurrentlyNotFailableBE[index], false); From a9f97bd210418cf8afb999e362af118d2c92fc30 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 25 Oct 2016 23:28:35 +0200 Subject: [PATCH 16/28] Set heuristic to probability Former-commit-id: a7d8fd77385ce805b2161b8d0b655240b9319f90 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 0328cf055..6a6474ad8 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -97,8 +97,7 @@ namespace storm { approximationThreshold = iteration; break; case storm::builder::ApproximationHeuristic::PROBABILITY: - //approximationThreshold = std::pow(0.1, iteration) * approximationThreshold; - approximationThreshold = iteration;//10 * std::pow(2, iteration); + approximationThreshold = 10 * std::pow(2, iteration); break; } exploreStateSpace(approximationThreshold); @@ -234,7 +233,6 @@ namespace storm { void ExplicitDFTModelBuilderApprox::exploreStateSpace(double approximationThreshold) { size_t nrExpandedStates = 0; size_t nrSkippedStates = 0; - size_t fix = 0; // TODO Matthias: do not empty queue every time but break before while (!explorationQueue.empty()) { explorationQueue.fix(); @@ -324,7 +322,6 @@ namespace storm { double oldPriority = iter->second.second->getPriority(); if (iter->second.second->updateHeuristicValues(*currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass())) { // Update priority queue - ++fix; explorationQueue.update(iter->second.second, oldPriority); } } @@ -334,7 +331,6 @@ namespace storm { } } } // end exploration - std::cout << "Fixed queue " << fix << " times" << std::endl; STORM_LOG_INFO("Expanded " << nrExpandedStates << " states"); STORM_LOG_INFO("Skipped " << nrSkippedStates << " states"); From 8e159133da0617fd8c88e20196e83d6f37b29a21 Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 26 Oct 2016 23:10:57 +0200 Subject: [PATCH 17/28] Compute lower/upper bounds only when needed Former-commit-id: 8f3af1ab100516000aba505fbe3620c5875d7f8f --- src/builder/DftExplorationHeuristic.cpp | 4 +-- src/builder/DftExplorationHeuristic.h | 12 ++++----- src/builder/ExplicitDFTModelBuilderApprox.cpp | 25 +++++++++---------- 3 files changed, 20 insertions(+), 21 deletions(-) diff --git a/src/builder/DftExplorationHeuristic.cpp b/src/builder/DftExplorationHeuristic.cpp index db26fc60d..40d00115f 100644 --- a/src/builder/DftExplorationHeuristic.cpp +++ b/src/builder/DftExplorationHeuristic.cpp @@ -8,12 +8,12 @@ namespace storm { namespace builder { template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(false), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id) : id(id), expand(true), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { // Intentionally left empty } template - DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : id(id), expand(false), lowerBound(lowerBound), upperBound(upperBound), depth(predecessor.depth + 1) { + DFTExplorationHeuristic::DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate) : id(id), expand(false), lowerBound(storm::utility::zero()), upperBound(storm::utility::zero()), depth(predecessor.depth + 1) { STORM_LOG_ASSERT(storm::utility::zero() < exitRate, "Exit rate is 0"); probability = predecessor.probability * rate/exitRate; } diff --git a/src/builder/DftExplorationHeuristic.h b/src/builder/DftExplorationHeuristic.h index 12f178f25..8feb0fefa 100644 --- a/src/builder/DftExplorationHeuristic.h +++ b/src/builder/DftExplorationHeuristic.h @@ -22,7 +22,7 @@ namespace storm { public: DFTExplorationHeuristic(size_t id); - DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound); + DFTExplorationHeuristic(size_t id, DFTExplorationHeuristic const& predecessor, ValueType rate, ValueType exitRate); void setBounds(ValueType lowerBound, ValueType upperBound); @@ -76,7 +76,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicNone(size_t id, DFTExplorationHeuristicNone const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -85,7 +85,7 @@ namespace storm { } double getPriority() const override { - return this->id; + return 0; } bool isSkip(double approximationThreshold) const override { @@ -104,7 +104,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicDepth(size_t id, DFTExplorationHeuristicDepth const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -137,7 +137,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicProbability(size_t id, DFTExplorationHeuristicProbability const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } @@ -161,7 +161,7 @@ namespace storm { // Intentionally left empty } - DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference const& predecessor, ValueType rate, ValueType exitRate, ValueType lowerBound, ValueType upperBound) : DFTExplorationHeuristic(id, predecessor, rate, exitRate, lowerBound, upperBound) { + DFTExplorationHeuristicBoundDifference(size_t id, DFTExplorationHeuristicBoundDifference const& predecessor, ValueType rate, ValueType exitRate) : DFTExplorationHeuristic(id, predecessor, rate, exitRate) { // Intentionally left empty } diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 6a6474ad8..432636161 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -255,9 +255,6 @@ namespace storm { if (currentState->isPseudoState()) { // Create concrete state from pseudo state currentState->construct(); - ValueType lowerBound = getLowerBound(currentState); - ValueType upperBound = getUpperBound(currentState); - currentExplorationHeuristic->setBounds(lowerBound, upperBound); } STORM_LOG_ASSERT(!currentState->isPseudoState(), "State is pseudo state."); @@ -301,17 +298,8 @@ namespace storm { // Update heuristic values DFTStatePointer state = iter->second.first; if (!iter->second.second) { - ValueType lowerBound; - ValueType upperBound; - if (state->isPseudoState()) { - lowerBound = storm::utility::infinity(); - upperBound = storm::utility::infinity(); - } else { - lowerBound = getLowerBound(state); - upperBound = getUpperBound(state); - } // Initialize heuristic values - ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass(), lowerBound, upperBound); + ExplorationHeuristicPointer heuristic = std::make_shared(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); iter->second.second = heuristic; 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 @@ -453,6 +441,16 @@ namespace storm { auto matrixEntry = matrix.getRow(it->first, 0).begin(); STORM_LOG_ASSERT(matrixEntry->getColumn() == failedStateId, "Transition has wrong target state."); STORM_LOG_ASSERT(!it->second.first->isPseudoState(), "State is still pseudo state."); + + ExplorationHeuristicPointer heuristic = it->second.second; + if (storm::utility::isZero(heuristic->getUpperBound())) { + // Initialize bounds + ValueType lowerBound = getLowerBound(it->second.first); + ValueType upperBound = getUpperBound(it->second.first); + heuristic->setBounds(lowerBound, upperBound); + } + + // Change bound if (lowerBound) { matrixEntry->setValue(it->second.second->getLowerBound()); } else { @@ -489,6 +487,7 @@ namespace storm { for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { rates[index + state->nrFailableBEs()] = state->getNotFailableBERate(index); } + STORM_LOG_ASSERT(rates.size() > 0, "State is absorbing"); // TODO Matthias: works only for <64 BEs! for (size_t i = 1; i < 4 && i <= rates.size(); ++i) { From 386d4c7f056b3ce475c76f574bf0f56c49d8f75f Mon Sep 17 00:00:00 2001 From: Mavo Date: Wed, 26 Oct 2016 23:14:21 +0200 Subject: [PATCH 18/28] Use heuristic NONE to explore complete state space Former-commit-id: 25990b5ddaa23c00702940d75ac03879df11aeae --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 10 +++++----- src/builder/ExplicitDFTModelBuilderApprox.h | 2 +- src/storage/BucketPriorityQueue.h | 2 +- src/storage/dft/DFTState.cpp | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 432636161..5a3e65585 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -33,12 +33,12 @@ namespace storm { matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), // TODO Matthias: make choosable - //explorationQueue(dft.nrElements()+1, 0, 1) - explorationQueue(1001, 0, 0.001) + explorationQueue(dft.nrElements()+1, 0, 1) + //explorationQueue(1001, 0, 0.001) { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; + heuristic = storm::builder::ApproximationHeuristic::NONE; } template @@ -266,8 +266,8 @@ namespace storm { // Try to explore the next state generator.load(currentState); - if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { - //if (currentExplorationHeuristic->isSkip(approximationThreshold)) { + //if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { + if (currentExplorationHeuristic->isSkip(approximationThreshold)) { // Skip the current state ++nrSkippedStates; STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 446bed6ad..c3ffe4467 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicProbability; + using ExplorationHeuristic = DFTExplorationHeuristicNone; using ExplorationHeuristicPointer = std::shared_ptr; diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index 253b34e19..1aa18689d 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket); diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index b9381598f..aaad9367f 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -323,7 +323,7 @@ namespace storm { mCurrentlyFailableBE.push_back(elem); // Remove from not failable BEs auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem); - STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element not found."); + STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << elem << " not found."); mCurrentlyNotFailableBE.erase(it); } } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { From d9b1285644ea8c5f97b194537ea259533cb9c526 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 27 Oct 2016 16:54:12 +0200 Subject: [PATCH 19/28] Alternative way of computing permutations (at the moment in parallel) Former-commit-id: f5886860bcf2854e1322fc780c113b530cec5094 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 5a3e65585..3be21bfb4 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -510,6 +510,25 @@ namespace storm { upperBound += sum; } } + + // Compute upper bound with permutations of size <= 3 + ValueType upperBound2 = storm::utility::zero(); + for (size_t i1 = 0; i1 < rates.size(); ++i1) { + // + 1/a + ValueType sum = rates[i1]; + upperBound2 += storm::utility::one() / sum; + for (size_t i2 = 0; i2 < i1; ++i2) { + // - 1/(a+b) + ValueType sum2 = sum + rates[i2]; + upperBound2 -= storm::utility::one() / sum2; + for (size_t i3 = 0; i3 < i2; ++i3) { + // + 1/(a+b+c) + upperBound2 += storm::utility::one() / (sum2 + rates[i3]); + } + } + } + STORM_LOG_ASSERT(upperBound == upperBound2, "Upperbounds are different: " << upperBound << " and " << upperBound2); + STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "UpperBound is 0"); return storm::utility::one() / upperBound; } From 876b147aa8a5123ffa1d8b4e86b3935d110479aa Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 27 Oct 2016 16:55:50 +0200 Subject: [PATCH 20/28] Fixed bug with iterator Former-commit-id: f7248a57c175d5ee47d5929fd739187c59507118 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 5a3e65585..ac61efc0f 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -153,7 +153,8 @@ namespace storm { auto iterSkipped = skippedStates.begin(); size_t skippedBefore = 0; for (size_t i = 0; i < indexRemapping.size(); ++i) { - while (iterSkipped->first <= i) { + while (iterSkipped != skippedStates.end() && iterSkipped->first <= i) { + STORM_LOG_ASSERT(iterSkipped->first < indexRemapping.size(), "Skipped is too high."); ++skippedBefore; ++iterSkipped; } From c12bbe29045202b3caa2108e6a46d1b3d4aca65b Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 27 Oct 2016 18:57:26 +0200 Subject: [PATCH 21/28] Disable old way of computing permutations as there is a bug for >31 elements Former-commit-id: ae7af404f3ab73f03463c6e5d1776bab229379b3 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 22 +++++++++---------- src/modelchecker/dft/DFTModelChecker.cpp | 2 ++ src/utility/bitoperations.h | 2 +- 3 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 3be21bfb4..1991cec95 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -475,8 +475,7 @@ namespace storm { template ValueType ExplicitDFTModelBuilderApprox::getUpperBound(DFTStatePointer const& state) const { // 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 + // The used formula for the rate is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...) ValueType upperBound = storm::utility::zero(); // Get all possible rates @@ -490,44 +489,45 @@ namespace storm { STORM_LOG_ASSERT(rates.size() > 0, "State is absorbing"); // TODO Matthias: works only for <64 BEs! - for (size_t i = 1; i < 4 && i <= rates.size(); ++i) { + // WARNING: this code produces wrong results for more than 32 BEs + /*for (size_t i = 1; i < 4 && i <= rates.size(); ++i) { size_t permutation = smallestIntWithNBitsSet(static_cast(i)); ValueType sum = storm::utility::zero(); do { ValueType permResult = storm::utility::zero(); for(size_t j = 0; j < rates.size(); ++j) { - if(permutation & (1 << j)) { + if(permutation & static_cast(1 << static_cast(j))) { + // WARNING: if the first bit is set, it also recognizes the 32nd bit as set + // TODO: fix permResult += rates[j]; } } permutation = nextBitPermutation(permutation); STORM_LOG_ASSERT(!storm::utility::isZero(permResult), "PermResult is 0"); sum += storm::utility::one() / permResult; - } while(permutation < (1 << rates.size()) && permutation != 0); + } while(permutation < (static_cast(1) << rates.size()) && permutation != 0); if (i % 2 == 0) { upperBound -= sum; } else { upperBound += sum; } - } + }*/ // Compute upper bound with permutations of size <= 3 - ValueType upperBound2 = storm::utility::zero(); for (size_t i1 = 0; i1 < rates.size(); ++i1) { // + 1/a ValueType sum = rates[i1]; - upperBound2 += storm::utility::one() / sum; + upperBound += storm::utility::one() / sum; for (size_t i2 = 0; i2 < i1; ++i2) { // - 1/(a+b) ValueType sum2 = sum + rates[i2]; - upperBound2 -= storm::utility::one() / sum2; + upperBound -= storm::utility::one() / sum2; for (size_t i3 = 0; i3 < i2; ++i3) { // + 1/(a+b+c) - upperBound2 += storm::utility::one() / (sum2 + rates[i3]); + upperBound += storm::utility::one() / (sum2 + rates[i3]); } } } - STORM_LOG_ASSERT(upperBound == upperBound2, "Upperbounds are different: " << upperBound << " and " << upperBound2); STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "UpperBound is 0"); return storm::utility::one() / upperBound; diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index 59d85f5c2..ff2148982 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -100,6 +100,8 @@ namespace storm { ValueType result = storm::utility::zero(); int limK = invResults ? -1 : nrM+1; int chK = invResults ? -1 : 1; + // WARNING: there is a bug for computing permutations with more than 32 elements + STORM_LOG_ASSERT(res.size() < 32, "Permutations work only for < 32 elements"); for(int cK = nrK; cK != limK; cK += chK ) { STORM_LOG_ASSERT(cK >= 0, "ck negative."); size_t permutation = smallestIntWithNBitsSet(static_cast(cK)); diff --git a/src/utility/bitoperations.h b/src/utility/bitoperations.h index bec6a6414..18b42a1cd 100644 --- a/src/utility/bitoperations.h +++ b/src/utility/bitoperations.h @@ -10,6 +10,6 @@ inline size_t smallestIntWithNBitsSet(size_t n) { inline size_t nextBitPermutation(size_t v) { if (v==0) return static_cast(0); // From https://graphics.stanford.edu/~seander/bithacks.html#NextBitPermutation - unsigned int t = (v | (v - 1)) + 1; + size_t t = (v | (v - 1)) + 1; return t | ((((t & -t) / (v & -v)) >> 1) - 1); } From 6778a018ad9848faabd8702b50f8bd53ecbf143f Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 27 Oct 2016 19:05:24 +0200 Subject: [PATCH 22/28] Use heuristic probability Former-commit-id: 747b34cfdc1bcabdb673155939946287923af3da --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 10 +++++----- src/builder/ExplicitDFTModelBuilderApprox.h | 2 +- src/storage/BucketPriorityQueue.h | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 86a45235d..131c0389e 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -33,12 +33,12 @@ namespace storm { matrixBuilder(!generator.isDeterministicModel()), stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), // TODO Matthias: make choosable - explorationQueue(dft.nrElements()+1, 0, 1) - //explorationQueue(1001, 0, 0.001) + //explorationQueue(dft.nrElements()+1, 0, 1) + explorationQueue(1001, 0, 0.001) { // Intentionally left empty. // TODO Matthias: remove again - heuristic = storm::builder::ApproximationHeuristic::NONE; + heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; } template @@ -267,8 +267,8 @@ namespace storm { // Try to explore the next state generator.load(currentState); - //if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { - if (currentExplorationHeuristic->isSkip(approximationThreshold)) { + if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) { + //if (currentExplorationHeuristic->isSkip(approximationThreshold)) { // Skip the current state ++nrSkippedStates; STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState)); diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index c3ffe4467..446bed6ad 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicNone; + using ExplorationHeuristic = DFTExplorationHeuristicProbability; using ExplorationHeuristicPointer = std::shared_ptr; diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index 1aa18689d..253b34e19 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket); From b669a3acef838a2841695eda8add73d85cc421d7 Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 27 Oct 2016 21:42:11 +0200 Subject: [PATCH 23/28] Only sort bucket queue if more than 10% is unsorted Former-commit-id: 7ebd1e49c8a74198e4e36e5eeffdfc0ddb158020 --- src/storage/BucketPriorityQueue.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp index eb174cce0..c758be7ee 100644 --- a/src/storage/BucketPriorityQueue.cpp +++ b/src/storage/BucketPriorityQueue.cpp @@ -14,7 +14,7 @@ namespace storm { template void BucketPriorityQueue::fix() { - if (currentBucket < buckets.size() && nrUnsortedItems > 0) { + if (currentBucket < buckets.size() && nrUnsortedItems > buckets[currentBucket].size() / 10) { // Fix current bucket std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); nrUnsortedItems = 0; From a2c484bba43de66721bd575ad98002eef7fabf0b Mon Sep 17 00:00:00 2001 From: Mavo Date: Thu, 27 Oct 2016 21:43:02 +0200 Subject: [PATCH 24/28] Support for probability approximation without modularisation Former-commit-id: 921c8d310c9eab5b82300c908d3f039e9451500a --- src/modelchecker/dft/DFTModelChecker.cpp | 18 ++++++++++++------ src/modelchecker/dft/DFTModelChecker.h | 6 ++++-- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index ff2148982..e49db7a37 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -158,6 +158,8 @@ namespace storm { storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula + bool probabilityFormula = formula->isProbabilityOperatorFormula(); + STORM_LOG_ASSERT((formula->isTimeOperatorFormula() && !probabilityFormula) || (!formula->isTimeOperatorFormula() && probabilityFormula), "Probability formula not initialized correctly"); size_t iteration = 0; do { // Iteratively build finer models @@ -170,7 +172,7 @@ namespace storm { // Build model for lower bound STORM_LOG_INFO("Getting model for lower bound..."); - model = builder.getModelApproximation(true); + model = builder.getModelApproximation(probabilityFormula ? false : true); // We only output the info from the lower bound as the info for the upper bound is the same STORM_LOG_INFO("No. states: " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); @@ -185,7 +187,7 @@ namespace storm { // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); explorationStart = std::chrono::high_resolution_clock::now(); - model = builder.getModelApproximation(false); + model = builder.getModelApproximation(probabilityFormula ? true : false); explorationTime += std::chrono::high_resolution_clock::now() - explorationStart; // Check upper bound result = checkModel(model, formula); @@ -197,7 +199,7 @@ namespace storm { ++iteration; STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); - } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError)); + } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); return approxResult; @@ -251,14 +253,18 @@ namespace storm { } template - bool DFTModelChecker::isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError) { + bool DFTModelChecker::isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError, bool relative) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Approximation works only for double."); } template<> - bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError) { + bool DFTModelChecker::isApproximationSufficient(double lowerBound, double upperBound, double approximationError, bool relative) { STORM_LOG_THROW(!std::isnan(lowerBound) && !std::isnan(upperBound), storm::exceptions::NotSupportedException, "Approximation does not work if result is NaN."); - return upperBound - lowerBound <= approximationError * (lowerBound + upperBound) / 2; + if (relative) { + return upperBound - lowerBound <= approximationError; + } else { + return upperBound - lowerBound <= approximationError * (lowerBound + upperBound) / 2; + } } template diff --git a/src/modelchecker/dft/DFTModelChecker.h b/src/modelchecker/dft/DFTModelChecker.h index 83df59bfa..b351ab67b 100644 --- a/src/modelchecker/dft/DFTModelChecker.h +++ b/src/modelchecker/dft/DFTModelChecker.h @@ -107,15 +107,17 @@ namespace storm { /*! * Checks if the computed approximation is sufficient, i.e. - * upperBound - lowerBound <= approximationError * mean(upperBound, lowerBound). + * upperBound - lowerBound <= approximationError * mean(lowerBound, upperBound). * * @param lowerBound The lower bound on the result. * @param upperBound The upper bound on the result. * @param approximationError The allowed error for approximating. + * @param relative Flag indicating if the error should be relative to 1 or + to the mean of lower and upper bound. * * @return True, if the approximation is sufficient. */ - bool isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError); + bool isApproximationSufficient(ValueType lowerBound, ValueType upperBound, double approximationError, bool relative); }; } From 02c4195f31102da38c3c37615197145f26c669f8 Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 28 Oct 2016 17:56:09 +0200 Subject: [PATCH 25/28] Better upper bound for independent subtrees Former-commit-id: 64f5a1ca603833ea1dafedb1078f17be7c049e20 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 115 +++++++++++++++--- src/builder/ExplicitDFTModelBuilderApprox.h | 13 ++ src/storage/BucketPriorityQueue.cpp | 2 - src/storage/dft/DFTState.cpp | 23 ++-- src/storage/dft/DFTState.h | 22 ++-- 5 files changed, 135 insertions(+), 40 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 131c0389e..7f3e8c09e 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -39,6 +39,61 @@ namespace storm { // Intentionally left empty. // TODO Matthias: remove again heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; + + // Compute independent subtrees + if (dft.topLevelType() == storm::storage::DFTElementType::OR) { + // We only support this for approximation with top level element OR + for (auto const& child : dft.getGate(dft.getTopLevelIndex())->children()) { + // Consider all children of the top level gate + std::vector isubdft; + if (child->nrParents() > 1 || child->hasOutgoingDependencies()) { + STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + isubdft.clear(); + } else if (dft.isGate(child->id())) { + isubdft = dft.getGate(child->id())->independentSubDft(false); + } else { + STORM_LOG_ASSERT(dft.isBasicElement(child->id()), "Child is no BE."); + if(dft.getBasicElement(child->id())->hasIngoingDependencies()) { + STORM_LOG_TRACE("child " << child->name() << "does not allow modularisation."); + isubdft.clear(); + } else { + isubdft = {child->id()}; + } + } + if(isubdft.empty()) { + subtreeBEs.clear(); + break; + } else { + // Add new independent subtree + std::vector subtree; + for (size_t id : isubdft) { + if (dft.isBasicElement(id)) { + subtree.push_back(id); + } + } + subtreeBEs.push_back(subtree); + } + } + } + if (subtreeBEs.empty()) { + // Consider complete tree + std::vector subtree; + for (size_t id = 0; id < dft.nrElements(); ++id) { + if (dft.isBasicElement(id)) { + subtree.push_back(id); + } + } + subtreeBEs.push_back(subtree); + } + + for (auto tree : subtreeBEs) { + std::stringstream stream; + stream << "Subtree: "; + for (size_t id : tree) { + stream << id << ", "; + } + STORM_LOG_TRACE(stream.str()); + } } template @@ -476,18 +531,42 @@ namespace storm { template ValueType ExplicitDFTModelBuilderApprox::getUpperBound(DFTStatePointer const& state) const { // Get the upper bound by considering the failure of all BEs - // The used formula for the rate is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...) - ValueType upperBound = storm::utility::zero(); + ValueType upperBound = storm::utility::one(); + ValueType rateSum = storm::utility::zero(); + + // Compute for each independent subtree + for (std::vector const& subtree : subtreeBEs) { + // Get all possible rates + std::vector rates; + for (size_t id : subtree) { + if (state->isOperational(id)) { + // Get BE rate + rates.push_back(state->getBERate(id, true)); + rateSum += rates.back(); + } + } - // Get all possible rates - std::vector rates(state->nrFailableBEs() + state->nrNotFailableBEs()); - for (size_t index = 0; index < state->nrFailableBEs(); ++index) { - rates[index] = state->getFailableBERate(index); + // We move backwards and start with swapping the last element to itself + // Then we do not need to swap back + for (auto it = rates.rbegin(); it != rates.rend(); ++it) { + // Compute AND MTTF of subtree without current rate and scale with current rate + std::iter_swap(it, rates.end() - 1); + upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1); + } } - for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { - rates[index + state->nrFailableBEs()] = state->getNotFailableBERate(index); + + STORM_LOG_TRACE("Upper bound is " << (rateSum / upperBound) << " for state " << state->getId()); + STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "Upper bound is 0"); + STORM_LOG_ASSERT(!storm::utility::isZero(rateSum), "State is absorbing"); + return rateSum / upperBound; + } + + template + ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector rates, size_t size) const { + ValueType result = storm::utility::zero(); + if (size == 0) { + return result; } - STORM_LOG_ASSERT(rates.size() > 0, "State is absorbing"); // TODO Matthias: works only for <64 BEs! // WARNING: this code produces wrong results for more than 32 BEs @@ -508,30 +587,30 @@ namespace storm { sum += storm::utility::one() / permResult; } while(permutation < (static_cast(1) << rates.size()) && permutation != 0); if (i % 2 == 0) { - upperBound -= sum; + result -= sum; } else { - upperBound += sum; + result += sum; } }*/ - // Compute upper bound with permutations of size <= 3 - for (size_t i1 = 0; i1 < rates.size(); ++i1) { + // Compute result with permutations of size <= 3 + for (size_t i1 = 0; i1 < size; ++i1) { // + 1/a ValueType sum = rates[i1]; - upperBound += storm::utility::one() / sum; + result += storm::utility::one() / sum; for (size_t i2 = 0; i2 < i1; ++i2) { // - 1/(a+b) ValueType sum2 = sum + rates[i2]; - upperBound -= storm::utility::one() / sum2; + result -= storm::utility::one() / sum2; for (size_t i3 = 0; i3 < i2; ++i3) { // + 1/(a+b+c) - upperBound += storm::utility::one() / (sum2 + rates[i3]); + result += storm::utility::one() / (sum2 + rates[i3]); } } } - STORM_LOG_ASSERT(!storm::utility::isZero(upperBound), "UpperBound is 0"); - return storm::utility::one() / upperBound; + STORM_LOG_ASSERT(!storm::utility::isZero(result), "UpperBound is 0"); + return result; } template diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 446bed6ad..8cc53a176 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -238,6 +238,16 @@ namespace storm { */ ValueType getUpperBound(DFTStatePointer const& state) const; + /*! + * Compute the MTTF of an AND gate via a closed formula. + * The used formula is 1/( 1/a + 1/b + 1/c + ... - 1/(a+b) - 1/(a+c) - ... + 1/(a+b+c) + ... - ...) + * + * @param rates List of rates of children of AND. + * @param size Only indices < size are considered in the vector. + * @return MTTF. + */ + ValueType computeMTTFAnd(std::vector rates, size_t size) const; + /*! * Compares the priority of two states. * @@ -314,6 +324,9 @@ namespace storm { // Notice that we need an ordered map here to easily iterate in increasing order over state ids. // TODO remove again std::map> skippedStates; + + // List of independent subtrees and the BEs contained in them. + std::vector> subtreeBEs; }; } diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp index c758be7ee..99ed19cd4 100644 --- a/src/storage/BucketPriorityQueue.cpp +++ b/src/storage/BucketPriorityQueue.cpp @@ -41,7 +41,6 @@ namespace storm { return immediateBucket.back(); } STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); - STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); return buckets[currentBucket].front(); } @@ -126,7 +125,6 @@ namespace storm { return; } STORM_LOG_ASSERT(!empty(), "BucketPriorityQueue is empty"); - STORM_LOG_ASSERT(nrUnsortedItems == 0, "First bucket is not sorted"); std::pop_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); buckets[currentBucket].pop_back(); if (buckets[currentBucket].empty()) { diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index aaad9367f..64728cbd5 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -241,21 +241,26 @@ namespace storm { } template - ValueType DFTState::getBERate(size_t id, bool considerPassive) const { + ValueType DFTState::getBERate(size_t id, bool avoidCold) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); - if (considerPassive && mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { - STORM_LOG_ASSERT(!storm::utility::isZero(mDft.getBasicElement(id)->passiveFailureRate()), "Failure rate of BE " << mDft.getBasicElement(id)->id() << " is 0 in state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); - return mDft.getBasicElement(id)->passiveFailureRate(); - } else { - STORM_LOG_ASSERT(!storm::utility::isZero(mDft.getBasicElement(id)->activeFailureRate()), "Failure rate of BE " << mDft.getBasicElement(id)->id() << " is 0 in state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); - return mDft.getBasicElement(id)->activeFailureRate(); + + if (mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { + if (avoidCold && mDft.getBasicElement(id)->isColdBasicElement()) { + // Return active failure rate instead of 0. + return mDft.getBasicElement(id)->activeFailureRate(); + } else { + // Return passive failure rate + return mDft.getBasicElement(id)->passiveFailureRate(); + } } + // Return active failure rate + return mDft.getBasicElement(id)->activeFailureRate(); } template ValueType DFTState::getFailableBERate(size_t index) const { STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid."); - return getBERate(mCurrentlyFailableBE[index], true); + return getBERate(mCurrentlyFailableBE[index], false); } template @@ -264,7 +269,7 @@ namespace storm { STORM_LOG_ASSERT(isPseudoState() || storm::utility::isZero(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) || (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail in state: " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); // Use active failure rate as passive failure rate is 0. - return getBERate(mCurrentlyNotFailableBE[index], false); + return getBERate(mCurrentlyNotFailableBE[index], true); } template diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 4ff36d1ab..0f8280591 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -208,6 +208,17 @@ namespace storm { */ ValueType getNotFailableBERate(size_t index) const; + /** + * Get the failure rate of the given BE. + * + * @param id Id of BE. + * @param avoidCold Flag indicating if a cold passive failure rate should be avoided by giving + * the active failure rate instead. + * + * @return Failure rate of the BE. + */ + ValueType getBERate(size_t id, bool avoidCold) const; + /** Get number of currently failable dependencies. * * @return Number of failable dependencies. @@ -302,17 +313,6 @@ namespace storm { private: void propagateActivation(size_t representativeId); - /** - * Get the failure rate of the given BE. - * - * @param id Id of BE. - * @param considerPassive Flag indicating if the passive failure rate should be returned if - * the BE currently is passive. - * - * @return Failure rate of the BE. - */ - ValueType getBERate(size_t id, bool considerPassive) const; - }; } From dae1a7eefe69c9ed7bdf7c34d7c43a437f63f105 Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 28 Oct 2016 19:31:59 +0200 Subject: [PATCH 26/28] Do not use cold BEs in first step of approximation formula Former-commit-id: d204be9633c605c450933ee4659a9b8a5e1ac4cd --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 32 ++++++----- src/storage/dft/DFTState.cpp | 53 +++---------------- src/storage/dft/DFTState.h | 25 +-------- 3 files changed, 29 insertions(+), 81 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 7f3e8c09e..28b943ba9 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -522,9 +522,6 @@ namespace storm { for (size_t index = 0; index < state->nrFailableBEs(); ++index) { lowerBound += state->getFailableBERate(index); } - for (size_t index = 0; index < state->nrNotFailableBEs(); ++index) { - lowerBound += state->getNotFailableBERate(index); - } return lowerBound; } @@ -538,20 +535,31 @@ namespace storm { for (std::vector const& subtree : subtreeBEs) { // Get all possible rates std::vector rates; - for (size_t id : subtree) { + storm::storage::BitVector coldBEs(subtree.size(), false); + for (size_t i = 0; i < subtree.size(); ++i) { + size_t id = subtree[i]; if (state->isOperational(id)) { // Get BE rate - rates.push_back(state->getBERate(id, true)); - rateSum += rates.back(); + ValueType rate = state->getBERate(id); + if (storm::utility::isZero(rate)) { + // Get active failure rate for cold BE + rate = dft.getBasicElement(id)->activeFailureRate(); + // Mark BE as cold + coldBEs.set(i, true); + } + rates.push_back(rate); + rateSum += rate; } } - // We move backwards and start with swapping the last element to itself - // Then we do not need to swap back - for (auto it = rates.rbegin(); it != rates.rend(); ++it) { - // Compute AND MTTF of subtree without current rate and scale with current rate - std::iter_swap(it, rates.end() - 1); - upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1); + for (size_t i = 0; i < rates.size(); ++i) { + // Cold BEs cannot fail in the first step + if (!coldBEs.get(i)) { + // Compute AND MTTF of subtree without current rate and scale with current rate + upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1); + // Swap here to avoid swapping back + std::iter_swap(rates.begin() + i, rates.end() - 1); + } } } diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp index 64728cbd5..cc0eaabec 100644 --- a/src/storage/dft/DFTState.cpp +++ b/src/storage/dft/DFTState.cpp @@ -17,23 +17,11 @@ namespace storm { this->setUses(spareId, elem->children()[0]->id()); } - for (auto elem : mDft.getBasicElements()) { - if (!storm::utility::isZero(elem->activeFailureRate())) { - mCurrentlyNotFailableBE.push_back(elem->id()); - } - } - // Initialize activation propagateActivation(mDft.getTopLevelIndex()); std::vector alwaysActiveBEs = mDft.nonColdBEs(); mCurrentlyFailableBE.insert(mCurrentlyFailableBE.end(), alwaysActiveBEs.begin(), alwaysActiveBEs.end()); - // Remove always active BEs from currently not failable BEs - for (size_t id : alwaysActiveBEs) { - auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id); - STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Id not found."); - mCurrentlyNotFailableBE.erase(it); - } } template @@ -46,7 +34,6 @@ namespace storm { STORM_LOG_TRACE("Construct concrete state from pseudo state " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); // Clear information from pseudo state mCurrentlyFailableBE.clear(); - mCurrentlyNotFailableBE.clear(); mFailableDependencies.clear(); mUsedRepresentants.clear(); STORM_LOG_ASSERT(mPseudoState, "Only pseudo states can be constructed."); @@ -57,10 +44,6 @@ namespace storm { if ((!be->isColdBasicElement() && be->canFail()) || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { mCurrentlyFailableBE.push_back(index); STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString()); - } else { - // BE currently is not failable - mCurrentlyNotFailableBE.push_back(index); - STORM_LOG_TRACE("Currently not failable: " << mDft.getBasicElement(index)->toString()); } } else if (mDft.getElement(index)->isSpareGate()) { // Initialize used representants @@ -204,11 +187,6 @@ namespace storm { auto it = std::find(mCurrentlyFailableBE.begin(), mCurrentlyFailableBE.end(), id); if (it != mCurrentlyFailableBE.end()) { mCurrentlyFailableBE.erase(it); - } else { - it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), id); - if (it != mCurrentlyNotFailableBE.end()) { - mCurrentlyNotFailableBE.erase(it); - } } } @@ -241,35 +219,22 @@ namespace storm { } template - ValueType DFTState::getBERate(size_t id, bool avoidCold) const { + ValueType DFTState::getBERate(size_t id) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); if (mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { - if (avoidCold && mDft.getBasicElement(id)->isColdBasicElement()) { - // Return active failure rate instead of 0. - return mDft.getBasicElement(id)->activeFailureRate(); - } else { - // Return passive failure rate - return mDft.getBasicElement(id)->passiveFailureRate(); - } + // Return passive failure rate + return mDft.getBasicElement(id)->passiveFailureRate(); + } else { + // Return active failure rate + return mDft.getBasicElement(id)->activeFailureRate(); } - // Return active failure rate - return mDft.getBasicElement(id)->activeFailureRate(); } template ValueType DFTState::getFailableBERate(size_t index) const { STORM_LOG_ASSERT(index < nrFailableBEs(), "Index invalid."); - return getBERate(mCurrentlyFailableBE[index], false); - } - - template - ValueType DFTState::getNotFailableBERate(size_t index) const { - STORM_LOG_ASSERT(index < nrNotFailableBEs(), "Index invalid."); - STORM_LOG_ASSERT(isPseudoState() || storm::utility::isZero(mDft.getBasicElement(mCurrentlyNotFailableBE[index])->activeFailureRate()) || - (mDft.hasRepresentant(mCurrentlyNotFailableBE[index]) && !isActive(mDft.getRepresentant(mCurrentlyNotFailableBE[index]))), "BE " << mCurrentlyNotFailableBE[index] << " can fail in state: " << mDft.getStateString(mStatus, mStateGenerationInfo, mId)); - // Use active failure rate as passive failure rate is 0. - return getBERate(mCurrentlyNotFailableBE[index], true); + return getBERate(mCurrentlyFailableBE[index]); } template @@ -326,10 +291,6 @@ namespace storm { if (be->isColdBasicElement() && be->canFail()) { // Add to failable BEs mCurrentlyFailableBE.push_back(elem); - // Remove from not failable BEs - auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem); - STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << elem << " not found."); - mCurrentlyNotFailableBE.erase(it); } } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { propagateActivation(uses(elem)); diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h index 0f8280591..b077b58b0 100644 --- a/src/storage/dft/DFTState.h +++ b/src/storage/dft/DFTState.h @@ -27,7 +27,6 @@ namespace storm { storm::storage::BitVector mStatus; size_t mId; std::vector mCurrentlyFailableBE; - std::vector mCurrentlyNotFailableBE; std::vector mFailableDependencies; std::vector mUsedRepresentants; bool mPseudoState; @@ -181,15 +180,6 @@ namespace storm { return mCurrentlyFailableBE.size(); } - /** - * Get number of currently not failable BEs. These are cold BE which can fail in the future. - * - * @return Number of not failable BEs. - */ - size_t nrNotFailableBEs() const { - return mCurrentlyNotFailableBE.size(); - } - /** * Get the failure rate of the currently failable BE on the given index. * @@ -200,24 +190,13 @@ namespace storm { ValueType getFailableBERate(size_t index) const; /** - * Get the failure rate of the currently not failable BE on the given index. - * - * @param index Index of BE in list of currently not failable BEs. - * - * @return Failure rate of the BE. - */ - ValueType getNotFailableBERate(size_t index) const; - - /** - * Get the failure rate of the given BE. + * Get the current failure rate of the given BE. * * @param id Id of BE. - * @param avoidCold Flag indicating if a cold passive failure rate should be avoided by giving - * the active failure rate instead. * * @return Failure rate of the BE. */ - ValueType getBERate(size_t id, bool avoidCold) const; + ValueType getBERate(size_t id) const; /** Get number of currently failable dependencies. * From 64699a7badb5a7e56f6e8366bb85758b5175f46d Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 28 Oct 2016 21:35:16 +0200 Subject: [PATCH 27/28] Several improvements Former-commit-id: 047ebde33bd77dcde7b0a2df5c5e384828f91684 --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 12 +++--- src/modelchecker/dft/DFTModelChecker.cpp | 26 +++++++------ src/modelchecker/dft/DFTModelChecker.h | 1 + src/storage/BucketPriorityQueue.cpp | 37 +++++++++++++------ src/storage/BucketPriorityQueue.h | 25 ++++++++----- 5 files changed, 60 insertions(+), 41 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 28b943ba9..1d04e5210 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -34,7 +34,7 @@ namespace storm { stateStorage(((dft.stateVectorSize() / 64) + 1) * 64), // TODO Matthias: make choosable //explorationQueue(dft.nrElements()+1, 0, 1) - explorationQueue(1001, 0, 0.001) + explorationQueue(200, 0, 0.9) { // Intentionally left empty. // TODO Matthias: remove again @@ -291,9 +291,6 @@ namespace storm { size_t nrSkippedStates = 0; // TODO Matthias: do not empty queue every time but break before while (!explorationQueue.empty()) { - explorationQueue.fix(); - //explorationQueue.print(std::cout); - //printNotExplored(); // Get the first state in the queue ExplorationHeuristicPointer currentExplorationHeuristic = explorationQueue.popTop(); StateType currentId = currentExplorationHeuristic->getId(); @@ -602,17 +599,18 @@ namespace storm { }*/ // Compute result with permutations of size <= 3 + ValueType one = storm::utility::one(); for (size_t i1 = 0; i1 < size; ++i1) { // + 1/a ValueType sum = rates[i1]; - result += storm::utility::one() / sum; + result += one / sum; for (size_t i2 = 0; i2 < i1; ++i2) { // - 1/(a+b) ValueType sum2 = sum + rates[i2]; - result -= storm::utility::one() / sum2; + result -= one / sum2; for (size_t i3 = 0; i3 < i2; ++i3) { // + 1/(a+b+c) - result += storm::utility::one() / (sum2 + rates[i3]); + result += one / (sum2 + rates[i3]); } } } diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp index e49db7a37..5eee17e3e 100644 --- a/src/modelchecker/dft/DFTModelChecker.cpp +++ b/src/modelchecker/dft/DFTModelChecker.cpp @@ -17,13 +17,13 @@ namespace storm { template void DFTModelChecker::check(storm::storage::DFT const& origDft, std::shared_ptr const& formula, bool symred, bool allowModularisation, bool enableDC, double approximationError) { // Initialize - this->buildingTime = std::chrono::duration::zero(); this->explorationTime = std::chrono::duration::zero(); + this->buildingTime = std::chrono::duration::zero(); this->bisimulationTime = std::chrono::duration::zero(); this->modelCheckingTime = std::chrono::duration::zero(); this->totalTime = std::chrono::duration::zero(); this->approximationError = approximationError; - std::chrono::high_resolution_clock::time_point totalStart = std::chrono::high_resolution_clock::now(); + totalStart = std::chrono::high_resolution_clock::now(); // Optimizing DFT storm::storage::DFT dft = origDft.optimize(); @@ -134,7 +134,7 @@ namespace storm { template typename DFTModelChecker::dft_result DFTModelChecker::checkDFT(storm::storage::DFT const& dft, std::shared_ptr const& formula, bool symred, bool enableDC, double approximationError) { - std::chrono::high_resolution_clock::time_point buildingStart = std::chrono::high_resolution_clock::now(); + std::chrono::high_resolution_clock::time_point checkingStart = std::chrono::high_resolution_clock::now(); // Find symmetries std::map>> emptySymmetry; @@ -145,15 +145,12 @@ namespace storm { STORM_LOG_INFO("Found " << symmetries.groups.size() << " symmetries."); STORM_LOG_TRACE("Symmetries: " << std::endl << symmetries); } - std::chrono::high_resolution_clock::time_point buildingEnd = std::chrono::high_resolution_clock::now(); - buildingTime += buildingEnd - buildingStart; if (approximationError > 0.0) { // Comparator for checking the error of the approximation storm::utility::ConstantsComparator comparator; // Build approximate Markov Automata for lower and upper bound approximation_result approxResult = std::make_pair(storm::utility::zero(), storm::utility::zero()); - std::chrono::high_resolution_clock::time_point explorationStart; std::shared_ptr> model; storm::builder::ExplicitDFTModelBuilderApprox builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula @@ -163,10 +160,12 @@ namespace storm { size_t iteration = 0; do { // Iteratively build finer models - explorationStart = std::chrono::high_resolution_clock::now(); + std::chrono::high_resolution_clock::time_point explorationStart = std::chrono::high_resolution_clock::now(); STORM_LOG_INFO("Building model..."); // TODO Matthias refine model using existing model and MC results builder.buildModel(labeloptions, iteration, approximationError); + std::chrono::high_resolution_clock::time_point explorationEnd = std::chrono::high_resolution_clock::now(); + explorationTime = explorationEnd - explorationStart; // TODO Matthias: possible to do bisimulation on approximated model and not on concrete one? @@ -176,7 +175,8 @@ namespace storm { // We only output the info from the lower bound as the info for the upper bound is the same STORM_LOG_INFO("No. states: " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions: " << model->getNumberOfTransitions()); - explorationTime += std::chrono::high_resolution_clock::now() - explorationStart; + buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd; + // Check lower bound std::unique_ptr result = checkModel(model, formula); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); @@ -186,9 +186,9 @@ namespace storm { // Build model for upper bound STORM_LOG_INFO("Getting model for upper bound..."); - explorationStart = std::chrono::high_resolution_clock::now(); + explorationEnd = std::chrono::high_resolution_clock::now(); model = builder.getModelApproximation(probabilityFormula ? true : false); - explorationTime += std::chrono::high_resolution_clock::now() - explorationStart; + buildingTime += std::chrono::high_resolution_clock::now() - explorationEnd; // Check upper bound result = checkModel(model, formula); result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); @@ -198,6 +198,8 @@ namespace storm { ++iteration; STORM_LOG_INFO("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); + totalTime = std::chrono::high_resolution_clock::now() - totalStart; + printTimings(); STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); @@ -221,7 +223,7 @@ namespace storm { //model->printModelInformationToStream(std::cout); STORM_LOG_INFO("No. states (Explored): " << model->getNumberOfStates()); STORM_LOG_INFO("No. transitions (Explored): " << model->getNumberOfTransitions()); - explorationTime += std::chrono::high_resolution_clock::now() - buildingEnd; + explorationTime += std::chrono::high_resolution_clock::now() - checkingStart; // Model checking std::unique_ptr result = checkModel(model, formula); @@ -270,8 +272,8 @@ namespace storm { template void DFTModelChecker::printTimings(std::ostream& os) { os << "Times:" << std::endl; - os << "Building:\t" << buildingTime.count() << std::endl; os << "Exploration:\t" << explorationTime.count() << std::endl; + os << "Building:\t" << buildingTime.count() << std::endl; os << "Bisimulation:\t" << bisimulationTime.count() << std::endl; os << "Modelchecking:\t" << modelCheckingTime.count() << std::endl; os << "Total:\t\t" << totalTime.count() << std::endl; diff --git a/src/modelchecker/dft/DFTModelChecker.h b/src/modelchecker/dft/DFTModelChecker.h index b351ab67b..543bf97fd 100644 --- a/src/modelchecker/dft/DFTModelChecker.h +++ b/src/modelchecker/dft/DFTModelChecker.h @@ -61,6 +61,7 @@ namespace storm { std::chrono::duration bisimulationTime = std::chrono::duration::zero(); std::chrono::duration modelCheckingTime = std::chrono::duration::zero(); std::chrono::duration totalTime = std::chrono::duration::zero(); + std::chrono::high_resolution_clock::time_point totalStart; // Model checking result dft_result checkResult; diff --git a/src/storage/BucketPriorityQueue.cpp b/src/storage/BucketPriorityQueue.cpp index 99ed19cd4..224b14cf6 100644 --- a/src/storage/BucketPriorityQueue.cpp +++ b/src/storage/BucketPriorityQueue.cpp @@ -2,11 +2,13 @@ #include "src/utility/macros.h" #include "src/adapters/CarlAdapter.h" +#include + namespace storm { namespace storage { template - BucketPriorityQueue::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket) : buckets(nrBuckets), currentBucket(nrBuckets), lowerValue(lowerValue), stepPerBucket(stepPerBucket), nrUnsortedItems(0) { + BucketPriorityQueue::BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio) : lowerValue(lowerValue), logBase(std::log(ratio)), nrBuckets(nrBuckets), nrUnsortedItems(0), buckets(nrBuckets), currentBucket(nrBuckets) { compare = ([this](HeuristicPointer a, HeuristicPointer b) { return *a < *b; }); @@ -14,7 +16,7 @@ namespace storm { template void BucketPriorityQueue::fix() { - if (currentBucket < buckets.size() && nrUnsortedItems > buckets[currentBucket].size() / 10) { + if (currentBucket < nrBuckets && nrUnsortedItems > buckets[currentBucket].size() / 10) { // Fix current bucket std::make_heap(buckets[currentBucket].begin(), buckets[currentBucket].end(), compare); nrUnsortedItems = 0; @@ -23,13 +25,13 @@ namespace storm { template bool BucketPriorityQueue::empty() const { - return currentBucket == buckets.size() && immediateBucket.empty(); + return currentBucket == nrBuckets && immediateBucket.empty(); } template std::size_t BucketPriorityQueue::size() const { size_t size = immediateBucket.size(); - for (size_t i = currentBucket; currentBucket < buckets.size(); ++i) { + for (size_t i = currentBucket; currentBucket < nrBuckets; ++i) { size += buckets[i].size(); } return size; @@ -129,7 +131,7 @@ namespace storm { buckets[currentBucket].pop_back(); if (buckets[currentBucket].empty()) { // Find next bucket with elements - for ( ; currentBucket < buckets.size(); ++currentBucket) { + for ( ; currentBucket < nrBuckets; ++currentBucket) { if (!buckets[currentBucket].empty()) { nrUnsortedItems = buckets[currentBucket].size(); if (AUTOSORT) { @@ -151,18 +153,21 @@ namespace storm { template size_t BucketPriorityQueue::getBucket(double priority) const { STORM_LOG_ASSERT(priority >= lowerValue, "Priority " << priority << " is too low"); - size_t newBucket = (priority - lowerValue) / stepPerBucket; - if (HIGHER) { - newBucket = buckets.size()-1 - newBucket; + size_t newBucket = std::log(priority - lowerValue) / logBase; + if (newBucket >= nrBuckets) { + newBucket = nrBuckets - 1; + } + if (!HIGHER) { + newBucket = nrBuckets-1 - newBucket; } - //std::cout << "get Bucket: " << priority << ", " << newBucket << ", " << ((priority - lowerValue) / stepPerBucket) << std::endl; - STORM_LOG_ASSERT(newBucket < buckets.size(), "Priority " << priority << " is too high"); + //std::cout << "get Bucket: " << priority << ", " << newBucket << std::endl; + STORM_LOG_ASSERT(newBucket < nrBuckets, "Priority " << priority << " is too high"); return newBucket; } template void BucketPriorityQueue::print(std::ostream& out) const { - out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and step per bucket: " << stepPerBucket << std::endl; + out << "Bucket priority queue with size " << buckets.size() << ", lower value: " << lowerValue << " and logBase: " << logBase << std::endl; out << "Immediate bucket: "; for (HeuristicPointer heuristic : immediateBucket) { out << heuristic->getId() << ", "; @@ -171,7 +176,7 @@ namespace storm { out << "Current bucket (" << currentBucket << ") has " << nrUnsortedItems << " unsorted items" << std::endl; for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { if (!buckets[bucket].empty()) { - out << "Bucket " << bucket << " (" << (HIGHER ? buckets.size() -1 - bucket * stepPerBucket : bucket * stepPerBucket) << "):" << std::endl; + out << "Bucket " << bucket << ":" << std::endl; for (HeuristicPointer heuristic : buckets[bucket]) { out << "\t" << heuristic->getId() << ": " << heuristic->getPriority() << std::endl; } @@ -179,6 +184,14 @@ namespace storm { } } + template + void BucketPriorityQueue::printSizes(std::ostream& out) const { + out << "Bucket sizes: " << immediateBucket.size() << " | "; + for (size_t bucket = 0; bucket < buckets.size(); ++bucket) { + out << buckets[bucket].size() << " "; + } + std::cout << std::endl; + } // Template instantiations template class BucketPriorityQueue; diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index 253b34e19..1719c7124 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -16,7 +16,7 @@ namespace storm { using HeuristicPointer = std::shared_ptr>; public: - explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket); + explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio); void fix(); @@ -36,10 +36,24 @@ namespace storm { void print(std::ostream& out) const; + void printSizes(std::ostream& out) const; + private: size_t getBucket(double priority) const; + const double lowerValue; + + const bool HIGHER = true; + + const bool AUTOSORT = false; + + const double logBase; + + const size_t nrBuckets; + + size_t nrUnsortedItems; + // List of buckets std::vector> buckets; @@ -51,15 +65,6 @@ namespace storm { std::function compare; - double lowerValue; - - double stepPerBucket; - - size_t nrUnsortedItems; - - const bool HIGHER = true; - - const bool AUTOSORT = false; }; } From d95bb71f75a4febcd93abf7b075261671fe070a5 Mon Sep 17 00:00:00 2001 From: Mavo Date: Sat, 29 Oct 2016 00:02:20 +0200 Subject: [PATCH 28/28] Tried to gain more performance Former-commit-id: 9af2ab7ce0cc6fc311bd5f45c8b2ea79f29c989c --- src/builder/ExplicitDFTModelBuilderApprox.cpp | 19 ++++++++++++++++--- src/builder/ExplicitDFTModelBuilderApprox.h | 2 +- 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 1d04e5210..93a7b282e 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp @@ -549,11 +549,24 @@ namespace storm { } } + STORM_LOG_ASSERT(rates.size() > 0, "No rates failable"); + + // Sort rates + std::sort(rates.begin(), rates.end()); + std::vector rateCount(rates.size(), 0); + size_t lastIndex = 0; + for (size_t i = 0; i < rates.size(); ++i) { + if (rates[lastIndex] != rates[i]) { + lastIndex = i; + } + ++rateCount[lastIndex]; + } + for (size_t i = 0; i < rates.size(); ++i) { // Cold BEs cannot fail in the first step - if (!coldBEs.get(i)) { + if (!coldBEs.get(i) && rateCount[i] > 0) { // Compute AND MTTF of subtree without current rate and scale with current rate - upperBound += rates.back() * computeMTTFAnd(rates, rates.size() - 1); + upperBound += rates.back() * rateCount[i] * computeMTTFAnd(rates, rates.size() - 1); // Swap here to avoid swapping back std::iter_swap(rates.begin() + i, rates.end() - 1); } @@ -567,7 +580,7 @@ namespace storm { } template - ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector rates, size_t size) const { + ValueType ExplicitDFTModelBuilderApprox::computeMTTFAnd(std::vector const& rates, size_t size) const { ValueType result = storm::utility::zero(); if (size == 0) { return result; diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index 8cc53a176..933cd3277 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -246,7 +246,7 @@ namespace storm { * @param size Only indices < size are considered in the vector. * @return MTTF. */ - ValueType computeMTTFAnd(std::vector rates, size_t size) const; + ValueType computeMTTFAnd(std::vector const& rates, size_t size) const; /*! * Compares the priority of two states.