diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp new file mode 100644 index 000000000..2c276dbc8 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp @@ -0,0 +1,81 @@ +#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" + +#include "storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + template + PcaaWeightVectorChecker::PcaaWeightVectorChecker(ModelType const& model, std::vector> const& objectives) : model(model), objectives(objectives) { + // Intentionally left empty + } + + template + void PcaaWeightVectorChecker::setWeightedPrecision(ValueType const& value) { + weightedPrecision = value; + } + + template + typename PcaaWeightVectorChecker::ValueType const& PcaaWeightVectorChecker::getWeightedPrecision() const { + return weightedPrecision; + } + + template + storm::storage::Scheduler::ValueType> PcaaWeightVectorChecker::computeScheduler() const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler generation is not supported in this setting."); + } + + template + template>::value, int>::type> + std::unique_ptr> WeightVectorCheckerFactory::create(ModelType const& model, + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) { + return std::make_unique>(model, objectives, possibleECActions, possibleBottomStates); + } + + template + template>::value, int>::type> + std::unique_ptr> WeightVectorCheckerFactory::create(ModelType const& model, + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) { + + return std::make_unique>(model, objectives, possibleECActions, possibleBottomStates); + } + + template + bool WeightVectorCheckerFactory::onlyCumulativeOrTotalRewardObjectives(std::vector> const& objectives) { + for (auto const& obj : objectives) { + if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula()))) { + return false; + } + } + return true; + } + + template class PcaaWeightVectorChecker>; + template class PcaaWeightVectorChecker>; + template class PcaaWeightVectorChecker>; + template class PcaaWeightVectorChecker>; + + template class WeightVectorCheckerFactory>; + template class WeightVectorCheckerFactory>; + template class WeightVectorCheckerFactory>; + template class WeightVectorCheckerFactory>; + + template std::unique_ptr>> WeightVectorCheckerFactory>::create(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates); + template std::unique_ptr>> WeightVectorCheckerFactory>::create(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates); + template std::unique_ptr>> WeightVectorCheckerFactory>::create(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates); + template std::unique_ptr>> WeightVectorCheckerFactory>::create(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates); + + + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h new file mode 100644 index 000000000..83896c236 --- /dev/null +++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h @@ -0,0 +1,105 @@ +#pragma once + +#include + +#include "storm/storage/Scheduler.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" +#include "storm/modelchecker/multiobjective/Objective.h" + + +namespace storm { + namespace modelchecker { + namespace multiobjective { + + /*! + * Helper Class that takes a weight vector and ... + * - computes the optimal value w.r.t. the weighted sum of the individual objectives + * - extracts the scheduler that induces this optimum + * - computes for each objective the value induced by this scheduler + */ + template + class PcaaWeightVectorChecker { + public: + typedef typename ModelType::ValueType ValueType; + + /* + * Creates a weight vector checker. + * + * @param objectives The (preprocessed) objectives + * + */ + + PcaaWeightVectorChecker(ModelType const& model, std::vector> const& objectives); + + virtual ~PcaaWeightVectorChecker() = default; + + virtual void check(std::vector const& weightVector) = 0; + + /*! + * Retrieves the results of the individual objectives at the initial state of the given model. + * Note that check(..) has to be called before retrieving results. Otherwise, an exception is thrown. + * Also note that there is no guarantee that the under/over approximation is in fact correct + * as long as the underlying solution methods are unsound (e.g., standard value iteration). + */ + virtual std::vector getUnderApproximationOfInitialStateResults() const = 0; + virtual std::vector getOverApproximationOfInitialStateResults() const = 0; + + /*! + * Sets the precision of this weight vector checker. After calling check() the following will hold: + * Let h_lower and h_upper be two hyperplanes such that + * * the normal vector is the provided weight-vector where the entry for minimizing objectives is negated + * * getUnderApproximationOfInitialStateResults() lies on h_lower and + * * getOverApproximationOfInitialStateResults() lies on h_upper. + * Then the distance between the two hyperplanes is at most weightedPrecision + */ + void setWeightedPrecision(ValueType const& value); + + /*! + * Returns the precision of this weight vector checker. + */ + ValueType const& getWeightedPrecision() const; + + /*! + * Retrieves a scheduler that induces the current values (if such a scheduler was generated). + * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. + */ + virtual storm::storage::Scheduler computeScheduler() const; + + + protected: + + // The (preprocessed) model + ModelType const& model; + // The (preprocessed) objectives + std::vector> const& objectives; + // The precision of this weight vector checker. + ValueType weightedPrecision; + + }; + + template + class WeightVectorCheckerFactory { + public: + + template>::value, int>::type = 0> + static std::unique_ptr> create(ModelType const& model, + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); + + template>::value, int>::type = 0> + static std::unique_ptr> create(ModelType const& model, + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); + private: + + static bool onlyCumulativeOrTotalRewardObjectives(std::vector> const& objectives); + }; + + } + } +} + diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index a978dc53c..63fa840e0 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -5,8 +5,6 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/multiobjective/Objective.h" -#include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h" -#include "storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/storage/geometry/Hyperrectangle.h" @@ -26,33 +24,13 @@ namespace storm { originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) { - initializeWeightVectorChecker(preprocessedModel, objectives, preprocessorResult.possibleECChoices, preprocessorResult.possibleBottomStates); + this->weightVectorChecker = WeightVectorCheckerFactory::create(preprocessedModel, objectives, preprocessorResult.possibleECChoices, preprocessorResult.possibleBottomStates); + this->diracWeightVectorsToBeChecked = storm::storage::BitVector(this->objectives.size(), true); this->overApproximation = storm::storage::geometry::Polytope::createUniversalPolytope(); this->underApproximation = storm::storage::geometry::Polytope::createEmptyPolytope(); } - template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); - } - - template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::Mdp const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); - } - - template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); - } - - template<> - void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, possibleECActions, possibleBottomStates)); - } - - template typename SparsePcaaQuery::WeightVector SparsePcaaQuery::findSeparatingVector(Point const& pointToBeSeparated) { STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(pointToBeSeparated)) << "."); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index b652af562..7a5588a3d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -3,7 +3,7 @@ #include "storm/modelchecker/results/CheckResult.h" #include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" #include "storm/storage/geometry/Polytope.h" namespace storm { @@ -39,14 +39,6 @@ namespace storm { protected: - /* - * Initializes the weight vector checker with the provided data from preprocessing - */ - void initializeWeightVectorChecker(SparseModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& possibleECActions, - storm::storage::BitVector const& possibleBottomStates); - /* * Represents the information obtained in a single iteration of the algorithm */ @@ -108,7 +100,7 @@ namespace storm { std::vector> objectives; // The corresponding weight vector checker - std::unique_ptr> weightVectorChecker; + std::unique_ptr> weightVectorChecker; //The results in each iteration of the algorithm std::vector refinementSteps; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 7333f6db6..fcc9fa1c6 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -28,10 +28,9 @@ namespace storm { std::vector> const& objectives, storm::storage::BitVector const& possibleECActions, storm::storage::BitVector const& possibleBottomStates) : - model(model), - objectives(objectives), + PcaaWeightVectorChecker(model, objectives), possibleECActions(possibleECActions), - actionsWithoutRewardInUnboundedPhase(model.getNumberOfChoices(), true), + actionsWithoutRewardInUnboundedPhase(this->model.getNumberOfChoices(), true), possibleBottomStates(possibleBottomStates), objectivesWithNoUpperTimeBound(objectives.size(), false), discreteActionRewards(objectives.size()), @@ -39,15 +38,15 @@ namespace storm { objectiveResults(objectives.size()), offsetsToUnderApproximation(objectives.size()), offsetsToOverApproximation(objectives.size()), - optimalChoices(model.getNumberOfStates(), 0) { + optimalChoices(this->model.getNumberOfStates(), 0) { // set data for unbounded objectives for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - auto const& formula = *objectives[objIndex].formula; + auto const& formula = *this->objectives[objIndex].formula; if (formula.getSubformula().isTotalRewardFormula()) { objectivesWithNoUpperTimeBound.set(objIndex, true); STORM_LOG_ASSERT(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), "Unexpected type of operator formula."); - actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()).getChoicesWithZeroReward(model.getTransitionMatrix()); + actionsWithoutRewardInUnboundedPhase &= this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()).getChoicesWithZeroReward(this->model.getTransitionMatrix()); } } } @@ -55,14 +54,14 @@ namespace storm { template void SparsePcaaWeightVectorChecker::check(std::vector const& weightVector) { - checkHasBeenCalled=true; + checkHasBeenCalled = true; STORM_LOG_INFO("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(weightVector))); - std::vector weightedRewardVector(model.getTransitionMatrix().getRowCount(), storm::utility::zero()); + std::vector weightedRewardVector(this->model.getTransitionMatrix().getRowCount(), storm::utility::zero()); boost::optional weightedLowerResultBound = storm::utility::zero(); boost::optional weightedUpperResultBound = storm::utility::zero(); for (auto objIndex : objectivesWithNoUpperTimeBound) { - auto const& obj = objectives[objIndex]; - if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) { + auto const& obj = this->objectives[objIndex]; + if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { if (obj.lowerResultBound && weightedUpperResultBound) { weightedUpperResultBound.get() -= weightVector[objIndex] * obj.lowerResultBound.get(); } else { @@ -103,17 +102,7 @@ namespace storm { // Validate that the results are sufficiently precise ValueType resultingWeightedPrecision = storm::utility::abs(storm::utility::vector::dotProduct(getOverApproximationOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getUnderApproximationOfInitialStateResults(), weightVector)); resultingWeightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weightVector, weightVector)); - STORM_LOG_THROW(resultingWeightedPrecision <= weightedPrecision, storm::exceptions::UnexpectedException, "The desired precision was not reached"); - } - - template - void SparsePcaaWeightVectorChecker::setWeightedPrecision(ValueType const& weightedPrecision) { - this->weightedPrecision = weightedPrecision; - } - - template - typename SparsePcaaWeightVectorChecker::ValueType const& SparsePcaaWeightVectorChecker::getWeightedPrecision() const { - return this->weightedPrecision; + STORM_LOG_THROW(resultingWeightedPrecision <= this->getWeightedPrecision(), storm::exceptions::UnexpectedException, "The desired precision was not reached"); } template @@ -160,24 +149,24 @@ namespace storm { void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector, boost::optional const& lowerResultBound, boost::optional const& upperResultBound) { if (this->objectivesWithNoUpperTimeBound.empty() || !storm::utility::vector::hasNonZeroEntry(weightedRewardVector)) { - this->weightedResult = std::vector(model.getNumberOfStates(), storm::utility::zero()); - this->optimalChoices = std::vector(model.getNumberOfStates(), 0); + this->weightedResult = std::vector(this->model.getNumberOfStates(), storm::utility::zero()); + this->optimalChoices = std::vector(this->model.getNumberOfStates(), 0); return; } // Only consider the states from which a transition with non-zero reward is reachable. (The remaining states always have reward zero). storm::storage::BitVector zeroRewardActions = storm::utility::vector::filterZero(weightedRewardVector); storm::storage::BitVector nonZeroRewardActions = ~zeroRewardActions; - storm::storage::BitVector nonZeroRewardStates(model.getNumberOfStates(), false); - for(uint_fast64_t state = 0; state < model.getNumberOfStates(); ++state){ - if(nonZeroRewardActions.getNextSetIndex(model.getTransitionMatrix().getRowGroupIndices()[state]) < model.getTransitionMatrix().getRowGroupIndices()[state+1]) { + storm::storage::BitVector nonZeroRewardStates(this->model.getNumberOfStates(), false); + for(uint_fast64_t state = 0; state < this->model.getNumberOfStates(); ++state){ + if(nonZeroRewardActions.getNextSetIndex(this->model.getTransitionMatrix().getRowGroupIndices()[state]) < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) { nonZeroRewardStates.set(state); } } - storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix().transpose(true), storm::storage::BitVector(model.getNumberOfStates(), true), nonZeroRewardStates); + storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(this->model.getTransitionMatrix().transpose(true), storm::storage::BitVector(this->model.getNumberOfStates(), true), nonZeroRewardStates); // Remove neutral end components, i.e., ECs in which no reward is earned. - auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates); + auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(this->model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates); std::vector subRewardVector(ecEliminatorResult.newToOldRowMapping.size()); storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector); @@ -195,7 +184,7 @@ namespace storm { } solver->solveEquations(subResult, subRewardVector); - this->weightedResult = std::vector(model.getNumberOfStates()); + this->weightedResult = std::vector(this->model.getNumberOfStates()); transformReducedSolutionToOriginalModel(ecEliminatorResult.matrix, subResult, solver->getSchedulerChoices(), ecEliminatorResult.newToOldRowMapping, ecEliminatorResult.oldToNewStateMapping, this->weightedResult, this->optimalChoices); } @@ -205,16 +194,16 @@ namespace storm { if (objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { uint_fast64_t objIndex = *objectivesWithNoUpperTimeBound.begin(); objectiveResults[objIndex] = weightedResult; - if (storm::solver::minimize(objectives[objIndex].formula->getOptimalityType())) { + if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) { storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one()); } - for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) { + for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) { if (objIndex != objIndex2) { - objectiveResults[objIndex2] = std::vector(model.getNumberOfStates(), storm::utility::zero()); + objectiveResults[objIndex2] = std::vector(this->model.getNumberOfStates(), storm::utility::zero()); } } } else { - storm::storage::SparseMatrix deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->optimalChoices, true); + storm::storage::SparseMatrix deterministicMatrix = this->model.getTransitionMatrix().selectRowsFromRowGroups(this->optimalChoices, true); storm::storage::SparseMatrix deterministicBackwardTransitions = deterministicMatrix.transpose(); std::vector deterministicStateRewards(deterministicMatrix.getRowCount()); storm::solver::GeneralLinearEquationSolverFactory linearEquationSolverFactory; @@ -225,11 +214,11 @@ namespace storm { ValueType sumOfWeightsOfUncheckedObjectives = storm::utility::vector::sum_if(weightVector, objectivesWithNoUpperTimeBound); for (uint_fast64_t const &objIndex : storm::utility::vector::getSortedIndices(weightVector)) { - auto const& obj = objectives[objIndex]; + auto const& obj = this->objectives[objIndex]; if (objectivesWithNoUpperTimeBound.get(objIndex)) { offsetsToUnderApproximation[objIndex] = storm::utility::zero(); offsetsToOverApproximation[objIndex] = storm::utility::zero(); - storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); + storm::utility::vector::selectVectorValues(deterministicStateRewards, this->optimalChoices, this->model.getTransitionMatrix().getRowGroupIndices(), discreteActionRewards[objIndex]); storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); // As maybestates we pick the states from which a state with reward is reachable storm::storage::BitVector maybeStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); @@ -245,7 +234,7 @@ namespace storm { storm::utility::vector::clip(objectiveResults[objIndex], obj.lowerResultBound, obj.upperResultBound); } // Make sure that the objectiveResult is initialized correctly - objectiveResults[objIndex].resize(model.getNumberOfStates(), storm::utility::zero()); + objectiveResults[objIndex].resize(this->model.getNumberOfStates(), storm::utility::zero()); if (!maybeStates.empty()) { storm::storage::SparseMatrix submatrix = deterministicMatrix.getSubmatrix( @@ -279,7 +268,7 @@ namespace storm { sumOfWeightsOfUncheckedObjectives -= weightVector[objIndex]; } } else { - objectiveResults[objIndex] = std::vector(model.getNumberOfStates(), storm::utility::zero()); + objectiveResults[objIndex] = std::vector(this->model.getNumberOfStates(), storm::utility::zero()); } } } @@ -294,13 +283,13 @@ namespace storm { std::vector& originalSolution, std::vector& originalOptimalChoices) const { - storm::storage::BitVector bottomStates(model.getTransitionMatrix().getRowGroupCount(), false); - storm::storage::BitVector statesThatShouldStayInTheirEC(model.getTransitionMatrix().getRowGroupCount(), false); - storm::storage::BitVector statesWithUndefSched(model.getTransitionMatrix().getRowGroupCount(), false); + storm::storage::BitVector bottomStates(this->model.getTransitionMatrix().getRowGroupCount(), false); + storm::storage::BitVector statesThatShouldStayInTheirEC(this->model.getTransitionMatrix().getRowGroupCount(), false); + storm::storage::BitVector statesWithUndefSched(this->model.getTransitionMatrix().getRowGroupCount(), false); // Handle all the states for which the choice in the original model is uniquely given by the choice in the reduced model // Also store some information regarding the remaining states - for(uint_fast64_t state = 0; state < model.getTransitionMatrix().getRowGroupCount(); ++state) { + for(uint_fast64_t state = 0; state < this->model.getTransitionMatrix().getRowGroupCount(); ++state) { // Check if the state exists in the reduced model, i.e., the mapping retrieves a valid index uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state]; if(stateInReducedModel < reducedMatrix.getRowGroupCount()) { @@ -309,7 +298,7 @@ namespace storm { uint_fast64_t chosenRowInOriginalModel = reducedToOriginalChoiceMapping[chosenRowInReducedModel]; // Check if the state is a bottom state, i.e., the chosen row stays inside its EC. bool stateIsBottom = possibleBottomStates.get(state); - for(auto const& entry : model.getTransitionMatrix().getRow(chosenRowInOriginalModel)) { + for(auto const& entry : this->model.getTransitionMatrix().getRow(chosenRowInOriginalModel)) { stateIsBottom &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; } if(stateIsBottom) { @@ -317,9 +306,9 @@ namespace storm { statesThatShouldStayInTheirEC.set(state); } else { // Check if the chosen row originaly belonged to the current state (and not to another state of the EC) - if(chosenRowInOriginalModel >= model.getTransitionMatrix().getRowGroupIndices()[state] && - chosenRowInOriginalModel < model.getTransitionMatrix().getRowGroupIndices()[state+1]) { - originalOptimalChoices[state] = chosenRowInOriginalModel - model.getTransitionMatrix().getRowGroupIndices()[state]; + if(chosenRowInOriginalModel >= this->model.getTransitionMatrix().getRowGroupIndices()[state] && + chosenRowInOriginalModel < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]) { + originalOptimalChoices[state] = chosenRowInOriginalModel - this->model.getTransitionMatrix().getRowGroupIndices()[state]; } else { statesWithUndefSched.set(state); statesThatShouldStayInTheirEC.set(state); @@ -344,16 +333,16 @@ namespace storm { // Find a row with zero rewards that only leads to bottom states. // If the state should stay in its EC, we also need to make sure that all successors map to the same state in the reduced model uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state]; - for(uint_fast64_t row = model.getTransitionMatrix().getRowGroupIndices()[state]; row < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { + for(uint_fast64_t row = this->model.getTransitionMatrix().getRowGroupIndices()[state]; row < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { bool rowOnlyLeadsToBottomStates = true; bool rowStaysInEC = true; - for( auto const& entry : model.getTransitionMatrix().getRow(row)) { + for( auto const& entry : this->model.getTransitionMatrix().getRow(row)) { rowOnlyLeadsToBottomStates &= bottomStates.get(entry.getColumn()); rowStaysInEC &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; } if(rowOnlyLeadsToBottomStates && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state)) && actionsWithoutRewardInUnboundedPhase.get(row)) { foundRowForState = true; - originalOptimalChoices[state] = row - model.getTransitionMatrix().getRowGroupIndices()[state]; + originalOptimalChoices[state] = row - this->model.getTransitionMatrix().getRowGroupIndices()[state]; break; } } @@ -365,15 +354,15 @@ namespace storm { for(auto state : statesWithUndefSched) { // Iteratively Try to find a choice such that at least one successor has a defined scheduler. uint_fast64_t stateInReducedModel = originalToReducedStateMapping[state]; - for(uint_fast64_t row = model.getTransitionMatrix().getRowGroupIndices()[state]; row < model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { + for(uint_fast64_t row = this->model.getTransitionMatrix().getRowGroupIndices()[state]; row < this->model.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { bool rowStaysInEC = true; bool rowLeadsToDefinedScheduler = false; - for(auto const& entry : model.getTransitionMatrix().getRow(row)) { + for(auto const& entry : this->model.getTransitionMatrix().getRow(row)) { rowStaysInEC &= ( stateInReducedModel == originalToReducedStateMapping[entry.getColumn()]); rowLeadsToDefinedScheduler |= !statesWithUndefSched.get(entry.getColumn()); } if(rowLeadsToDefinedScheduler && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state))) { - originalOptimalChoices[state] = row - model.getTransitionMatrix().getRowGroupIndices()[state]; + originalOptimalChoices[state] = row - this->model.getTransitionMatrix().getRowGroupIndices()[state]; statesWithUndefSched.set(state, false); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index 3cf75c83b..8eaf8a892 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -1,11 +1,10 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAWEIGHTVECTORCHECKER_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAWEIGHTVECTORCHECKER_H_ - +#pragma once #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/Scheduler.h" #include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" #include "storm/utility/vector.h" namespace storm { @@ -19,7 +18,7 @@ namespace storm { * - computes for each objective the value induced by this scheduler */ template - class SparsePcaaWeightVectorChecker { + class SparsePcaaWeightVectorChecker : public PcaaWeightVectorChecker { public: typedef typename SparseModelType::ValueType ValueType; @@ -45,7 +44,7 @@ namespace storm { * - extracts the scheduler that induces this optimum * - computes for each objective the value induced by this scheduler */ - void check(std::vector const& weightVector); + virtual void check(std::vector const& weightVector) override; /*! * Retrieves the results of the individual objectives at the initial state of the given model. @@ -53,31 +52,15 @@ namespace storm { * Also note that there is no guarantee that the under/over approximation is in fact correct * as long as the underlying solution methods are unsound (e.g., standard value iteration). */ - std::vector getUnderApproximationOfInitialStateResults() const; - std::vector getOverApproximationOfInitialStateResults() const; - - - /*! - * Sets the precision of this weight vector checker. After calling check() the following will hold: - * Let h_lower and h_upper be two hyperplanes such that - * * the normal vector is the provided weight-vector where the entry for minimizing objectives is negated - * * getUnderApproximationOfInitialStateResults() lies on h_lower and - * * getOverApproximationOfInitialStateResults() lies on h_upper. - * Then the distance between the two hyperplanes is at most weightedPrecision - */ - void setWeightedPrecision(ValueType const& weightedPrecision); - - /*! - * Returns the precision of this weight vector checker. - */ - ValueType const& getWeightedPrecision() const; + virtual std::vector getUnderApproximationOfInitialStateResults() const override; + virtual std::vector getOverApproximationOfInitialStateResults() const override; /*! * Retrieves a scheduler that induces the current values * Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown. * Also note that (currently) the scheduler only supports unbounded objectives. */ - storm::storage::Scheduler computeScheduler() const; + virtual storm::storage::Scheduler computeScheduler() const override; protected: @@ -118,10 +101,6 @@ namespace storm { std::vector& originalSolution, std::vector& originalOptimalChoices) const; - // The (preprocessed) model - SparseModelType const& model; - // The (preprocessed) objectives - std::vector> const& objectives; // Overapproximation of the set of choices that are part of an end component. storm::storage::BitVector possibleECActions; @@ -135,8 +114,6 @@ namespace storm { storm::storage::BitVector objectivesWithNoUpperTimeBound; // stores the (discretized) state action rewards for each objective. std::vector> discreteActionRewards; - // stores the precision of this weight vector checker. - ValueType weightedPrecision; // Memory for the solution of the most recent call of check(..) // becomes true after the first call of check(..) bool checkHasBeenCalled; @@ -157,4 +134,3 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAWEIGHTVECTORCHECKER_H_ */