From 725e0e12e76e0f52afc6fb8c2cf91b53b02f619a Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 3 May 2017 00:49:15 +0200 Subject: [PATCH] replaced old pcaa preprocessor with the refactored preprocessor. --- .../modelchecker/multiobjective/pcaa.cpp | 10 +- .../multiobjective/pcaa/PcaaObjective.h | 72 --- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 39 +- .../pcaa/SparseMaPcaaWeightVectorChecker.h | 7 +- .../pcaa/SparseMdpPcaaWeightVectorChecker.cpp | 26 +- .../pcaa/SparseMdpPcaaWeightVectorChecker.h | 17 +- .../pcaa/SparsePcaaAchievabilityQuery.cpp | 21 +- .../pcaa/SparsePcaaAchievabilityQuery.h | 2 +- .../pcaa/SparsePcaaParetoQuery.cpp | 4 +- .../pcaa/SparsePcaaParetoQuery.h | 2 +- .../pcaa/SparsePcaaPreprocessor.cpp | 447 ------------------ .../pcaa/SparsePcaaPreprocessor.h | 82 ---- .../pcaa/SparsePcaaPreprocessorReturnType.h | 93 ---- .../pcaa/SparsePcaaQuantitativeQuery.cpp | 82 ++-- .../pcaa/SparsePcaaQuantitativeQuery.h | 2 +- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 65 ++- .../multiobjective/pcaa/SparsePcaaQuery.h | 14 +- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 126 +++-- .../pcaa/SparsePcaaWeightVectorChecker.h | 28 +- 19 files changed, 284 insertions(+), 855 deletions(-) delete mode 100644 src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h delete mode 100644 src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp delete mode 100644 src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h delete mode 100644 src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h diff --git a/src/storm/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp index 6019c19cd..c07ea26a1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa.cpp @@ -5,7 +5,7 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" @@ -34,7 +34,7 @@ namespace storm { STORM_LOG_THROW(dynamic_cast const *>(&model)->isClosed(), storm::exceptions::InvalidArgumentException, "Unable to check multi-objective formula on non-closed Markov automaton."); } - auto preprocessorResult = SparsePcaaPreprocessor::preprocess(model, formula); + auto preprocessorResult = SparseMultiObjectivePreprocessor::preprocess(model, formula); swPreprocessing.stop(); if (storm::settings::getModule().isShowStatisticsSet()) { STORM_PRINT_AND_LOG("Preprocessing done in " << swPreprocessing << " seconds." << std::endl << " Result: " << preprocessorResult << std::endl); @@ -44,13 +44,13 @@ namespace storm { storm::utility::Stopwatch swValueIterations(true); std::unique_ptr> query; switch (preprocessorResult.queryType) { - case SparsePcaaPreprocessorReturnType::QueryType::Achievability: + case SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability: query = std::unique_ptr> (new SparsePcaaAchievabilityQuery(preprocessorResult)); break; - case SparsePcaaPreprocessorReturnType::QueryType::Quantitative: + case SparseMultiObjectivePreprocessorReturnType::QueryType::Quantitative: query = std::unique_ptr> (new SparsePcaaQuantitativeQuery(preprocessorResult)); break; - case SparsePcaaPreprocessorReturnType::QueryType::Pareto: + case SparseMultiObjectivePreprocessorReturnType::QueryType::Pareto: query = std::unique_ptr> (new SparsePcaaParetoQuery(preprocessorResult)); break; default: diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h deleted file mode 100644 index ac0043fae..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa/PcaaObjective.h +++ /dev/null @@ -1,72 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_PCAAOBJECTIVE_H_ - -#include -#include - -#include "storm/logic/Formulas.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - template - struct PcaaObjective { - // the original input formula - std::shared_ptr originalFormula; - - // the name of the considered reward model in the preprocessedModel - std::string rewardModelName; - - // true if all rewards for this objective are positive, false if all rewards are negative. - bool rewardsArePositive; - - // transformation from the values of the preprocessed model to the ones for the actual input model, i.e., - // x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model - ValueType toOriginalValueTransformationFactor; - ValueType toOriginalValueTransformationOffset; - - // The probability/reward threshold for the preprocessed model (if originalFormula specifies one). - // This is always a lower bound. - boost::optional threshold; - // True iff the specified threshold is strict, i.e., > - bool thresholdIsStrict = false; - - // The time bound(s) for the formula (if given by the originalFormula) - boost::optional lowerTimeBound; - boost::optional upperTimeBound; - bool lowerTimeBoundStrict = false; - bool upperTimeBoundStrict = false; - - void printToStream(std::ostream& out) const { - out << std::setw(30) << originalFormula->toString(); - out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t"; - out << "intern threshold:"; - if(threshold){ - out << (thresholdIsStrict ? " >" : ">="); - out << std::setw(5) << (*threshold) << ","; - } else { - out << " none,"; - } - out << " \t"; - out << "intern reward model: " << std::setw(10) << rewardModelName; - out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t"; - out << "time bounds:"; - if(lowerTimeBound) { - if(upperTimeBound) { - out << (lowerTimeBoundStrict ? "(" : "[") << *lowerTimeBound << ", " << *upperTimeBound << (upperTimeBoundStrict ? ")" : "]"); - } else { - out << (lowerTimeBoundStrict ? " >" : ">=") << std::setw(5) << *lowerTimeBound; - } - } else if (upperTimeBound) { - out << (upperTimeBoundStrict ? " <" : "<=") << std::setw(5) << *upperTimeBound; - } else { - out << " none"; - } - out << ")" << std::endl; - } - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_OBJECTIVE_H_ */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index e2cce333d..0a3beeabe 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -15,17 +15,17 @@ namespace storm { namespace modelchecker { namespace multiobjective { + template SparseMaPcaaWeightVectorChecker::SparseMaPcaaWeightVectorChecker(SparseMaModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates) : - SparsePcaaWeightVectorChecker(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates) { + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) : + SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { // Set the (discretized) state action rewards. this->discreteActionRewards.resize(objectives.size()); for(auto objIndex : this->objectivesWithNoUpperTimeBound) { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.hasStateActionRewards() ? rewModel.getStateActionRewardVector() : std::vector(this->model.getTransitionMatrix().getRowCount(), storm::utility::zero()); if(rewModel.hasStateRewards()) { @@ -119,7 +119,7 @@ namespace storm { if(this->objectivesWithNoUpperTimeBound.get(objIndex)) { storm::utility::vector::selectVectorValues(objVector, result.choices, this->discreteActionRewards[objIndex]); } else { - typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); + typename SparseMaModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Preprocessed Reward model has transition rewards which is not expected."); STORM_LOG_ASSERT(!rewModel.hasStateRewards(), "State rewards for bounded objectives for MAs are not expected (bounded rewards are not supported)."); if(rewModel.hasStateActionRewards()) { @@ -160,8 +160,8 @@ namespace storm { VT smallestNonZeroBound = storm::utility::zero(); for(auto const& obj : this->objectives) { if(obj.upperTimeBound){ - STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << *obj.upperTimeBound << " contains undefined variables"); - timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational())); + STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidOperationException, "The time bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); + timeBounds.push_back(storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational())); STORM_LOG_ASSERT(!storm::utility::isZero(timeBounds.back()), "Got zero-valued upper time bound."); eToPowerOfMinusMaxRateTimesBound.push_back(std::exp(-maxRate * timeBounds.back())); smallestNonZeroBound = storm::utility::isZero(smallestNonZeroBound) ? timeBounds.back() : std::min(smallestNonZeroBound, timeBounds.back()); @@ -259,7 +259,7 @@ namespace storm { VT errorTowardsZero = storm::utility::zero(); VT errorAwayFromZero = storm::utility::zero(); if(obj.upperTimeBound) { - VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->evaluateAsRational()); + VT timeBound = storm::utility::convertNumber(obj.upperTimeBound->getBound().evaluateAsRational()); uint_fast64_t digitizedBound = storm::utility::convertNumber(timeBound/digitizationConstant); auto timeBoundIt = upperTimeBounds.insert(std::make_pair(digitizedBound, storm::storage::BitVector(this->objectives.size(), false))).first; timeBoundIt->second.set(objIndex); @@ -267,7 +267,7 @@ namespace storm { digitizationError -= std::exp(-maxRate * timeBound) * storm::utility::pow(storm::utility::one() + maxRate * digitizationConstant, digitizedBound); errorAwayFromZero += digitizationError; } - if (obj.rewardsArePositive) { + if (storm::solver::maximize(obj.optimizationDirection)) { this->offsetsToLowerBound[objIndex] = -errorTowardsZero; this->offsetsToUpperBound[objIndex] = errorAwayFromZero; } else { @@ -314,8 +314,9 @@ namespace storm { consideredObjectives |= upperTimeBoundIt->second; for(auto objIndex : upperTimeBoundIt->second) { // This objective now plays a role in the weighted sum - storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], weightVector[objIndex]); - storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], weightVector[objIndex]); + ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + storm::utility::vector::addScaledVector(MS.weightedRewardVector, MS.objectiveRewardVectors[objIndex], factor); + storm::utility::vector::addScaledVector(PS.weightedRewardVector, PS.objectiveRewardVectors[objIndex], factor); } ++upperTimeBoundIt; } @@ -334,6 +335,9 @@ namespace storm { // In this case there is no need to perform the computation on the individual objectives optimalChoicesAtCurrentEpoch = newScheduler->getChoices(); PS.objectiveSolutionVectors[*consideredObjectives.begin()] = PS.weightedSolutionVector; + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); + } } else { // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed if(linEq.solver == nullptr || newScheduler->getChoices() != optimalChoicesAtCurrentEpoch) { @@ -378,6 +382,9 @@ namespace storm { if(consideredObjectives.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*consideredObjectives.begin()])) { // In this case there is no need to perform the computation on the individual objectives MS.objectiveSolutionVectors[*consideredObjectives.begin()] = MS.weightedSolutionVector; + if (storm::solver::minimize(this->objectives[*consideredObjectives.begin()].optimizationDirection)) { + storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[*consideredObjectives.begin()], -storm::utility::one()); + } } else { for(auto objIndex : consideredObjectives) { MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues); @@ -393,12 +400,6 @@ namespace storm { template double SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, double const& digitizationConstant) const; template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds( SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); -#ifdef STORM_HAVE_CARL -// template class SparseMaPcaaWeightVectorChecker>; - // template storm::RationalNumber SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; - // template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; -// template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); -#endif } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index 827f1701e..559882c9a 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h @@ -26,10 +26,9 @@ namespace storm { typedef typename SparseMaModelType::ValueType ValueType; SparseMaPcaaWeightVectorChecker(SparseMaModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); virtual ~SparseMaPcaaWeightVectorChecker() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index a6dc7a3b4..f41e4c621 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -14,14 +14,13 @@ namespace storm { template SparseMdpPcaaWeightVectorChecker::SparseMdpPcaaWeightVectorChecker(SparseMdpModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates) : - SparsePcaaWeightVectorChecker(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates) { + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) : + SparsePcaaWeightVectorChecker(model, objectives, possibleECActions, possibleBottomStates) { // set the state action rewards for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(this->objectives[objIndex].rewardModelName); + typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(*this->objectives[objIndex].rewardModelName); STORM_LOG_ASSERT(!rewModel.hasTransitionRewards(), "Reward model has transition rewards which is not expected."); this->discreteActionRewards[objIndex] = rewModel.getTotalRewardVector(this->model.getTransitionMatrix()); } @@ -33,16 +32,15 @@ namespace storm { std::vector optimalChoicesInCurrentEpoch(this->model.getNumberOfStates()); std::vector choiceValues(weightedRewardVector.size()); std::vector temporaryResult(this->model.getNumberOfStates()); - std::vector zeroReward(weightedRewardVector.size(), storm::utility::zero()); // Get for each occurring timeBound the indices of the objectives with that bound. std::map> stepBounds; for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& obj = this->objectives[objIndex]; STORM_LOG_THROW(!obj.lowerTimeBound, storm::exceptions::InvalidPropertyException, "Lower step bounds are not supported by this model checker"); if (obj.upperTimeBound) { - STORM_LOG_THROW(!obj.upperTimeBound->containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << * obj.upperTimeBound << " contains undefined variables"); - uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->evaluateAsInt(); - if (obj.upperTimeBoundStrict) { + STORM_LOG_THROW(!obj.upperTimeBound->getBound().containsVariables(), storm::exceptions::InvalidPropertyException, "The step bound '" << obj.upperTimeBound->getBound() << " contains undefined variables"); + uint_fast64_t stepBound = (uint_fast64_t) obj.upperTimeBound->getBound().evaluateAsInt(); + if (obj.upperTimeBound->isStrict()) { --stepBound; } auto stepBoundIt = stepBounds.insert(std::make_pair(stepBound, storm::storage::BitVector(this->objectives.size(), false))).first; @@ -57,9 +55,6 @@ namespace storm { // Stores the objectives for which we need to compute values in the current time epoch. storm::storage::BitVector consideredObjectives = this->objectivesWithNoUpperTimeBound; - // Stores objectives for which the current epoch passed their lower bound - storm::storage::BitVector lowerBoundViolatedObjectives(consideredObjectives.size(), false); - auto stepBoundIt = stepBounds.begin(); uint_fast64_t currentEpoch = stepBounds.empty() ? 0 : stepBoundIt->first; @@ -69,7 +64,8 @@ namespace storm { consideredObjectives |= stepBoundIt->second; for(auto objIndex : stepBoundIt->second) { // This objective now plays a role in the weighted sum - storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], weightVector[objIndex]); + ValueType factor = storm::solver::minimize(this->objectives[objIndex].optimizationDirection) ? -weightVector[objIndex] : weightVector[objIndex]; + storm::utility::vector::addScaledVector(weightedRewardVector, this->discreteActionRewards[objIndex], factor); } ++stepBoundIt; } @@ -83,7 +79,7 @@ namespace storm { // 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 : consideredObjectives) { std::vector& objectiveResult = this->objectiveResults[objIndex]; - std::vector const& objectiveRewards = lowerBoundViolatedObjectives.get(objIndex) ? zeroReward : this->discreteActionRewards[objIndex]; + std::vector const& objectiveRewards = this->discreteActionRewards[objIndex]; auto rowGroupIndexIt = this->model.getTransitionMatrix().getRowGroupIndices().begin(); auto optimalChoiceIt = optimalChoicesInCurrentEpoch.begin(); for(ValueType& stateValue : temporaryResult){ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h index 8b56386c9..91cb862f1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h @@ -20,11 +20,20 @@ namespace storm { public: typedef typename SparseMdpModelType::ValueType ValueType; + /* + * Creates a weight vextor checker. + * + * @param model The (preprocessed) model + * @param objectives The (preprocessed) objectives + * @param possibleECActions Overapproximation of the actions that are part of an EC + * @param possibleBottomStates The states for which it is posible to not collect further reward with prob. 1 + * + */ + SparseMdpPcaaWeightVectorChecker(SparseMdpModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); virtual ~SparseMdpPcaaWeightVectorChecker() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index fec46a006..052e59007 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -7,18 +7,20 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings//SettingsManager.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/MultiObjectiveSettings.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace modelchecker { namespace multiobjective { template - SparsePcaaAchievabilityQuery::SparsePcaaAchievabilityQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparsePcaaPreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); + SparsePcaaAchievabilityQuery::SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Achievability, "Invalid query Type"); initializeThresholdData(); // Set the precision of the weight vector checker. Will be refined during the computation @@ -30,8 +32,17 @@ namespace storm { thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - thresholds.push_back(storm::utility::convertNumber(*this->objectives[objIndex].threshold)); - strictThresholds.set(objIndex, this->objectives[objIndex].thresholdIsStrict); + auto const& obj = this->objectives[objIndex]; + STORM_LOG_ASSERT(obj.bound.is_initialized(), "Achievability query invoked but there is an objective without bound."); + STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); + thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); + if (storm::solver::minimize(obj.optimizationDirection)) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. + // Hence, we also negate the threshold + thresholds.back() *= -storm::utility::one(); + } + strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h index c250f257b..fe455e457 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h @@ -23,7 +23,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaAchievabilityQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); virtual ~SparsePcaaAchievabilityQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 9caf36d04..8961c2dc4 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -17,8 +17,8 @@ namespace storm { namespace multiobjective { template - SparsePcaaParetoQuery::SparsePcaaParetoQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparsePcaaPreprocessorReturnType::QueryType::Pareto, "Invalid query Type"); + SparsePcaaParetoQuery::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType::QueryType::Pareto, "Invalid query Type"); // Set the precision of the weight vector checker typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber(storm::settings::getModule().getPrecision()); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h index b6361faff..ffcf7bb3d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h @@ -23,7 +23,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaParetoQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); virtual ~SparsePcaaParetoQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp deleted file mode 100644 index abc37571c..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ /dev/null @@ -1,447 +0,0 @@ -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h" - -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" -#include "storm/storage/MaximalEndComponentDecomposition.h" -#include "storm/storage/memorystructure/MemoryStructureBuilder.h" -#include "storm/storage/memorystructure/SparseModelMemoryProduct.h" -#include "storm/transformer/SubsystemBuilder.h" -#include "storm/utility/macros.h" -#include "storm/utility/vector.h" -#include "storm/utility/graph.h" - -#include "storm/exceptions/InvalidPropertyException.h" -#include "storm/exceptions/UnexpectedException.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - template - typename SparsePcaaPreprocessor::ReturnType SparsePcaaPreprocessor::preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) { - - ReturnType result(originalFormula, originalModel, SparseModelType(originalModel)); - result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, originalModel.getNumberOfStates()); - - //Invoke preprocessing on the individual objectives - for (auto const& subFormula : originalFormula.getSubformulas()){ - STORM_LOG_INFO("Preprocessing objective " << *subFormula<< "."); - result.objectives.emplace_back(); - PcaaObjective& currentObjective = result.objectives.back(); - currentObjective.originalFormula = subFormula; - if (currentObjective.originalFormula->isOperatorFormula()) { - preprocessOperatorFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); - } - } - // Set the query type. In case of a quantitative query, also set the index of the objective to be optimized. - // Note: If there are only zero (or one) objectives left, we should not consider a pareto query! - storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size()); - for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { - objectivesWithoutThreshold.set(objIndex, !result.objectives[objIndex].threshold); - } - uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits(); - if (numOfObjectivesWithoutThreshold == 0) { - result.queryType = ReturnType::QueryType::Achievability; - } else if (numOfObjectivesWithoutThreshold == 1) { - result.queryType = ReturnType::QueryType::Quantitative; - result.indexOfOptimizingObjective = objectivesWithoutThreshold.getNextSetIndex(0); - } else if (numOfObjectivesWithoutThreshold == result.objectives.size()) { - result.queryType = ReturnType::QueryType::Pareto; - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievability query), 1 (quantitative query), or " << result.objectives.size() << " (Pareto Query). Got " << numOfObjectivesWithoutThreshold << " instead."); - } - - //We can remove the original reward models to save some memory - std::set origRewardModels = originalFormula.getReferencedRewardModels(); - for (auto const& rewModel : origRewardModels){ - result.preprocessedModel.removeRewardModel(rewModel); - } - - //Get actions to which a positive or negative reward is assigned for at least one objective - result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); - result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); - for (uint_fast64_t objIndex = 0; objIndex < result.objectives.size(); ++objIndex) { - if (!result.objectives[objIndex].upperTimeBound) { - if (result.objectives[objIndex].rewardsArePositive) { - result.actionsWithPositiveReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); - } else { - result.actionsWithNegativeReward |= ~storm::utility::vector::filterZero(result.preprocessedModel.getRewardModel(result.objectives[objIndex].rewardModelName).getTotalRewardVector(result.preprocessedModel.getTransitionMatrix())); - } - } - } - - // Analyze End components and ensure reward finiteness. - // Note that this is only necessary if there is at least one objective with no upper time bound - for (auto const& obj : result.objectives) { - if (!obj.upperTimeBound) { - auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); - analyzeEndComponents(result, backwardTransitions); - ensureRewardFiniteness(result, backwardTransitions); - break; - } - } - return result; - } - - template - void SparsePcaaPreprocessor::updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping) { - result.preprocessedModel = std::move(newPreprocessedModel); - // the given newToOldStateIndexMapping refers to the indices of the former preprocessedModel as 'old indices' - for (auto & preprocessedModelStateIndex : newToOldStateIndexMapping){ - preprocessedModelStateIndex = result.newToOldStateIndexMapping[preprocessedModelStateIndex]; - } - result.newToOldStateIndexMapping = std::move(newToOldStateIndexMapping); - } - - template - void SparsePcaaPreprocessor::addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory) { - storm::storage::SparseModelMemoryProduct product = memory.product(result.preprocessedModel); - auto newModel = product.build(); - - // update the newToOldStateIndexMapping - std::vector updatedMapping; - updatedMapping.reserve(newModel->getNumberOfStates()); - for (uint_fast64_t oldState = 0; oldState < result.preprocessedModel.getNumberOfStates(); ++oldState) { - for (uint_fast64_t memoryState = 0; memoryState < memory.getNumberOfStates(); ++memoryState) { - uint_fast64_t const& newState = product.getResultState(oldState, memoryState); - // Check if the state actually exists in the new model - if (newState < newModel->getNumberOfStates()) { - assert(newState == updatedMapping.size()); - updatedMapping.push_back(result.newToOldStateIndexMapping[oldState]); - } - } - } - - result.preprocessedModel = std::move(dynamic_cast(*newModel)); - result.newToOldStateIndexMapping = std::move(updatedMapping); - } - - template - void SparsePcaaPreprocessor::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - - // Get a unique name for the new reward model. - currentObjective.rewardModelName = "objective" + std::to_string(result.objectives.size()); - while(result.preprocessedModel.hasRewardModel(currentObjective.rewardModelName)){ - currentObjective.rewardModelName = "_" + currentObjective.rewardModelName; - } - - currentObjective.toOriginalValueTransformationFactor = storm::utility::one(); - currentObjective.toOriginalValueTransformationOffset = storm::utility::zero(); - currentObjective.rewardsArePositive = true; - - bool formulaMinimizes = false; - if (formula.hasBound()) { - currentObjective.threshold = formula.template getThresholdAs(); - currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType); - //Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler - formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType); - } else if (formula.hasOptimalityType()){ - formulaMinimizes = storm::solver::minimize(formula.getOptimalityType()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Current objective " << formula << " does not specify whether to minimize or maximize"); - } - if (formulaMinimizes) { - // We negate all the values so we can consider the maximum for this objective - // Thus, all objectives will be maximized. - currentObjective.rewardsArePositive = false; - currentObjective.toOriginalValueTransformationFactor = -storm::utility::one(); - } - - if (formula.isProbabilityOperatorFormula()){ - preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), result, currentObjective); - } else if (formula.isRewardOperatorFormula()){ - preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), result, currentObjective); - } else if (formula.isTimeOperatorFormula()){ - preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); - } - - // Transform the threshold for the preprocessed Model - if (currentObjective.threshold) { - currentObjective.threshold = (currentObjective.threshold.get() - currentObjective.toOriginalValueTransformationOffset) / currentObjective.toOriginalValueTransformationFactor; - } - } - - template - void SparsePcaaPreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - - if (formula.getSubformula().isUntilFormula()){ - preprocessUntilFormula(formula.getSubformula().asUntilFormula(), result, currentObjective); - } else if (formula.getSubformula().isBoundedUntilFormula()){ - preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective); - } else if (formula.getSubformula().isGloballyFormula()){ - preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective); - } else if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparsePcaaPreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - // Check if the reward model is uniquely specified - STORM_LOG_THROW((formula.hasRewardModelName() && result.preprocessedModel.hasRewardModel(formula.getRewardModelName())) - || result.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); - - if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName()); - } else if (formula.getSubformula().isCumulativeRewardFormula()) { - preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); - } else if (formula.getSubformula().isTotalRewardFormula()) { - preprocessTotalRewardFormula(result, currentObjective, formula.getOptionalRewardModelName()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparsePcaaPreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - // Time formulas are only supported for Markov automata - STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); - - if (formula.getSubformula().isEventuallyFormula()){ - preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); - } - } - - template - void SparsePcaaPreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - - // Create a memory structure that stores whether a PhiState or a PsiState has already been reached - storm::storage::MemoryStructureBuilder builder(2); - // Get a unique label that is not already present in the model - std::string memoryLabel = "obj" + std::to_string(result.objectives.size()); - while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel; - builder.setLabel(0, memoryLabel); - auto negatedLeftSubFormula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getLeftSubformula().asSharedPointer()); - auto targetFormula = std::make_shared(storm::logic::BinaryBooleanStateFormula::OperatorType::Or, negatedLeftSubFormula, formula.getRightSubformula().asSharedPointer()); - builder.setTransition(0, 0, std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, targetFormula)); - builder.setTransition(0, 1, targetFormula); - builder.setTransition(1, 1, std::make_shared(true)); - storm::storage::MemoryStructure memory = builder.build(); - addMemoryToPreprocessedModel(result, memory); - - // build stateAction reward vector that gives (one*transitionProbability) reward whenever a transition leads from a memoryLabel-state to a psiState - storm::storage::BitVector const& statesWithMemoryLabel = result.preprocessedModel.getStates(memoryLabel); - if ((statesWithMemoryLabel & result.preprocessedModel.getInitialStates()).empty() && !currentObjective.lowerTimeBound) { - // The probability is always one as the initial state is a target state. - // For this special case, the transformation to an expected reward objective fails. - // We could handle this with further preprocessing steps but as this case is trivial anyway, we reject the input. - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The Probability for the objective " << *currentObjective.originalFormula << " is always one as the rhs of the until formula is true in the initial state. Please omit this objective."); - } - storm::modelchecker::SparsePropositionalModelChecker mc(result.preprocessedModel); - storm::storage::BitVector psiStates = mc.check(formula.getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); - - std::vector objectiveRewards(result.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); - for (auto const& state : statesWithMemoryLabel) { - for (uint_fast64_t row = result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++row) { - objectiveRewards[row] = result.preprocessedModel.getTransitionMatrix().getConstrainedRowSum(row, psiStates); - } - } - if (!currentObjective.rewardsArePositive) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); - } - - template - void SparsePcaaPreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - STORM_LOG_THROW(!result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || !formula.isStepBounded(), storm::exceptions::InvalidPropertyException, "Multi-objective model checking currently does not support STEP-bounded properties for Markov automata."); - - if (formula.hasLowerBound()) { - currentObjective.lowerTimeBound = formula.getLowerBound(); - currentObjective.lowerTimeBoundStrict = formula.isLowerBoundStrict(); - } - if (formula.hasUpperBound()) { - currentObjective.upperTimeBound = formula.getUpperBound(); - currentObjective.upperTimeBoundStrict = formula.isUpperBoundStrict(); - } - preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); - } - - template - void SparsePcaaPreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { - // The formula will be transformed to an until formula for the complementary event. - // If the original formula minimizes, the complementary one will maximize and vice versa. - // Hence, the decision whether to consider positive or negative rewards flips. - currentObjective.rewardsArePositive = !currentObjective.rewardsArePositive; - // To transform from the value of the preprocessed model back to the value of the original model, we have to add 1 to the result. - // The transformation factor has already been set correctly. - currentObjective.toOriginalValueTransformationOffset = storm::utility::one(); - - auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); - - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), result, currentObjective); - } - - template - void SparsePcaaPreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { - if (formula.isReachabilityProbabilityFormula()){ - preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective); - return; - } - - // Create a memory structure that stores whether a target state has already been reached - storm::storage::MemoryStructureBuilder builder(2); - // Get a unique label that is not already present in the model - std::string memoryLabel = "obj" + std::to_string(result.objectives.size()); - while (result.preprocessedModel.hasLabel(memoryLabel)) memoryLabel = "_" + memoryLabel; - builder.setLabel(0, memoryLabel); - builder.setTransition(0, 0, std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer())); - builder.setTransition(0, 1, formula.getSubformula().asSharedPointer()); - builder.setTransition(1, 1, std::make_shared(true)); - storm::storage::MemoryStructure memory = builder.build(); - addMemoryToPreprocessedModel(result, memory); - - // Add a reward model that only gives reward to states with the memory label - RewardModelType objectiveRewards(boost::none); - if (formula.isReachabilityRewardFormula()) { - storm::storage::BitVector statesWithoutMemoryLabel = ~result.preprocessedModel.getStates(memoryLabel); - objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if (objectiveRewards.hasStateRewards()) { - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), statesWithoutMemoryLabel, storm::utility::zero()); - } - if (objectiveRewards.hasStateActionRewards()) { - for (auto state : statesWithoutMemoryLabel) { - std::fill_n(objectiveRewards.getStateActionRewardVector().begin() + result.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state], result.preprocessedModel.getTransitionMatrix().getRowGroupSize(state), storm::utility::zero()); - } - } - } else if (formula.isReachabilityTimeFormula() && result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton)) { - objectiveRewards = RewardModelType(std::vector(result.preprocessedModel.getNumberOfStates(), storm::utility::zero())); - storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), dynamic_cast*>(&result.preprocessedModel)->getMarkovianStates() & result.preprocessedModel.getStates(memoryLabel), storm::utility::one()); - } else { - STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (result.preprocessedModel.isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); - } - if (!currentObjective.rewardsArePositive){ - if (objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if (objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - template - void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { - STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); - currentObjective.upperTimeBound = formula.getBound(); - currentObjective.upperTimeBoundStrict = formula.isBoundStrict(); - - RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if (!currentObjective.rewardsArePositive){ - if (objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if (objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - template - void SparsePcaaPreprocessor::preprocessTotalRewardFormula(ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { - RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); - objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); - if (!currentObjective.rewardsArePositive){ - if (objectiveRewards.hasStateRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateRewardVector(), -storm::utility::one()); - } - if (objectiveRewards.hasStateActionRewards()) { - storm::utility::vector::scaleVectorInPlace(objectiveRewards.getStateActionRewardVector(), -storm::utility::one()); - } - } - result.preprocessedModel.addRewardModel(currentObjective.rewardModelName, std::move(objectiveRewards)); - } - - - template - void SparsePcaaPreprocessor::analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { - - result.ecActions = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); - std::vector ecs; - auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions); - STORM_LOG_ASSERT(!mecDecomposition.empty(), "Empty maximal end component decomposition."); - ecs.reserve(mecDecomposition.size()); - for (auto& mec : mecDecomposition) { - for (auto const& stateActionsPair : mec) { - for (auto const& action : stateActionsPair.second) { - result.ecActions.set(action); - } - } - ecs.push_back(std::move(mec)); - } - - result.possiblyRecurrentStates = storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), false); - storm::storage::BitVector neutralActions = ~(result.actionsWithNegativeReward | result.actionsWithPositiveReward); - storm::storage::BitVector statesInCurrentECWithNeutralAction(result.preprocessedModel.getNumberOfStates(), false); - for (uint_fast64_t ecIndex = 0; ecIndex < ecs.size(); ++ecIndex) { //we will insert new ecs in the vector (thus no iterators for the loop) - bool currentECIsNeutral = true; - for (auto const& stateActionsPair : ecs[ecIndex]) { - bool stateHasNeutralActionWithinEC = false; - for (auto const& action : stateActionsPair.second) { - stateHasNeutralActionWithinEC |= neutralActions.get(action); - } - statesInCurrentECWithNeutralAction.set(stateActionsPair.first, stateHasNeutralActionWithinEC); - currentECIsNeutral &= stateHasNeutralActionWithinEC; - } - if (currentECIsNeutral) { - result.possiblyRecurrentStates |= statesInCurrentECWithNeutralAction; - }else{ - // Check if the ec contains neutral sub ecs. This is done by adding the subECs to our list of ECs - // A neutral subEC only consist of states that can stay in statesInCurrentECWithNeutralAction - statesInCurrentECWithNeutralAction = storm::utility::graph::performProb0E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions,statesInCurrentECWithNeutralAction, ~statesInCurrentECWithNeutralAction); - auto subECs = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions, statesInCurrentECWithNeutralAction); - ecs.reserve(ecs.size() + subECs.size()); - for (auto& ec : subECs){ - ecs.push_back(std::move(ec)); - } - } - statesInCurrentECWithNeutralAction.clear(); - } - } - - template - void SparsePcaaPreprocessor::ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { - STORM_LOG_THROW((result.actionsWithPositiveReward & result.ecActions).empty(), storm::exceptions::InvalidPropertyException, "Infinite reward: There is one maximizing objective for which infinite reward is possible. This is not supported."); - - //Check whether the states that can be visited inf. often are reachable with prob. 1 under some scheduler - storm::storage::BitVector statesReachingNegativeRewardsFinitelyOftenForSomeScheduler = storm::utility::graph::performProb1E(result.preprocessedModel.getTransitionMatrix(), result.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), backwardTransitions, storm::storage::BitVector(result.preprocessedModel.getNumberOfStates(), true), result.possiblyRecurrentStates); - STORM_LOG_THROW(!(statesReachingNegativeRewardsFinitelyOftenForSomeScheduler & result.preprocessedModel.getInitialStates()).empty(), storm::exceptions::InvalidPropertyException, "Infinite Rewards: For every scheduler, the induced reward for one or more of the objectives that minimize rewards is infinity."); - - if (!statesReachingNegativeRewardsFinitelyOftenForSomeScheduler.full()) { - // Remove the states that for any scheduler have one objective with infinite expected reward. - auto subsystemBuilderResult = storm::transformer::SubsystemBuilder::transform(result.preprocessedModel, statesReachingNegativeRewardsFinitelyOftenForSomeScheduler, storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), true)); - updatePreprocessedModel(result, *subsystemBuilderResult.model, subsystemBuilderResult.newToOldStateIndexMapping); - result.ecActions = result.ecActions % subsystemBuilderResult.keptActions; - result.actionsWithPositiveReward = result.actionsWithPositiveReward % subsystemBuilderResult.keptActions; - result.actionsWithNegativeReward = result.actionsWithNegativeReward % subsystemBuilderResult.keptActions; - result.possiblyRecurrentStates = result.possiblyRecurrentStates % statesReachingNegativeRewardsFinitelyOftenForSomeScheduler; - } - } - - - - template class SparsePcaaPreprocessor>; - template class SparsePcaaPreprocessor>; - -#ifdef STORM_HAVE_CARL - template class SparsePcaaPreprocessor>; - template class SparsePcaaPreprocessor>; -#endif - } - } -} diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h deleted file mode 100644 index 70e5a6018..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h +++ /dev/null @@ -1,82 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ - -#include - -#include "storm/logic/Formulas.h" -#include "storm/storage/BitVector.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h" -#include "storm/storage/memorystructure/MemoryStructure.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - /* - * This class invokes the necessary preprocessing for the Pareto Curve Approximation Algorithm (PCAA) - */ - template - class SparsePcaaPreprocessor { - public: - typedef typename SparseModelType::ValueType ValueType; - typedef typename SparseModelType::RewardModelType RewardModelType; - typedef SparsePcaaPreprocessorReturnType ReturnType; - - /*! - * Preprocesses the given model w.r.t. the given formulas. - * @param originalModel The considered model - * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple. - */ - static ReturnType preprocess(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula); - - private: - - /*! - * Updates the preprocessed model stored in the given result to the given model. - * The given newToOldStateIndexMapping should give for each state in the newPreprocessedModel - * the index of the state in the current result.preprocessedModel. - */ - static void updatePreprocessedModel(ReturnType& result, SparseModelType& newPreprocessedModel, std::vector& newToOldStateIndexMapping); - - /*! - * Updates the preprocessed model stored in the given result to the product of the model and the given memory structure. - */ - static void addMemoryToPreprocessedModel(ReturnType& result, storm::storage::MemoryStructure& memory); - - /*! - * Apply the neccessary preprocessing for the given formula. - * @param formula the current (sub)formula - * @param result the information collected so far - * @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective - * @param optionalRewardModelName the reward model name that is considered for the formula (if available) - */ - static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessTotalRewardFormula(ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. - - /*! - * Analyzes the end components of the preprocessed model. That is: - * -get the set of actions that are part of an end component - * -Find the states that can be visited infinitely often without inducing infinite reward - */ - static void analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions); - - /*! - * Checks whether the occurring expected rewards are finite. If not, the input is rejected. - * Also removes all states for which no finite reward wrt. all objectives is possible - */ - static void ensureRewardFiniteness(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions); - - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSOR_H_ */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h deleted file mode 100644 index 8237da3c0..000000000 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h +++ /dev/null @@ -1,93 +0,0 @@ -#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ -#define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ - -#include -#include -#include -#include -#include - -#include "storm/logic/Formulas.h" -#include "storm/modelchecker/multiobjective/pcaa/PcaaObjective.h" -#include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/storage/BitVector.h" -#include "storm/utility/macros.h" -#include "storm/utility/constants.h" - -#include "storm/exceptions/UnexpectedException.h" - -namespace storm { - namespace modelchecker { - namespace multiobjective { - - template - struct SparsePcaaPreprocessorReturnType { - - enum class QueryType { Achievability, Quantitative, Pareto }; - - storm::logic::MultiObjectiveFormula const& originalFormula; - SparseModelType const& originalModel; - SparseModelType preprocessedModel; - QueryType queryType; - - // The (preprocessed) objectives - std::vector> objectives; - - // The index of the objective that is to be maximized (or minimized) in case of a quantitative Query - boost::optional indexOfOptimizingObjective; - - // Maps any state of the preprocessed model to the corresponding state of the original Model - std::vector newToOldStateIndexMapping; - - // The actions of the preprocessed model that have positive reward assigned for at least one objective (objectives with an upper time-bound are ignored!) - storm::storage::BitVector actionsWithPositiveReward; - // The actions of the preprocessed model that have negative reward assigned for at least one objective (objectives with an upper time-bound are ignored!) - storm::storage::BitVector actionsWithNegativeReward; - // The actions of the preprocessed model that are part of an EC - storm::storage::BitVector ecActions; - - // The set of states of the preprocessed model for which there is a scheduler such that - // the state is visited infinitely often and the induced reward is finite for all objectives - storm::storage::BitVector possiblyRecurrentStates; - - SparsePcaaPreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel, SparseModelType&& preprocessedModel) : originalFormula(originalFormula), originalModel(originalModel), preprocessedModel(preprocessedModel) { - // Intentionally left empty - } - - void printToStream(std::ostream& out) const { - out << std::endl; - out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - out << " Multi-objective Query " << std::endl; - out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - out << std::endl; - out << "Original Formula: " << std::endl; - out << "--------------------------------------------------------------" << std::endl; - out << "\t" << originalFormula << std::endl; - out << std::endl; - out << "Objectives:" << std::endl; - out << "--------------------------------------------------------------" << std::endl; - for (auto const& obj : objectives) { - obj.printToStream(out); - } - out << "--------------------------------------------------------------" << std::endl; - out << std::endl; - out << "Original Model Information:" << std::endl; - originalModel.printModelInformationToStream(out); - out << std::endl; - out << "Preprocessed Model Information:" << std::endl; - preprocessedModel.printModelInformationToStream(out); - out << std::endl; - out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl; - } - - friend std::ostream& operator<<(std::ostream& out, SparsePcaaPreprocessorReturnType const& ret) { - ret.printToStream(out); - return out; - } - - }; - } - } -} - -#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAPREPROCESSORRETURNTYPE_H_ */ diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 48448f968..ae5484a50 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -8,20 +8,27 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/settings//SettingsManager.h" +#include "storm/settings/SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/modules/GeneralSettings.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace modelchecker { namespace multiobjective { template - SparsePcaaQuantitativeQuery::SparsePcaaQuantitativeQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { - STORM_LOG_ASSERT(preprocessorResult.queryType==SparsePcaaPreprocessorReturnType::QueryType::Quantitative, "Invalid query Type"); - STORM_LOG_ASSERT(preprocessorResult.indexOfOptimizingObjective, "Detected quantitative query but index of optimizing objective is not set."); - indexOfOptimizingObjective = *preprocessorResult.indexOfOptimizingObjective; + SparsePcaaQuantitativeQuery::SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : SparsePcaaQuery(preprocessorResult) { + STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType::QueryType::Quantitative, "Invalid query Type"); + + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (!this->objectives[objIndex].bound.is_initialized()) { + indexOfOptimizingObjective = objIndex; + break; + } + } initializeThresholdData(); // Set the maximum distance between lower and upper bound of the weightVectorChecker result. @@ -30,17 +37,26 @@ namespace storm { template void SparsePcaaQuantitativeQuery::initializeThresholdData() { + thresholds.reserve(this->objectives.size()); strictThresholds = storm::storage::BitVector(this->objectives.size(), false); std::vector> thresholdConstraints; thresholdConstraints.reserve(this->objectives.size()-1); - for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if(this->objectives[objIndex].threshold) { - thresholds.push_back(storm::utility::convertNumber(*this->objectives[objIndex].threshold)); + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + auto const& obj = this->objectives[objIndex]; + if (obj.bound) { + STORM_LOG_THROW(!obj.bound->threshold.containsVariables(), storm::exceptions::InvalidOperationException, "There is an objective whose bound contains undefined variables."); + thresholds.push_back(storm::utility::convertNumber(obj.bound->threshold.evaluateAsRational())); + if (storm::solver::minimize(obj.optimizationDirection)) { + STORM_LOG_ASSERT(!storm::logic::isLowerBound(obj.bound->comparisonType), "Minimizing objective should not specify an upper bound."); + // Values for minimizing objectives will be negated in order to convert them to maximizing objectives. + // Hence, we also negate the threshold + thresholds.back() *= -storm::utility::one(); + } + strictThresholds.set(objIndex, storm::logic::isStrict(obj.bound->comparisonType)); WeightVector normalVector(this->objectives.size(), storm::utility::zero()); normalVector[objIndex] = -storm::utility::one(); thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back()); - strictThresholds.set(objIndex, this->objectives[objIndex].thresholdIsStrict); } else { thresholds.push_back(storm::utility::zero()); } @@ -52,26 +68,34 @@ namespace storm { template std::unique_ptr SparsePcaaQuantitativeQuery::check() { // First find one solution that achieves the given thresholds ... - if(this->checkAchievability()) { + if (this->checkAchievability()) { // ... then improve it GeometryValueType result = this->improveSolution(); // transform the obtained result for the preprocessed model to a result w.r.t. the original model and return the checkresult - typename SparseModelType::ValueType resultForOriginalModel = - storm::utility::convertNumber(result) * - this->objectives[indexOfOptimizingObjective].toOriginalValueTransformationFactor + - this->objectives[indexOfOptimizingObjective].toOriginalValueTransformationOffset; + auto const& obj = this->objectives[indexOfOptimizingObjective]; + if (storm::solver::maximize(obj.optimizationDirection)) { + if (obj.considersComplementaryEvent) { + result = storm::utility::one() - result; + } + } else { + if (obj.considersComplementaryEvent) { + result = storm::utility::one() + result; // 1 - (-result) + } else { + result *= -storm::utility::one(); + } + } + auto resultForOriginalModel = storm::utility::convertNumber(result); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), resultForOriginalModel)); } else { return std::unique_ptr(new ExplicitQualitativeCheckResult(this->originalModel.getInitialStates().getNextSetIndex(0), false)); } - - } template bool SparsePcaaQuantitativeQuery::checkAchievability() { - if(this->objectives.size()>1) { + if (this->objectives.size()>1) { // We don't care for the optimizing objective at this point this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false); @@ -81,10 +105,10 @@ namespace storm { this->performRefinementStep(std::move(separatingVector)); //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded thresholds[indexOfOptimizingObjective] = std::min(thresholds[indexOfOptimizingObjective], this->refinementSteps.back().lowerBoundPoint[indexOfOptimizingObjective]); - if(!checkIfThresholdsAreSatisfied(this->overApproximation)){ + if (!checkIfThresholdsAreSatisfied(this->overApproximation)){ return false; } - if(checkIfThresholdsAreSatisfied(this->underApproximation)){ + if (checkIfThresholdsAreSatisfied(this->underApproximation)){ return true; } } @@ -100,9 +124,9 @@ namespace storm { void SparsePcaaQuantitativeQuery::updateWeightedPrecisionInAchievabilityPhase(WeightVector const& weights) { // Our heuristic considers the distance between the under- and the over approximation w.r.t. the given direction std::pair optimizationResOverApprox = this->overApproximation->optimize(weights); - if(optimizationResOverApprox.second) { + if (optimizationResOverApprox.second) { std::pair optimizationResUnderApprox = this->underApproximation->optimize(weights); - if(optimizationResUnderApprox.second) { + if (optimizationResUnderApprox.second) { GeometryValueType distance = storm::utility::vector::dotProduct(optimizationResOverApprox.first, weights) - storm::utility::vector::dotProduct(optimizationResUnderApprox.first, weights); STORM_LOG_ASSERT(distance >= storm::utility::zero(), "Negative distance between under- and over approximation was not expected"); // Normalize the distance by dividing it with the Euclidean Norm of the weight-vector @@ -127,7 +151,7 @@ namespace storm { // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds. GeometryValueType result = storm::utility::zero(); while(!this->maxStepsPerformed()) { - if(this->refinementSteps.empty()) { + if (this->refinementSteps.empty()) { // We did not make any refinement steps during the checkAchievability phase (e.g., because there is only one objective). this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber(storm::settings::getModule().getPrecision())); WeightVector separatingVector = directionOfOptimizingObjective; @@ -139,9 +163,9 @@ namespace storm { STORM_LOG_DEBUG("Best solution found so far is ~" << storm::utility::convertNumber(result) << "."); //Compute an upper bound for the optimum and check for convergence optimizationRes = this->overApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective); - if(optimizationRes.second) { + if (optimizationRes.second) { GeometryValueType precisionOfResult = optimizationRes.first[indexOfOptimizingObjective] - result; - if(precisionOfResult < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { + if (precisionOfResult < storm::utility::convertNumber(storm::settings::getModule().getPrecision())) { // Goal precision reached! return result; } else { @@ -177,12 +201,12 @@ namespace storm { template bool SparsePcaaQuantitativeQuery::checkIfThresholdsAreSatisfied(std::shared_ptr> const& polytope) { std::vector> halfspaces = polytope->getHalfspaces(); - for(auto const& h : halfspaces) { - if(storm::utility::isZero(h.distance(thresholds))) { + for (auto const& h : halfspaces) { + if (storm::utility::isZero(h.distance(thresholds))) { // Check if the threshold point is on the boundary of the halfspace and whether this is violates strict thresholds - if(h.isPointOnBoundary(thresholds)) { - for(auto strictThreshold : strictThresholds) { - if(h.normalVector()[strictThreshold] > storm::utility::zero()) { + if (h.isPointOnBoundary(thresholds)) { + for (auto strictThreshold : strictThresholds) { + if (h.normalVector()[strictThreshold] > storm::utility::zero()) { return false; } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h index ca2d8c81a..d28ea4e9f 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h @@ -23,7 +23,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaQuantitativeQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); virtual ~SparsePcaaQuantitativeQuery() = default; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 5bc096c93..c85a22c5c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -4,10 +4,10 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/modelchecker/multiobjective/pcaa/PcaaObjective.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/SettingsManager.h" #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/storage/geometry/Hyperrectangle.h" #include "storm/utility/constants.h" @@ -22,28 +22,29 @@ namespace storm { template - SparsePcaaQuery::SparsePcaaQuery(SparsePcaaPreprocessorReturnType& preprocessorResult) : + SparsePcaaQuery::SparsePcaaQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult) : originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula), - preprocessedModel(std::move(preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) { - initializeWeightVectorChecker(preprocessedModel, objectives, preprocessorResult.actionsWithNegativeReward, preprocessorResult.ecActions, preprocessorResult.possiblyRecurrentStates); + preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) { + + initializeWeightVectorChecker(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& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + 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& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMdpPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + 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& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { - this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + 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 @@ -98,6 +99,13 @@ namespace storm { step.weightVector = direction; step.lowerBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getLowerBoundsOfInitialStateResults()); step.upperBoundPoint = storm::utility::vector::convertNumericVector(weightVectorChecker->getUpperBoundsOfInitialStateResults()); + // For the minimizing objectives, we need to scale the corresponding entries with -1 in order to consider the downward closure + for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { + if (storm::solver::minimize(this->objectives[objIndex].optimizationDirection)) { + step.lowerBoundPoint[objIndex] *= -storm::utility::one(); + step.upperBoundPoint[objIndex] *= -storm::utility::one(); + } + } refinementSteps.push_back(std::move(step)); updateOverApproximation(); @@ -146,7 +154,20 @@ namespace storm { Point result; result.reserve(point.size()); for(uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - result.push_back(point[objIndex] * storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationOffset)); + auto const& obj = this->objectives[objIndex]; + if (storm::solver::maximize(obj.optimizationDirection)) { + if (obj.considersComplementaryEvent) { + result.push_back(storm::utility::one() - point[objIndex]); + } else { + result.push_back(point[objIndex]); + } + } else { + if (obj.considersComplementaryEvent) { + result.push_back(storm::utility::one() + point[objIndex]); + } else { + result.push_back(-point[objIndex]); + } + } } return result; } @@ -164,8 +185,24 @@ namespace storm { std::vector transformationVector; transformationVector.reserve(numObjectives); for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) { - transformationMatrix[objIndex][objIndex] = storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationFactor); - transformationVector.push_back(storm::utility::convertNumber(this->objectives[objIndex].toOriginalValueTransformationOffset)); + auto const& obj = this->objectives[objIndex]; + if (storm::solver::maximize(obj.optimizationDirection)) { + if (obj.considersComplementaryEvent) { + transformationMatrix[objIndex][objIndex] = -storm::utility::one(); + transformationVector.push_back(storm::utility::one()); + } else { + transformationMatrix[objIndex][objIndex] = storm::utility::one(); + transformationVector.push_back(storm::utility::zero()); + } + } else { + if (obj.considersComplementaryEvent) { + transformationMatrix[objIndex][objIndex] = storm::utility::one(); + transformationVector.push_back(storm::utility::one()); + } else { + transformationMatrix[objIndex][objIndex] = -storm::utility::one(); + transformationVector.push_back(storm::utility::zero()); + } + } } return polytope->affineTransformation(transformationMatrix, transformationVector); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h index e6404c9ac..05cd258eb 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h @@ -2,7 +2,7 @@ #define STORM_MODELCHECKER_MULTIOBJECTIVE_PCAA_SPARSEPCAAQUERY_H_ #include "storm/modelchecker/results/CheckResult.h" -#include "storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessorReturnType.h" +#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h" #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h" #include "storm/storage/geometry/Polytope.h" @@ -43,10 +43,9 @@ namespace storm { * Initializes the weight vector checker with the provided data from preprocessing */ void initializeWeightVectorChecker(SparseModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + 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 @@ -61,7 +60,7 @@ namespace storm { * Creates a new query for the Pareto curve approximation algorithm (Pcaa) * @param preprocessorResult the result from preprocessing */ - SparsePcaaQuery(SparsePcaaPreprocessorReturnType& preprocessorResult); + SparsePcaaQuery(SparseMultiObjectivePreprocessorReturnType& preprocessorResult); /* * Returns a weight vector w that separates the under approximation from the given point p, i.e., @@ -106,8 +105,7 @@ namespace storm { storm::logic::MultiObjectiveFormula const& originalFormula; SparseModelType preprocessedModel; - std::vector> objectives; - + std::vector> objectives; // The corresponding weight vector checker std::unique_ptr> weightVectorChecker; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index d93cedab8..d944aa7c3 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -24,25 +24,28 @@ namespace storm { template SparsePcaaWeightVectorChecker::SparsePcaaWeightVectorChecker(SparseModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates) : + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates) : model(model), objectives(objectives), - actionsWithNegativeReward(actionsWithNegativeReward), - ecActions(ecActions), - possiblyRecurrentStates(possiblyRecurrentStates), - objectivesWithNoUpperTimeBound(objectives.size()), + possibleECActions(possibleECActions), + actionsWithoutRewardInUnboundedPhase(model.getNumberOfChoices(), true), + possibleBottomStates(possibleBottomStates), + objectivesWithNoUpperTimeBound(objectives.size(), false), discreteActionRewards(objectives.size()), checkHasBeenCalled(false), objectiveResults(objectives.size()), offsetsToLowerBound(objectives.size()), offsetsToUpperBound(objectives.size()) { - // set the unbounded objectives + // set data for unbounded objectives for(uint_fast64_t objIndex = 0; objIndex < objectives.size(); ++objIndex) { - objectivesWithNoUpperTimeBound.set(objIndex, !objectives[objIndex].upperTimeBound); + auto const& obj = objectives[objIndex]; + if (!obj.upperTimeBound) { + objectivesWithNoUpperTimeBound.set(objIndex, true); + actionsWithoutRewardInUnboundedPhase &= model.getRewardModel(*obj.rewardModelName).getChoicesWithZeroReward(model.getTransitionMatrix()); + } } } @@ -52,10 +55,37 @@ namespace storm { 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()); - for(auto objIndex : objectivesWithNoUpperTimeBound) { - storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); + boost::optional weightedLowerResultBound = storm::utility::zero(); + boost::optional weightedUpperResultBound = storm::utility::zero(); + for (auto objIndex : objectivesWithNoUpperTimeBound) { + if (storm::solver::minimize(objectives[objIndex].optimizationDirection)) { + if (objectives[objIndex].lowerResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() -= weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + } else { + weightedUpperResultBound = boost::none; + } + if (objectives[objIndex].upperResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() -= weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + } else { + weightedLowerResultBound = boost::none; + } + storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], -weightVector[objIndex]); + } else { + if (objectives[objIndex].lowerResultBound && weightedLowerResultBound) { + weightedLowerResultBound.get() += weightVector[objIndex] * objectives[objIndex].lowerResultBound.get(); + } else { + weightedLowerResultBound = boost::none; + } + if (objectives[objIndex].upperResultBound && weightedUpperResultBound) { + weightedUpperResultBound.get() += weightVector[objIndex] * objectives[objIndex].upperResultBound.get(); + } else { + weightedUpperResultBound = boost::none; + } + storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]); + } } - unboundedWeightedPhase(weightedRewardVector); + + unboundedWeightedPhase(weightedRewardVector, weightedLowerResultBound, weightedUpperResultBound); unboundedIndividualPhase(weightVector); // Only invoke boundedPhase if necessarry, i.e., if there is at least one objective with a time bound for(auto const& obj : this->objectives) { @@ -116,14 +146,13 @@ namespace storm { } template - void SparsePcaaWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightedRewardVector) { + 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->scheduler = storm::storage::TotalScheduler(model.getNumberOfStates()); 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; @@ -136,7 +165,7 @@ namespace storm { storm::storage::BitVector subsystemStates = storm::utility::graph::performProbGreater0E(model.getTransitionMatrix().transpose(true), storm::storage::BitVector(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, ecActions & zeroRewardActions, possiblyRecurrentStates); + auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(model.getTransitionMatrix(), subsystemStates, possibleECActions & zeroRewardActions, possibleBottomStates); std::vector subRewardVector(ecEliminatorResult.newToOldRowMapping.size()); storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector); @@ -146,6 +175,12 @@ namespace storm { std::unique_ptr> solver = solverFactory.create(ecEliminatorResult.matrix); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->setTrackScheduler(true); + if (lowerResultBound) { + solver->setLowerBound(*lowerResultBound); + } + if (upperResultBound) { + solver->setUpperBound(*upperResultBound); + } solver->solveEquations(subResult, subRewardVector); this->weightedResult = std::vector(model.getNumberOfStates()); @@ -158,10 +193,14 @@ namespace storm { template void SparsePcaaWeightVectorChecker::unboundedIndividualPhase(std::vector const& weightVector) { - if(objectivesWithNoUpperTimeBound.getNumberOfSetBits() == 1 && storm::utility::isOne(weightVector[*objectivesWithNoUpperTimeBound.begin()])) { - objectiveResults[*objectivesWithNoUpperTimeBound.begin()] = weightedResult; + 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].optimizationDirection)) { + storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one()); + } for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) { - if(*objectivesWithNoUpperTimeBound.begin() != objIndex2) { + if (objIndex != objIndex2) { objectiveResults[objIndex2] = std::vector(model.getNumberOfStates(), storm::utility::zero()); } } @@ -177,6 +216,7 @@ 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]; if (objectivesWithNoUpperTimeBound.get(objIndex)) { offsetsToLowerBound[objIndex] = storm::utility::zero(); offsetsToUpperBound[objIndex] = storm::utility::zero(); @@ -188,7 +228,12 @@ namespace storm { // Compute the estimate for this objective if (!storm::utility::isZero(weightVector[objIndex])) { objectiveResults[objIndex] = weightedSumOfUncheckedObjectives; - storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one() / sumOfWeightsOfUncheckedObjectives); + ValueType scalingFactor = storm::utility::one() / sumOfWeightsOfUncheckedObjectives; + if (storm::solver::minimize(obj.optimizationDirection)) { + scalingFactor *= -storm::utility::one(); + } + storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], scalingFactor); + 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()); @@ -206,6 +251,12 @@ namespace storm { // Now solve the resulting equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(std::move(submatrix)); + if (obj.lowerResultBound) { + solver->setLowerBound(*obj.lowerResultBound); + } + if (obj.upperResultBound) { + solver->setUpperBound(*obj.upperResultBound); + } solver->solveEquations(x, b); // Set the result for this objective accordingly @@ -234,7 +285,7 @@ namespace storm { std::vector& originalSolution, std::vector& originalOptimalChoices) const { - storm::storage::BitVector recurrentStates(model.getTransitionMatrix().getRowGroupCount(), false); + storm::storage::BitVector bottomStates(model.getTransitionMatrix().getRowGroupCount(), false); storm::storage::BitVector statesThatShouldStayInTheirEC(model.getTransitionMatrix().getRowGroupCount(), false); storm::storage::BitVector statesWithUndefSched(model.getTransitionMatrix().getRowGroupCount(), false); @@ -247,13 +298,13 @@ namespace storm { originalSolution[state] = reducedSolution[stateInReducedModel]; uint_fast64_t chosenRowInReducedModel = reducedMatrix.getRowGroupIndices()[stateInReducedModel] + reducedOptimalChoices[stateInReducedModel]; uint_fast64_t chosenRowInOriginalModel = reducedToOriginalChoiceMapping[chosenRowInReducedModel]; - // Check if the state is recurrent, i.e., the chosen row stays inside this EC. - bool stateIsRecurrent = possiblyRecurrentStates.get(state); + // 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)) { - stateIsRecurrent &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; + stateIsBottom &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; } - if(stateIsRecurrent) { - recurrentStates.set(state); + if(stateIsBottom) { + bottomStates.set(state); statesThatShouldStayInTheirEC.set(state); } else { // Check if the chosen row originaly belonged to the current state (and not to another state of the EC) @@ -269,42 +320,41 @@ namespace storm { // if the state does not exist in the reduced model, it means that the (weighted) result is always zero, independent of the scheduler. originalSolution[state] = storm::utility::zero(); // However, it might be the case that infinite reward is induced for an objective with weight 0. - // To avoid this, all possibly recurrent states are made recurrent and the remaining states have to reach a recurrent state with prob. one - if(possiblyRecurrentStates.get(state)) { - recurrentStates.set(state); + // To avoid this, all possible bottom states are made bottom and the remaining states have to reach a bottom state with prob. one + if(possibleBottomStates.get(state)) { + bottomStates.set(state); } else { statesWithUndefSched.set(state); } } } - // Handle recurrent states - for(auto state : recurrentStates) { + // Handle bottom states + for(auto state : bottomStates) { bool foundRowForState = false; - // Find a row with zero rewards that only leads to recurrent states. + // 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) { - bool rowOnlyLeadsToRecurrentStates = true; + bool rowOnlyLeadsToBottomStates = true; bool rowStaysInEC = true; for( auto const& entry : model.getTransitionMatrix().getRow(row)) { - rowOnlyLeadsToRecurrentStates &= recurrentStates.get(entry.getColumn()); + rowOnlyLeadsToBottomStates &= bottomStates.get(entry.getColumn()); rowStaysInEC &= originalToReducedStateMapping[entry.getColumn()] == stateInReducedModel; } - if(rowOnlyLeadsToRecurrentStates && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state)) && !actionsWithNegativeReward.get(row)) { + if(rowOnlyLeadsToBottomStates && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state)) && actionsWithoutRewardInUnboundedPhase.get(row)) { foundRowForState = true; originalOptimalChoices[state] = row - model.getTransitionMatrix().getRowGroupIndices()[state]; break; } } - STORM_LOG_ASSERT(foundRowForState, "Could not find a suitable choice for a recurrent state."); + STORM_LOG_ASSERT(foundRowForState, "Could not find a suitable choice for a bottom state."); } // Handle remaining states with still undef. scheduler (either EC states or non-subsystem states) while(!statesWithUndefSched.empty()) { for(auto state : statesWithUndefSched) { - // Try to find a choice such that at least one successor has a defined scheduler. - // This way, a non-recurrent state will never become recurrent + // 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) { bool rowStaysInEC = true; diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h index d80eb4931..314cec988 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h @@ -5,7 +5,7 @@ #include "storm/storage/BitVector.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/TotalScheduler.h" -#include "storm/modelchecker/multiobjective/pcaa/PcaaObjective.h" +#include "storm/modelchecker/multiobjective/Objective.h" #include "storm/utility/vector.h" namespace storm { @@ -28,17 +28,15 @@ namespace storm { * * @param model The (preprocessed) model * @param objectives The (preprocessed) objectives - * @param actionsWithNegativeReward The actions that have negative reward assigned for at least one objective - * @param ecActions The actions that are part of an EC - * @param possiblyRecurrentStates The states for which it is posible to visit them infinitely often (without inducing inf. reward) + * @param possibleECActions Overapproximation of the actions that are part of an EC + * @param possibleBottomStates The states for which it is posible to not collect further reward with prob. 1 * */ SparsePcaaWeightVectorChecker(SparseModelType const& model, - std::vector> const& objectives, - storm::storage::BitVector const& actionsWithNegativeReward, - storm::storage::BitVector const& ecActions, - storm::storage::BitVector const& possiblyRecurrentStates); + std::vector> const& objectives, + storm::storage::BitVector const& possibleECActions, + storm::storage::BitVector const& possibleBottomStates); virtual ~SparsePcaaWeightVectorChecker() = default; @@ -88,7 +86,7 @@ namespace storm { * * @param weightedRewardVector the weighted rewards (only considering the unbounded objectives) */ - void unboundedWeightedPhase(std::vector const& weightedRewardVector); + void unboundedWeightedPhase(std::vector const& weightedRewardVector, boost::optional const& lowerResultBound, boost::optional const& upperResultBound); /*! * Computes the values of the objectives that do not have a stepBound w.r.t. the scheduler computed in the unboundedWeightedPhase @@ -122,16 +120,16 @@ namespace storm { // The (preprocessed) model SparseModelType const& model; // The (preprocessed) objectives - std::vector> const& objectives; + std::vector> const& objectives; - // The actions that have negative reward assigned for at least one objective - storm::storage::BitVector actionsWithNegativeReward; - // The actions that are part of an EC - storm::storage::BitVector ecActions; + // Overapproximation of the set of choices that are part of an end component. + storm::storage::BitVector possibleECActions; + // The actions that have reward assigned for at least one objective without upper timeBound + storm::storage::BitVector actionsWithoutRewardInUnboundedPhase; // The states for which it is allowed to visit them infinitely often // Put differently, if one of the states is part of a neutral EC, it is possible to // stay in this EC forever (withoud inducing infinite reward for some objective). - storm::storage::BitVector possiblyRecurrentStates; + storm::storage::BitVector possibleBottomStates; // stores the indices of the objectives for which there is no upper time bound storm::storage::BitVector objectivesWithNoUpperTimeBound; // stores the (discretized) state action rewards for each objective.