From 90ae65ffa94ee7ff999b4141d4d6972b0320860a Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 4 Jul 2016 18:28:14 +0200 Subject: [PATCH] computation of digitization constant Former-commit-id: cd75d845661b4e187f9ad2b079d2ae22a31567e2 --- .../ma/stream/stream_bounded_pareto.csl | 1 + ...rseMaMultiObjectiveWeightVectorChecker.cpp | 93 ++++++++++++++++++- ...parseMaMultiObjectiveWeightVectorChecker.h | 11 +++ .../SparseMultiObjectivePreprocessor.cpp | 2 +- 4 files changed, 105 insertions(+), 2 deletions(-) create mode 100644 examples/multiobjective/ma/stream/stream_bounded_pareto.csl diff --git a/examples/multiobjective/ma/stream/stream_bounded_pareto.csl b/examples/multiobjective/ma/stream/stream_bounded_pareto.csl new file mode 100644 index 000000000..63661cf61 --- /dev/null +++ b/examples/multiobjective/ma/stream/stream_bounded_pareto.csl @@ -0,0 +1 @@ +multi(Pmin=? [ F<=3.5 "done" ], Pmin=? [ F<=1 s=2 ]) diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp index 938d0964e..b35fda77a 100644 --- a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp @@ -1,11 +1,14 @@ #include "src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h" +#include + #include "src/adapters/CarlAdapter.h" #include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/utility/macros.h" #include "src/utility/vector.h" +#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace modelchecker { @@ -26,11 +29,17 @@ namespace storm { } } + } template void SparseMaMultiObjectiveWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { - STORM_LOG_ERROR("BOUNDED OBJECTIVES FOR MARKOV AUTOMATA NOT YET IMPLEMENTED"); + + + // Set the digitization constant + ValueType digitizationConstant = getDigitizationConstant(); + std::cout << "Got delta: " << digitizationConstant << std::endl; + /* // Allocate some memory so this does not need to happen for each time epoch std::vector optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates()); @@ -84,9 +93,91 @@ namespace storm { } */ } + + template + template ::SupportsExponential, int>::type> + VT SparseMaMultiObjectiveWeightVectorChecker::getDigitizationConstant() const { + STORM_LOG_DEBUG("Retrieving digitization constant"); + // We need to find a delta such that for each pair of lower and upper bounds it holds that + // 1 - e^(-maxRate lowerbound) * (1 + maxRate delta) ^ (lowerbound / delta) + 1-e^(-maxRate upperbound) * (1 + maxRate delta) ^ (upperbound / delta) <= maximumLowerUpperBoundGap + // and lowerbound/delta , upperbound/delta are natural numbers. + + // Initialize some data for fast and easy access + VT const maxRate = this->data.preprocessedModel.getMaximalExitRate(); + std::vector> lowerUpperBounds; + std::vector> eToPowerOfMinusMaxRateTimesBound; + for(auto const& obj : this->data.objectives) { + if(obj.timeBounds) { + if(obj.timeBounds->which() == 0) { + lowerUpperBounds.emplace_back(storm::utility::zero(), boost::get(*obj.timeBounds)); + eToPowerOfMinusMaxRateTimesBound.emplace_back(storm::utility::one(), std::exp(-maxRate * lowerUpperBounds.back().second)); + } else { + auto const& pair = boost::get>(*obj.timeBounds); + lowerUpperBounds.emplace_back(storm::utility::convertNumber(pair.first), storm::utility::convertNumber(pair.second)); + eToPowerOfMinusMaxRateTimesBound.emplace_back(std::exp(-maxRate * lowerUpperBounds.back().first), std::exp(-maxRate * lowerUpperBounds.back().second)); + } + } + } + VT smallestNonZeroBound = storm::utility::zero(); + for (auto const& bounds : lowerUpperBounds) { + if(!storm::utility::isZero(bounds.first)) { + smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? bounds.first : std::min(smallestNonZeroBound, bounds.first); + } else if (!storm::utility::isZero(bounds.second)) { + smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? bounds.second : std::min(smallestNonZeroBound, bounds.second); + } + } + if(storm::utility::isZero(smallestNonZeroBound)) { + // All time bounds are zero which means that any delta>0 is valid. + // This includes the case where there are no time bounds + return storm::utility::one(); + } + + // We brute-force a delta, since a direct computation is apparently not easy. + // Also note that the number of times this loop runs is a lower bound for the number of minMaxSolver invocations. + // Hence, this brute-force approach will most likely not be a bottleneck. + uint_fast64_t smallestStepBound = 1; + VT delta = smallestNonZeroBound / smallestStepBound; + while(true) { + bool deltaValid = true; + for(auto const& bounds : lowerUpperBounds) { + if(bounds.first/delta != std::floor(bounds.first/delta) || + bounds.second/delta != std::floor(bounds.second/delta)) { + deltaValid = false; + break; + } + } + if(deltaValid) { + for(uint_fast64_t i = 0; i() - (eToPowerOfMinusMaxRateTimesBound[i].first * storm::utility::pow(storm::utility::one() + maxRate * delta, lowerUpperBounds[i].first / delta) ); + precisionOfObj += storm::utility::one() - (eToPowerOfMinusMaxRateTimesBound[i].second * storm::utility::pow(storm::utility::one() + maxRate * delta, lowerUpperBounds[i].second / delta) ); + if(precisionOfObj > this->maximumLowerUpperBoundGap) { + deltaValid = false; + break; + } + } + } + if(deltaValid) { + break; + } + ++smallestStepBound; + STORM_LOG_ASSERT(delta>smallestNonZeroBound / smallestStepBound, "Digitization constant is expected to become smaller in every iteration"); + delta = smallestNonZeroBound / smallestStepBound; + } + STORM_LOG_DEBUG("Found digitization constant: " << delta << ". At least " << smallestStepBound << " digitization steps will be necessarry"); + return delta; + } + + + template + template ::SupportsExponential, int>::type> + VT SparseMaMultiObjectiveWeightVectorChecker::getDigitizationConstant() const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); + } template class SparseMaMultiObjectiveWeightVectorChecker>; + template double SparseMaMultiObjectiveWeightVectorChecker>::getDigitizationConstant() const; #ifdef STORM_HAVE_CARL + template storm::RationalNumber SparseMaMultiObjectiveWeightVectorChecker>::getDigitizationConstant() const; template class SparseMaMultiObjectiveWeightVectorChecker>; #endif diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h index f94a4094b..2670fb5e3 100644 --- a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h +++ b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h @@ -2,8 +2,10 @@ #define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ #include +#include #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h" +#include "src/utility/NumberTraits.h" namespace storm { namespace modelchecker { @@ -31,6 +33,15 @@ namespace storm { * @param weightedRewardVector the weighted rewards (initially only considering the unbounded objectives, will be extended to all objectives) */ virtual void boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) override; + + /*! + * + * Retrieves the delta used for the digitization + */ + template ::SupportsExponential, int>::type = 0> + VT getDigitizationConstant() const; + template ::SupportsExponential, int>::type = 0> + VT getDigitizationConstant() const; }; diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index 75cebba30..01b5c1f9f 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp @@ -271,7 +271,7 @@ namespace storm { STORM_LOG_THROW(formula.getDiscreteTimeBound() > 0, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula with time bound 0. This is not supported."); currentObjective.timeBounds = formula.getDiscreteTimeBound(); } else { - STORM_LOG_THROW(formula.getIntervalBounds().first==formula.getIntervalBounds().second, storm::exceptions::InvalidPropertyException, "Got a boundedUntilFormula where upper and lower time bounds are equal. This is not supported."); + STORM_LOG_THROW(formula.getIntervalBounds().first