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::check(preprocessorData); + std::shared_ptr> weightVectorChecker( new helper::SparseMaMultiObjectiveWeightVectorChecker(preprocessorData)); + auto resultData = helper::SparseMultiObjectiveHelper::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::check(preprocessorData); + std::shared_ptr> weightVectorChecker( new helper::SparseMdpMultiObjectiveWeightVectorChecker(preprocessorData)); + auto resultData = helper::SparseMultiObjectiveHelper::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 + SparseMaMultiObjectiveWeightVectorChecker::SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker(data) { + // Intentionally left empty + } + + template + std::vector::ValueType> SparseMaMultiObjectiveWeightVectorChecker::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 + void SparseMaMultiObjectiveWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& 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 optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates()); + std::vector choiceValues(weightedRewardVector.size()); + std::vector temporaryResult(this->data.preprocessedModel.getNumberOfStates()); + // Get for each occurring timeBound the indices of the objectives with that bound. + std::map> timeBounds; + storm::storage::BitVector boundedObjectives = ~this->unboundedObjectives; + for(uint_fast64_t objIndex : boundedObjectives) { + uint_fast64_t timeBound = boost::get(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& objectiveResult = this->objectiveResults[objIndex]; + std::vector 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>; +#ifdef STORM_HAVE_CARL + template class SparseMaMultiObjectiveWeightVectorChecker>; +#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 + +#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 SparseMaMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker { + public: + typedef typename SparseMaModelType::ValueType ValueType; + typedef SparseMultiObjectivePreprocessorData PreprocessorData; + + SparseMaMultiObjectiveWeightVectorChecker(PreprocessorData const& data); + + private: + + + /*! + * Retrieves the rewards for the objective with the given index as state action reward vector. + */ + virtual std::vector 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 const& weightVector, std::vector& 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 + SparseMdpMultiObjectiveWeightVectorChecker::SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : SparseMultiObjectiveWeightVectorChecker(data) { + // Intentionally left empty + } + + template + std::vector::ValueType> SparseMdpMultiObjectiveWeightVectorChecker::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 + void SparseMdpMultiObjectiveWeightVectorChecker::boundedPhase(std::vector const& weightVector, std::vector& weightedRewardVector) { + // Allocate some memory so this does not need to happen for each time epoch + std::vector optimalChoicesInCurrentEpoch(this->data.preprocessedModel.getNumberOfStates()); + std::vector choiceValues(weightedRewardVector.size()); + std::vector temporaryResult(this->data.preprocessedModel.getNumberOfStates()); + // Get for each occurring timeBound the indices of the objectives with that bound. + std::map> timeBounds; + storm::storage::BitVector boundedObjectives = ~this->unboundedObjectives; + for(uint_fast64_t objIndex : boundedObjectives) { + uint_fast64_t timeBound = boost::get(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& objectiveResult = this->objectiveResults[objIndex]; + std::vector 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>; +#ifdef STORM_HAVE_CARL + template class SparseMdpMultiObjectiveWeightVectorChecker>; +#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 + +#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 SparseMdpMultiObjectiveWeightVectorChecker : public SparseMultiObjectiveWeightVectorChecker { + public: + typedef typename SparseMdpModelType::ValueType ValueType; + typedef SparseMultiObjectivePreprocessorData PreprocessorData; + + SparseMdpMultiObjectiveWeightVectorChecker(PreprocessorData const& data); + + private: + + + /*! + * Retrieves the rewards for the objective with the given index as state action reward vector. + */ + virtual std::vector 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 const& weightVector, std::vector& 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 - typename SparseMultiObjectiveHelper::ResultData SparseMultiObjectiveHelper::check(PreprocessorData const& preprocessorData) { + typename SparseMultiObjectiveHelper::ResultData SparseMultiObjectiveHelper::check(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker) { ResultData resultData; resultData.overApproximation() = storm::storage::geometry::Polytope::createUniversalPolytope(); resultData.underApproximation() = storm::storage::geometry::Polytope::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 - void SparseMultiObjectiveHelper::achievabilityQuery(PreprocessorData const& preprocessorData, ResultData& resultData) { + void SparseMultiObjectiveHelper::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 weightVectorChecker(preprocessorData); do { WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked); performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData); @@ -80,7 +79,7 @@ namespace storm { } template - void SparseMultiObjectiveHelper::numericalQuery(PreprocessorData const& preprocessorData, ResultData& resultData) { + void SparseMultiObjectiveHelper::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 weightVectorChecker(preprocessorData); do { WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked); performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData); @@ -150,8 +148,7 @@ namespace storm { } template - void SparseMultiObjectiveHelper::paretoQuery(PreprocessorData const& preprocessorData, ResultData& resultData) { - SparseMultiObjectiveWeightVectorChecker weightVectorChecker(preprocessorData); + void SparseMultiObjectiveHelper::paretoQuery(PreprocessorData const& preprocessorData, WeightVectorCheckerType weightVectorChecker, ResultData& resultData) { //First consider the objectives individually for(uint_fast64_t objIndex = 0; objIndex()); @@ -228,13 +225,13 @@ namespace storm { } template - void SparseMultiObjectiveHelper::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker& weightVectorChecker, ResultData& result) { - weightVectorChecker.check(storm::utility::vector::convertNumericVector(direction)); - STORM_LOG_DEBUG("weighted objectives checker result is " << storm::utility::vector::convertNumericVector(weightVectorChecker.getInitialStateResultOfObjectives())); + void SparseMultiObjectiveHelper::performRefinementStep(WeightVector const& direction, bool saveScheduler, WeightVectorCheckerType weightVectorChecker, ResultData& result) { + weightVectorChecker->check(storm::utility::vector::convertNumericVector(direction)); + STORM_LOG_DEBUG("weighted objectives checker result is " << storm::utility::vector::convertNumericVector(weightVectorChecker->getInitialStateResultOfObjectives())); if(saveScheduler) { - result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives(), weightVectorChecker.getScheduler()); + result.refinementSteps().emplace_back(direction, weightVectorChecker->template getInitialStateResultOfObjectives(), weightVectorChecker->getScheduler()); } else { - result.refinementSteps().emplace_back(direction, weightVectorChecker.template getInitialStateResultOfObjectives()); + result.refinementSteps().emplace_back(direction, weightVectorChecker->template getInitialStateResultOfObjectives()); } 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 PreprocessorData; typedef SparseMultiObjectiveResultData ResultData; typedef SparseMultiObjectiveRefinementStep RefinementStep; + typedef std::shared_ptr> WeightVectorCheckerType; typedef std::vector Point; typedef std::vector 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& 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 - SparseMultiObjectiveWeightVectorChecker::SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data) : data(data), checkHasBeenCalled(false) , objectiveResults(data.objectives.size()){ + SparseMultiObjectiveWeightVectorChecker::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 void SparseMultiObjectiveWeightVectorChecker::check(std::vector const& weightVector) { checkHasBeenCalled=true; STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::convertNumericVector(weightVector)); - storm::storage::BitVector unboundedObjectives(data.objectives.size(), false); std::vector weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - 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()); - boundedPhase(weightVector, ~unboundedObjectives, weightedRewardVector); - STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives() << " ...WeightVectorChecker done."); + if(!this->unboundedObjectives.full()) { + boundedPhase(weightVector, weightedRewardVector); + STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives() << " ...WeightVectorChecker done."); + } } template @@ -63,16 +66,14 @@ namespace storm { template storm::storage::TotalScheduler const& SparseMultiObjectiveWeightVectorChecker::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 - void SparseMultiObjectiveWeightVectorChecker::unboundedWeightedPhase(storm::storage::BitVector const& unboundedObjectives, std::vector const& weightedRewardVector) { - if(unboundedObjectives.empty()) { + void SparseMultiObjectiveWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector) { + if(this->unboundedObjectives.empty()) { this->weightedResult = std::vector(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); 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(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); - } 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::computeReachabilityRewards(deterministicMatrix, - deterministicBackwardTransitions, - deterministicStateRewards, - targetStates, - false, //no qualitative checking, - linearEquationSolverFactory); - } - } - } - - template - void SparseMultiObjectiveWeightVectorChecker::boundedPhase(std::vector const& weightVector, storm::storage::BitVector const& boundedObjectives, std::vector& weightedRewardVector) { - if(boundedObjectives.empty()) { - return; - } - // Allocate some memory so this does not need to happen for each time epoch - std::vector optimalChoicesInCurrentEpoch(data.preprocessedModel.getNumberOfStates()); - std::vector choiceValues(weightedRewardVector.size()); - std::vector temporaryResult(data.preprocessedModel.getNumberOfStates()); - // Get for each occurring timeBound the indices of the objectives with that bound. - std::map> timeBounds; - for(auto objIndex : boundedObjectives) { - uint_fast64_t timeBound = boost::get(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& objectiveResult = objectiveResults[objIndex]; - std::vector 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(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); } } } - - template class SparseMultiObjectiveWeightVectorChecker>; template std::vector SparseMultiObjectiveWeightVectorChecker>::getInitialStateResultOfObjectives() 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 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 const& weightedRewardVector); + void unboundedWeightedPhase(std::vector 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 const& weightVector, storm::storage::BitVector const& unboundedObjectives, std::vector& weightedRewardVector); + virtual void boundedPhase(std::vector const& weightVector, std::vector& 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