From 0e34bdbfc4fc8d767ee737a9437ea0091049d91d Mon Sep 17 00:00:00 2001 From: TimQu <tim.quatmann@web.de> Date: Thu, 30 Jun 2016 19:36:14 +0200 Subject: [PATCH] split weight vector checker into one for MDPs and one for MAs Former-commit-id: 142a151f3c038b16eee45c576296cf94f3f423a0 --- .../SparseMaMultiObjectiveModelChecker.cpp | 4 +- .../SparseMdpMultiObjectiveModelChecker.cpp | 4 +- ...rseMaMultiObjectiveWeightVectorChecker.cpp | 88 ++++++++++++++ ...parseMaMultiObjectiveWeightVectorChecker.h | 47 ++++++++ ...seMdpMultiObjectiveWeightVectorChecker.cpp | 85 ++++++++++++++ ...arseMdpMultiObjectiveWeightVectorChecker.h | 51 +++++++++ .../helper/SparseMultiObjectiveHelper.cpp | 27 ++--- .../helper/SparseMultiObjectiveHelper.h | 11 +- ...parseMultiObjectiveWeightVectorChecker.cpp | 108 +++++------------- .../SparseMultiObjectiveWeightVectorChecker.h | 16 ++- 10 files changed, 333 insertions(+), 108 deletions(-) create mode 100644 src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp create mode 100644 src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h create mode 100644 src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp create mode 100644 src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h diff --git a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp index 529f141c2..18b44c44d 100644 --- a/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMaMultiObjectiveModelChecker.cpp @@ -10,6 +10,7 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h" +#include "src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h" @@ -47,7 +48,8 @@ namespace storm { STORM_LOG_DEBUG("Preprocessing done. Data: " << preprocessorData); storm::utility::Stopwatch swHelper; - auto resultData = helper::SparseMultiObjectiveHelper<SparseMaModelType, storm::RationalNumber>::check(preprocessorData); + std::shared_ptr<helper::SparseMultiObjectiveWeightVectorChecker<SparseMaModelType>> weightVectorChecker( new helper::SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>(preprocessorData)); + auto resultData = helper::SparseMultiObjectiveHelper<SparseMaModelType, storm::RationalNumber>::check(preprocessorData, weightVectorChecker); swHelper.pause(); STORM_LOG_DEBUG("Modelchecking done."); diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index 820172d5a..08fccb12e 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -10,6 +10,7 @@ #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h" +#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h" #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h" @@ -46,7 +47,8 @@ namespace storm { STORM_LOG_DEBUG("Preprocessing done. Data: " << preprocessorData); storm::utility::Stopwatch swHelper; - auto resultData = helper::SparseMultiObjectiveHelper<SparseMdpModelType, storm::RationalNumber>::check(preprocessorData); + std::shared_ptr<helper::SparseMultiObjectiveWeightVectorChecker<SparseMdpModelType>> weightVectorChecker( new helper::SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>(preprocessorData)); + auto resultData = helper::SparseMultiObjectiveHelper<SparseMdpModelType, storm::RationalNumber>::check(preprocessorData, weightVectorChecker); swHelper.pause(); STORM_LOG_DEBUG("Modelchecking done."); diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp new file mode 100644 index 000000000..18ac306da --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.cpp @@ -0,0 +1,88 @@ +#include "src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h" + +#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" + + +namespace storm { + namespace modelchecker { + namespace helper { + + template <class SparseMaModelType> + SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker<SparseMaModelType>(data) { + // Intentionally left empty + } + + template <class SparseMaModelType> + std::vector<typename SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::ValueType> SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::getObjectiveRewardAsDiscreteActionRewards(uint_fast64_t objectiveIndex) const { + // Assert that the state and transition rewards have already been removed in prerpocessing + STORM_LOG_ASSERT(!this->data.preprocessedModel.getRewardModel(this->data.objectives[objectiveIndex].rewardModelName).hasStateRewards(), "Reward model has state rewards which is not expected."); + STORM_LOG_ASSERT(!this->data.preprocessedModel.getRewardModel(this->data.objectives[objectiveIndex].rewardModelName).hasTransitionRewards(), "Reward model has transition rewards which is not expected."); + return this->data.preprocessedModel.getRewardModel(this->data.objectives[objectiveIndex].rewardModelName).getStateActionRewardVector(); + } + + template <class SparseMaModelType> + void SparseMaMultiObjectiveWeightVectorChecker<SparseMaModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) { + STORM_LOG_ERROR("BOUNDED OBJECTIVES FOR MARKOV AUTOMATA NOT YET IMPLEMENTED"); + /* + // Allocate some memory so this does not need to happen for each time epoch + std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates()); + std::vector<ValueType> choiceValues(weightedRewardVector.size()); + std::vector<ValueType> temporaryResult(this->data.preprocessedModel.getNumberOfStates()); + // Get for each occurring timeBound the indices of the objectives with that bound. + std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> timeBounds; + storm::storage::BitVector boundedObjectives = ~this->unboundedObjectives; + for(uint_fast64_t objIndex : boundedObjectives) { + uint_fast64_t timeBound = boost::get<uint_fast64_t>(this->data.objectives[objIndex].timeBounds.get()); + auto timeBoundIt = timeBounds.insert(std::make_pair(timeBound, storm::storage::BitVector(this->data.objectives.size(), false))).first; + timeBoundIt->second.set(objIndex); + } + storm::storage::BitVector objectivesAtCurrentEpoch = this->unboundedObjectives; + auto timeBoundIt = timeBounds.begin(); + for(uint_fast64_t currentEpoch = timeBoundIt->first; currentEpoch > 0; --currentEpoch) { + if(timeBoundIt != timeBounds.end() && currentEpoch == timeBoundIt->first) { + objectivesAtCurrentEpoch |= timeBoundIt->second; + for(auto objIndex : timeBoundIt->second) { + storm::utility::vector::addScaledVector(weightedRewardVector, getObjectiveRewardAsDiscreteActionRewards(objIndex), weightVector[objIndex]); + } + ++timeBoundIt; + } + + // Get values and scheduler for weighted sum of objectives + this->data.preprocessedModel.getTransitionMatrix().multiplyWithVector(this->weightedResult, choiceValues); + storm::utility::vector::addVectors(choiceValues, weightedRewardVector, choiceValues); + storm::utility::vector::reduceVectorMax(choiceValues, this->weightedResult, this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), &optimalChoicesInCurrentEpoch); + + // get values for individual objectives + // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. + for(auto objIndex : objectivesAtCurrentEpoch) { + std::vector<ValueType>& objectiveResult = this->objectiveResults[objIndex]; + std::vector<ValueType> objectiveRewards = getObjectiveRewardAsDiscreteActionRewards(objIndex); + auto rowGroupIndexIt = this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin(); + auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin(); + for(ValueType& stateValue : temporaryResult){ + uint_fast64_t row = (*rowGroupIndexIt) + (*optimalChoiceIt); + ++rowGroupIndexIt; + ++optimalChoiceIt; + stateValue = objectiveRewards[row]; + for(auto const& entry : this->data.preprocessedModel.getTransitionMatrix().getRow(row)) { + stateValue += entry.getValue() * objectiveResult[entry.getColumn()]; + } + } + objectiveResult.swap(temporaryResult); + } + } + */ + } + + template class SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>; +#ifdef STORM_HAVE_CARL + template class SparseMaMultiObjectiveWeightVectorChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>; +#endif + + } + } +} diff --git a/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h new file mode 100644 index 000000000..dcc007bfe --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMaMultiObjectiveWeightVectorChecker.h @@ -0,0 +1,47 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ + +#include <vector> + +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + /*! + * Helper Class that takes preprocessed multi objective data and a weight vector and ... + * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives + * - extracts the scheduler that induces this maximum + * - computes for each objective the value induced by this scheduler + */ + template <class SparseMaModelType> + class SparseMaMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker<SparseMaModelType> { + public: + typedef typename SparseMaModelType::ValueType ValueType; + typedef SparseMultiObjectivePreprocessorData<SparseMaModelType> PreprocessorData; + + SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data); + + private: + + + /*! + * Retrieves the rewards for the objective with the given index as state action reward vector. + */ + virtual std::vector<ValueType> getObjectiveRewardAsDiscreteActionRewards(uint_fast64_t objectiveIndex) const override; + + /*! + * + * @param weightVector the weight vector of the current check + * @param weightedRewardVector the weighted rewards (initially only considering the unbounded objectives, will be extended to all objectives) + */ + virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) override; + + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMAMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp new file mode 100644 index 000000000..3c1137721 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.cpp @@ -0,0 +1,85 @@ +#include "src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h" + +#include "src/adapters/CarlAdapter.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/StandardRewardModel.h" +#include "src/utility/macros.h" +#include "src/utility/vector.h" + + +namespace storm { + namespace modelchecker { + namespace helper { + + template <class SparseMdpModelType> + SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>::SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker<SparseMdpModelType>(data) { + // Intentionally left empty + } + + template <class SparseMdpModelType> + std::vector<typename SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>::ValueType> SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>::getObjectiveRewardAsDiscreteActionRewards(uint_fast64_t objectiveIndex) const { + // Assert that the state and transition rewards have already been removed in prerpocessing + STORM_LOG_ASSERT(!this->data.preprocessedModel.getRewardModel(this->data.objectives[objectiveIndex].rewardModelName).hasStateRewards(), "Reward model has state rewards which is not expected."); + STORM_LOG_ASSERT(!this->data.preprocessedModel.getRewardModel(this->data.objectives[objectiveIndex].rewardModelName).hasTransitionRewards(), "Reward model has transition rewards which is not expected."); + return this->data.preprocessedModel.getRewardModel(this->data.objectives[objectiveIndex].rewardModelName).getStateActionRewardVector(); + } + + template <class SparseMdpModelType> + void SparseMdpMultiObjectiveWeightVectorChecker<SparseMdpModelType>::boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) { + // Allocate some memory so this does not need to happen for each time epoch + std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates()); + std::vector<ValueType> choiceValues(weightedRewardVector.size()); + std::vector<ValueType> temporaryResult(this->data.preprocessedModel.getNumberOfStates()); + // Get for each occurring timeBound the indices of the objectives with that bound. + std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> timeBounds; + storm::storage::BitVector boundedObjectives = ~this->unboundedObjectives; + for(uint_fast64_t objIndex : boundedObjectives) { + uint_fast64_t timeBound = boost::get<uint_fast64_t>(this->data.objectives[objIndex].timeBounds.get()); + auto timeBoundIt = timeBounds.insert(std::make_pair(timeBound, storm::storage::BitVector(this->data.objectives.size(), false))).first; + timeBoundIt->second.set(objIndex); + } + storm::storage::BitVector objectivesAtCurrentEpoch = this->unboundedObjectives; + auto timeBoundIt = timeBounds.begin(); + for(uint_fast64_t currentEpoch = timeBoundIt->first; currentEpoch > 0; --currentEpoch) { + if(timeBoundIt != timeBounds.end() && currentEpoch == timeBoundIt->first) { + objectivesAtCurrentEpoch |= timeBoundIt->second; + for(auto objIndex : timeBoundIt->second) { + storm::utility::vector::addScaledVector(weightedRewardVector, getObjectiveRewardAsDiscreteActionRewards(objIndex), weightVector[objIndex]); + } + ++timeBoundIt; + } + + // Get values and scheduler for weighted sum of objectives + this->data.preprocessedModel.getTransitionMatrix().multiplyWithVector(this->weightedResult, choiceValues); + storm::utility::vector::addVectors(choiceValues, weightedRewardVector, choiceValues); + storm::utility::vector::reduceVectorMax(choiceValues, this->weightedResult, this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), &optimalChoicesInCurrentEpoch); + + // get values for individual objectives + // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. + for(auto objIndex : objectivesAtCurrentEpoch) { + std::vector<ValueType>& objectiveResult = this->objectiveResults[objIndex]; + std::vector<ValueType> objectiveRewards = getObjectiveRewardAsDiscreteActionRewards(objIndex); + auto rowGroupIndexIt = this->data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin(); + auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin(); + for(ValueType& stateValue : temporaryResult){ + uint_fast64_t row = (*rowGroupIndexIt) + (*optimalChoiceIt); + ++rowGroupIndexIt; + ++optimalChoiceIt; + stateValue = objectiveRewards[row]; + for(auto const& entry : this->data.preprocessedModel.getTransitionMatrix().getRow(row)) { + stateValue += entry.getValue() * objectiveResult[entry.getColumn()]; + } + } + objectiveResult.swap(temporaryResult); + } + } + } + + template class SparseMdpMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>; +#ifdef STORM_HAVE_CARL + template class SparseMdpMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>; +#endif + + } + } +} diff --git a/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h new file mode 100644 index 000000000..ab67bab22 --- /dev/null +++ b/src/modelchecker/multiobjective/helper/SparseMdpMultiObjectiveWeightVectorChecker.h @@ -0,0 +1,51 @@ +#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ +#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTVECTORCHECKER_H_ + +#include <vector> + +#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h" + +namespace storm { + namespace modelchecker { + namespace helper { + + /*! + * Helper Class that takes preprocessed multi objective data and a weight vector and ... + * - computes the maximal expected reward w.r.t. the weighted sum of the rewards of the individual objectives + * - extracts the scheduler that induces this maximum + * - computes for each objective the value induced by this scheduler + */ + template <class SparseMdpModelType> + class SparseMdpMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker<SparseMdpModelType> { + public: + typedef typename SparseMdpModelType::ValueType ValueType; + typedef SparseMultiObjectivePreprocessorData<SparseMdpModelType> PreprocessorData; + + SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data); + + private: + + + /*! + * Retrieves the rewards for the objective with the given index as state action reward vector. + */ + virtual std::vector<ValueType> getObjectiveRewardAsDiscreteActionRewards(uint_fast64_t objectiveIndex) const override; + + /*! + * For each time epoch (starting with the maximal stepBound occurring in the objectives), this method + * - determines the objectives that are relevant in the current time epoch + * - determines the maximizing scheduler for the weighted reward vector of these objectives + * - computes the values of these objectives w.r.t. this scheduler + * + * @param weightVector the weight vector of the current check + * @param weightedRewardVector the weighted rewards (initially only considering the unbounded objectives, will be extended to all objectives) + */ + virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) override; + + }; + + } + } +} + +#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMDPMULTIOBJECTIVEWEIGHTEDVECTORCHECKER_H_ */ diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp index 0f3606c2b..46e9dcf44 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp @@ -18,7 +18,7 @@ namespace storm { template <class SparseModelType, typename RationalNumberType> - typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::ResultData SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::check(PreprocessorData const& preprocessorData) { + typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::ResultData SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::check(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker) { ResultData resultData; resultData.overApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope(); resultData.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope(); @@ -26,13 +26,13 @@ namespace storm { if(!checkIfPreprocessingWasConclusive(preprocessorData)) { switch(preprocessorData.queryType) { case PreprocessorData::QueryType::Achievability: - achievabilityQuery(preprocessorData, resultData); + achievabilityQuery(preprocessorData, weightVectorChecker, resultData); break; case PreprocessorData::QueryType::Numerical: - numericalQuery(preprocessorData, resultData); + numericalQuery(preprocessorData, weightVectorChecker, resultData); break; case PreprocessorData::QueryType::Pareto: - paretoQuery(preprocessorData, resultData); + paretoQuery(preprocessorData, weightVectorChecker, resultData); break; default: STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type"); @@ -56,7 +56,7 @@ namespace storm { } template <class SparseModelType, typename RationalNumberType> - void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::achievabilityQuery(PreprocessorData const& preprocessorData, ResultData& resultData) { + void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::achievabilityQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) { Point thresholds; thresholds.reserve(preprocessorData.objectives.size()); storm::storage::BitVector strictThresholds(preprocessorData.objectives.size()); @@ -66,7 +66,6 @@ namespace storm { } storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true); - SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(preprocessorData); do { WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked); performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData); @@ -80,7 +79,7 @@ namespace storm { } template <class SparseModelType, typename RationalNumberType> - void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::numericalQuery(PreprocessorData const& preprocessorData, ResultData& resultData) { + void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::numericalQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) { STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Detected numerical query but index of optimizing objective is not set."); uint_fast64_t optimizingObjIndex = *preprocessorData.indexOfOptimizingObjective; Point thresholds; @@ -107,7 +106,6 @@ namespace storm { // Try to find one valid solution storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true); individualObjectivesToBeChecked.set(optimizingObjIndex, false); - SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(preprocessorData); do { WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked); performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData); @@ -150,8 +148,7 @@ namespace storm { } template <class SparseModelType, typename RationalNumberType> - void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::paretoQuery(PreprocessorData const& preprocessorData, ResultData& resultData) { - SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(preprocessorData); + void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) { //First consider the objectives individually for(uint_fast64_t objIndex = 0; objIndex<preprocessorData.objectives.size() && !maxStepsPerformed(resultData); ++objIndex) { WeightVector direction(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>()); @@ -228,13 +225,13 @@ namespace storm { } template <class SparseModelType, typename RationalNumberType> - void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ResultData& result) { - weightVectorChecker.check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction)); - STORM_LOG_DEBUG("weighted objectives checker result is " << storm::utility::vector::convertNumericVector<double>(weightVectorChecker.getInitialStateResultOfObjectives())); + void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector const& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& result) { + weightVectorChecker->check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction)); + STORM_LOG_DEBUG("weighted objectives checker result is " << storm::utility::vector::convertNumericVector<double>(weightVectorChecker->getInitialStateResultOfObjectives())); if(saveScheduler) { - result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives<RationalNumberType>(), weightVectorChecker.getScheduler()); + result.refinementSteps().emplace_back(direction, weightVectorChecker->template getInitialStateResultOfObjectives<RationalNumberType>(), weightVectorChecker->getScheduler()); } else { - result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives<RationalNumberType>()); + result.refinementSteps().emplace_back(direction, weightVectorChecker->template getInitialStateResultOfObjectives<RationalNumberType>()); } updateOverApproximation(result.refinementSteps(), result.overApproximation()); updateUnderApproximation(result.refinementSteps(), result.underApproximation()); diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h index c1746eda0..f5a8746bb 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h @@ -19,11 +19,12 @@ namespace storm { typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData; typedef SparseMultiObjectiveResultData<RationalNumberType> ResultData; typedef SparseMultiObjectiveRefinementStep<RationalNumberType> RefinementStep; + typedef std::shared_ptr<SparseMultiObjectiveWeightVectorChecker<SparseModelType>> WeightVectorCheckerType; typedef std::vector<RationalNumberType> Point; typedef std::vector<RationalNumberType> WeightVector; - static ResultData check(PreprocessorData const& preprocessorData); + static ResultData check(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker); private: @@ -34,9 +35,9 @@ namespace storm { */ static bool checkIfPreprocessingWasConclusive(PreprocessorData const& preprocessorData); - static void achievabilityQuery(PreprocessorData const& preprocessorData, ResultData& resultData); - static void numericalQuery(PreprocessorData const& preprocessorData, ResultData& resultData); - static void paretoQuery(PreprocessorData const& preprocessorData, ResultData& resultData); + static void achievabilityQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); + static void numericalQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); + static void paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); /* * Returns a weight vector w that separates the under approximation from the given point p, i.e., @@ -51,7 +52,7 @@ namespace storm { /* * Refines the current result w.r.t. the given direction vector */ - static void performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ResultData& resultData); + static void performRefinementStep(WeightVector const& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& resultData); /* * Updates the overapproximation after a refinement step has been performed diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index c631baa2d..5bf5e3547 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp @@ -22,30 +22,33 @@ namespace storm { template <class SparseModelType> - SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), checkHasBeenCalled(false) , objectiveResults(data.objectives.size()){ + SparseMultiObjectiveWeightVectorChecker<SparseModelType>::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), unboundedObjectives(data.objectives.size()),checkHasBeenCalled(false), objectiveResults(data.objectives.size()){ + // set the unbounded objectives + for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { + unboundedObjectives.set(objIndex, !data.objectives[objIndex].timeBounds); + } // Enlarge the set of prob1 states to the states that are only reachable via prob1 states statesThatAreAllowedToBeVisitedInfinitelyOften = ~storm::utility::graph::getReachableStates(data.preprocessedModel.getTransitionMatrix(), data.preprocessedModel.getInitialStates(), ~data.preprocessedModel.getStates(data.prob1StatesLabel), storm::storage::BitVector(data.preprocessedModel.getNumberOfStates(), false)); } + template <class SparseModelType> void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) { checkHasBeenCalled=true; STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::convertNumericVector<double>(weightVector)); - storm::storage::BitVector unboundedObjectives(data.objectives.size(), false); std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>()); - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - if(!data.objectives[objIndex].timeBounds) { - unboundedObjectives.set(objIndex, true); - storm::utility::vector::addScaledVector(weightedRewardVector, data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector(), weightVector[objIndex]); - } + for(auto objIndex : unboundedObjectives) { + storm::utility::vector::addScaledVector(weightedRewardVector, getObjectiveRewardAsDiscreteActionRewards(objIndex), weightVector[objIndex]); } - unboundedWeightedPhase(unboundedObjectives, weightedRewardVector); + unboundedWeightedPhase(weightedRewardVector); STORM_LOG_DEBUG("Unbounded weighted phase result: " << weightedResult[data.preprocessedModel.getInitialStates().getNextSetIndex(0)] << " (value in initial state)."); unboundedIndividualPhase(weightVector); STORM_LOG_DEBUG("Unbounded individual phase results in initial state: " << getInitialStateResultOfObjectives<double>()); - boundedPhase(weightVector, ~unboundedObjectives, weightedRewardVector); - STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives<double>() << " ...WeightVectorChecker done."); + if(!this->unboundedObjectives.full()) { + boundedPhase(weightVector, weightedRewardVector); + STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives<double>() << " ...WeightVectorChecker done."); + } } template <class SparseModelType> @@ -63,16 +66,14 @@ namespace storm { template <class SparseModelType> storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker<SparseModelType>::getScheduler() const { - STORM_LOG_THROW(checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); - for(auto const& obj : data.objectives) { - STORM_LOG_THROW(!obj.timeBounds, storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives."); - } + STORM_LOG_THROW(this->checkHasBeenCalled, storm::exceptions::IllegalFunctionCallException, "Tried to retrieve results but check(..) has not been called before."); + STORM_LOG_THROW(this->unboundedObjectives.full(), storm::exceptions::NotImplementedException, "Scheduler retrival is not implemented for timeBounded objectives."); return scheduler; } template <class SparseModelType> - void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(storm::storage::BitVector const& unboundedObjectives, std::vector<ValueType> const& weightedRewardVector) { - if(unboundedObjectives.empty()) { + void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector) { + if(this->unboundedObjectives.empty()) { this->weightedResult = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>()); this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates()); return; @@ -145,79 +146,24 @@ namespace storm { //Also only compute values for objectives with weightVector != zero, //one check can be omitted as the result can be computed back from the weighed result and the results from the remaining objectives for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - if(data.objectives[objIndex].timeBounds){ - objectiveResults[objIndex] = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>()); - } else { - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector()); + if(unboundedObjectives.get(objIndex)){ + storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), getObjectiveRewardAsDiscreteActionRewards(objIndex)); storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); // As target states, we pick the states from which no reward is reachable. storm::storage::BitVector targetStates = ~storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); - + //TODO: we could give the solver some hint for the result (e.g., weightVector[ObjIndex] * weightedResult or (weightedResult - sum_i=0^objIndex-1 objectiveResult) * weightVector[objIndex]/ sum_i=objIndex^n weightVector[i] ) objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeReachabilityRewards(deterministicMatrix, - deterministicBackwardTransitions, - deterministicStateRewards, - targetStates, - false, //no qualitative checking, - linearEquationSolverFactory); - } - } - } - - template <class SparseModelType> - void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::boundedPhase(std::vector<ValueType> const& weightVector, storm::storage::BitVector const& boundedObjectives, std::vector<ValueType>& weightedRewardVector) { - if(boundedObjectives.empty()) { - return; - } - // Allocate some memory so this does not need to happen for each time epoch - std::vector<uint_fast64_t> optimalChoicesInCurrentEpoch(data.preprocessedModel.getNumberOfStates()); - std::vector<ValueType> choiceValues(weightedRewardVector.size()); - std::vector<ValueType> temporaryResult(data.preprocessedModel.getNumberOfStates()); - // Get for each occurring timeBound the indices of the objectives with that bound. - std::map<uint_fast64_t, storm::storage::BitVector, std::greater<uint_fast64_t>> timeBounds; - for(auto objIndex : boundedObjectives) { - uint_fast64_t timeBound = boost::get<uint_fast64_t>(data.objectives[objIndex].timeBounds.get()); - auto timeBoundIt = timeBounds.insert(std::make_pair(timeBound, storm::storage::BitVector(data.objectives.size(), false))).first; - timeBoundIt->second.set(objIndex); - } - storm::storage::BitVector objectivesAtCurrentEpoch = ~boundedObjectives; - auto timeBoundIt = timeBounds.begin(); - for(uint_fast64_t currentEpoch = timeBoundIt->first; currentEpoch > 0; --currentEpoch) { - if(timeBoundIt != timeBounds.end() && currentEpoch == timeBoundIt->first) { - objectivesAtCurrentEpoch |= timeBoundIt->second; - for(auto objIndex : timeBoundIt->second) { - storm::utility::vector::addScaledVector(weightedRewardVector, data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector(), weightVector[objIndex]); - } - ++timeBoundIt; - } - - // Get values and scheduler for weighted sum of objectives - data.preprocessedModel.getTransitionMatrix().multiplyWithVector(weightedResult, choiceValues); - storm::utility::vector::addVectors(choiceValues, weightedRewardVector, choiceValues); - storm::utility::vector::reduceVectorMax(choiceValues, weightedResult, data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), &optimalChoicesInCurrentEpoch); - - // get values for individual objectives - // TODO we could compute the result for one of the objectives from the weighted result, the given weight vector, and the remaining objective results. - for(auto objIndex : objectivesAtCurrentEpoch) { - std::vector<ValueType>& objectiveResult = objectiveResults[objIndex]; - std::vector<ValueType> const& objectiveRewards = data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector(); - auto rowGroupIndexIt = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin(); - auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin(); - for(ValueType& stateValue : temporaryResult){ - uint_fast64_t row = (*rowGroupIndexIt) + (*optimalChoiceIt); - ++rowGroupIndexIt; - ++optimalChoiceIt; - stateValue = objectiveRewards[row]; - for(auto const& entry : data.preprocessedModel.getTransitionMatrix().getRow(row)) { - stateValue += entry.getValue() * objectiveResult[entry.getColumn()]; - } - } - objectiveResult.swap(temporaryResult); + deterministicBackwardTransitions, + deterministicStateRewards, + targetStates, + false, //no qualitative checking, + linearEquationSolverFactory); + } else { + objectiveResults[objIndex] = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>()); } } } - - template class SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>; template std::vector<double> SparseMultiObjectiveWeightVectorChecker<storm::models::sparse::Mdp<double>>::getInitialStateResultOfObjectives<double>() const; diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h index c64749b25..f8e8af92e 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h @@ -43,15 +43,20 @@ namespace storm { storm::storage::TotalScheduler const& getScheduler() const; - private: + protected: + + /*! + * Retrieves the rewards for the objective with the given index as state action reward vector. + * Note that this discretizes state rewards of Markovian states by dividing them with the exit rate. + */ + virtual std::vector<ValueType> getObjectiveRewardAsDiscreteActionRewards(uint_fast64_t objectiveIndex) const = 0 ; /*! * Determines the scheduler that maximizes the weighted reward vector of the unbounded objectives * - * @param unboundedObjectives the objectives without a stepBound * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives) */ - void unboundedWeightedPhase(storm::storage::BitVector const& unboundedObjectives, std::vector<ValueType> const& weightedRewardVector); + void unboundedWeightedPhase(std::vector<ValueType> const& weightedRewardVector); /*! * Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase @@ -67,13 +72,14 @@ namespace storm { * - computes the values of these objectives w.r.t. this scheduler * * @param weightVector the weight vector of the current check - * @param boundedObjectives the objectives with a stepBound * @param weightedRewardVector the weighted rewards (initially only considering the unbounded objectives, will be extended to all objectives) */ - void boundedPhase(std::vector<ValueType> const& weightVector, storm::storage::BitVector const& unboundedObjectives, std::vector<ValueType>& weightedRewardVector); + virtual void boundedPhase(std::vector<ValueType> const& weightVector, std::vector<ValueType>& weightedRewardVector) = 0; // stores the considered information of the multi-objective model checking problem PreprocessorData const& data; + // stores the indices of the objectives for which there is no time bound + storm::storage::BitVector unboundedObjectives; // stores the set of states for which it is allowed to visit them infinitely often // This means that, if one of the states is part of a neutral EC, it is allowed to