From 4a6f53031e01069f68789c205ff70b77f56c504d Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 18 Oct 2016 14:42:52 +0200 Subject: [PATCH] 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; }