diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
index c6cfc0aa4..72c01f11f 100644
--- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
+++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp
@@ -63,6 +63,13 @@ namespace storm {
task->perform(*preprocessedModel);
}
+ // Remove reward models that are not needed anymore
+ std::set<std::string> relevantRewardModels;
+ for (auto const& obj : data.objectives) {
+ obj->formula->gatherReferencedRewardModels(relevantRewardModels);
+ }
+ preprocessedModel->restrictRewardModels(relevantRewardModels);
+
// Build the actual result
return buildResult(originalModel, originalFormula, data, preprocessedModel, backwardTransitions);
}
@@ -378,35 +385,38 @@ namespace storm {
result.queryType = getQueryType(result.objectives);
- auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions);
- auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions);
+ setReward0States(result, backwardTransitions);
+ checkRewardFiniteness(result, data.finiteRewardCheckObjectives, backwardTransitions);
+
+ /////
std::set<std::string> relevantRewardModels;
for (auto const& obj : result.objectives) {
obj.formula->gatherReferencedRewardModels(relevantRewardModels);
}
- // Build a subsystem that discards states that yield infinite reward for all schedulers.
- // We can also merge the states that will have reward zero anyway.
- storm::storage::BitVector zeroRewardStates = ~minMaxNonZeroRewardStates.second;
- storm::storage::BitVector maybeStates = finiteRewardStates & ~zeroRewardStates;
- storm::transformer::GoalStateMerger<SparseModelType> merger(*result.preprocessedModel);
- typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = merger.mergeTargetAndSinkStates(maybeStates, zeroRewardStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
-
- result.preprocessedModel = mergerResult.model;
- result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % maybeStates;
- if (mergerResult.targetState) {
- storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false);
- targetStateAsVector.set(*mergerResult.targetState, true);
- // The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself.
- result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowFilter(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector));
- result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true);
- // There is an additional state in the result
- result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true);
- } else {
- result.possibleECChoices = storm::storage::BitVector(result.preprocessedModel->getNumberOfChoices(), true);
+ STORM_LOG_THROW(result.rewardFinitenessType != ReturnType::RewardFinitenessType::Infinite, storm::exceptions::InvalidPropertyException, "Infinite rewards unsupported.");
+
+ if (result.containsOnlyRewardObjectives()) {
+ // Build a subsystem that discards states that yield infinite reward for all schedulers.
+ // We can also merge the states that will have reward zero anyway.
+ storm::storage::BitVector maybeStates = result.rewardLessInfinityEStates.get() & ~result.reward0AStates;
+ storm::transformer::GoalStateMerger<SparseModelType> merger(*result.preprocessedModel);
+ typename storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = merger.mergeTargetAndSinkStates(maybeStates, result.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
+
+ result.preprocessedModel = mergerResult.model;
+ result.reward0EStates = result.reward0EStates % maybeStates;
+ if (mergerResult.targetState) {
+ storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false);
+ targetStateAsVector.set(*mergerResult.targetState, true);
+ // The overapproximation for the possible ec choices consists of the states that can reach the target states with prob. 0 and the target state itself.
+ //result.ecChoicesHint = result.preprocessedModel->getTransitionMatrix().getRowFilter(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector));
+ //result.ecChoicesHint->set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true);
+ // There is an additional state in the result
+ result.reward0EStates.resize(result.reward0EStates.size() + 1, true);
+ }
+ assert(result.reward0EStates.size() == result.preprocessedModel->getNumberOfStates());
}
- assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates());
return result;
}
@@ -432,7 +442,7 @@ namespace storm {
}
template<typename SparseModelType>
- std::pair<storm::storage::BitVector, storm::storage::BitVector> SparseMultiObjectivePreprocessor<SparseModelType>::getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
+ void SparseMultiObjectivePreprocessor<SparseModelType>::setReward0States(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
uint_fast64_t stateCount = result.preprocessedModel->getNumberOfStates();
auto const& transitions = result.preprocessedModel->getTransitionMatrix();
@@ -445,10 +455,6 @@ namespace storm {
if (obj.formula->isRewardOperatorFormula()) {
auto const& rewModel = result.preprocessedModel->getRewardModel(obj.formula->asRewardOperatorFormula().getRewardModelName());
zeroRewardChoices &= rewModel.getChoicesWithZeroReward(transitions);
- } else {
- zeroRewardChoices.clear();
- STORM_LOG_WARN("Formula type not handled properly");
- //STORM_LOG_ASSERT(false, "Unknown formula type.");
}
}
@@ -474,51 +480,55 @@ namespace storm {
}
}
- // get the states from which the minimal/maximal expected reward is always non-zero
- storm::storage::BitVector minStates = storm::utility::graph::performProbGreater0A(transitions, groupIndices, backwardTransitions, allStates, statesWithRewardForAllChoices, false, 0, zeroRewardChoices);
- storm::storage::BitVector maxStates = storm::utility::graph::performProbGreater0E(backwardTransitions, allStates, statesWithRewardForOneChoice);
- STORM_LOG_ASSERT(minStates.isSubsetOf(maxStates), "The computed set of states with minimal non-zero expected rewards is not a subset of the states with maximal non-zero rewards.");
- return std::make_pair(std::move(minStates), std::move(maxStates));
+ // get the states for which there is a scheduler yielding reward zero
+ result.reward0EStates = storm::utility::graph::performProbGreater0A(transitions, groupIndices, backwardTransitions, allStates, statesWithRewardForAllChoices, false, 0, zeroRewardChoices);
+ result.reward0EStates.complement();
+ result.reward0AStates = storm::utility::graph::performProb0A(backwardTransitions, allStates, statesWithRewardForOneChoice);
+ assert(result.reward0EStates.isSubsetOf(result.reward0AStates));
}
template<typename SparseModelType>
- storm::storage::BitVector SparseMultiObjectivePreprocessor<SparseModelType>::ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
+ void SparseMultiObjectivePreprocessor<SparseModelType>::checkRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
+
+ result.rewardFinitenessType = ReturnType::RewardFinitenessType::AllFinite;
auto const& transitions = result.preprocessedModel->getTransitionMatrix();
std::vector<uint_fast64_t> const& groupIndices = transitions.getRowGroupIndices();
storm::storage::BitVector maxRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true);
- bool hasMinRewardToCheck = false;
+ storm::storage::BitVector minRewardsToCheck(result.preprocessedModel->getNumberOfChoices(), true);
for (auto const& objIndex : finiteRewardCheckObjectives) {
STORM_LOG_ASSERT(result.objectives[objIndex].formula->isRewardOperatorFormula(), "Objective needs to be checked for finite reward but has no reward operator.");
auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName());
if (storm::solver::minimize(result.objectives[objIndex].formula->getOptimalityType())) {
- hasMinRewardToCheck = true;
+ minRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions);
} else {
maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions);
}
}
maxRewardsToCheck.complement();
+ minRewardsToCheck.complement();
- // Assert reward finitiness for maximizing objectives under all schedulers
+ // Check reward finiteness under all schedulers
storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true);
- if (storm::utility::graph::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck)) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "At least one of the maximizing objectives induces infinite expected reward (or time). This is not supported");
- }
-
- // Assert that there is one scheduler under which all rewards are finite.
- // This only has to be done if there are minimizing expected rewards that potentially can be infinite
- storm::storage::BitVector finiteRewardStates;
- if (hasMinRewardToCheck) {
- finiteRewardStates = storm::utility::graph::performProb1E(transitions, groupIndices, backwardTransitions, allStates, ~nonZeroRewardMin);
- if ((finiteRewardStates & result.preprocessedModel->getInitialStates()).empty()) {
- // There is no scheduler that induces finite reward for the initial state
- STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "For every scheduler, at least one objective gets infinite reward.");
+ if (storm::utility::graph::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck | minRewardsToCheck)) {
+ // Check whether there is a scheduler yielding infinite reward for a maximizing objective
+ if (storm::utility::graph::checkIfECWithChoiceExists(transitions, backwardTransitions, allStates, maxRewardsToCheck)) {
+ result.rewardFinitenessType = ReturnType::RewardFinitenessType::Infinite;
+ } else {
+ // Check whether there is a scheduler under which all rewards are finite.
+ result.rewardLessInfinityEStates = storm::utility::graph::performProb1E(transitions, groupIndices, backwardTransitions, allStates, result.reward0EStates);
+ if ((result.rewardLessInfinityEStates.get() & result.preprocessedModel->getInitialStates()).empty()) {
+ // There is no scheduler that induces finite reward for the initial state
+ result.rewardFinitenessType = ReturnType::RewardFinitenessType::Infinite;
+ } else {
+ result.rewardFinitenessType = ReturnType::RewardFinitenessType::ExistsParetoFinite;
+ }
}
} else {
- finiteRewardStates = allStates;
+ result.rewardLessInfinityEStates = allStates;
}
- return finiteRewardStates;
+
}
template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
index fe0cf145a..56fb932fb 100644
--- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
+++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h
@@ -5,7 +5,7 @@
#include "storm/logic/Formulas.h"
#include "storm/storage/BitVector.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h"
+#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorTask.h"
#include "storm/storage/memorystructure/MemoryStructure.h"
@@ -21,7 +21,7 @@ namespace storm {
public:
typedef typename SparseModelType::ValueType ValueType;
typedef typename SparseModelType::RewardModelType RewardModelType;
- typedef SparseMultiObjectivePreprocessorReturnType<SparseModelType> ReturnType;
+ typedef SparseMultiObjectivePreprocessorResult<SparseModelType> ReturnType;
/*!
* Preprocesses the given model w.r.t. the given formulas
@@ -79,16 +79,16 @@ namespace storm {
/*!
- * Computes the set of states that have a non-zero reward w.r.t. all objectives, assuming that the objectives are all minimizing and maximizing, respectively.
+ * Computes the set of states that have zero expected reward w.r.t. all expected reward objectives
*/
- static std::pair<storm::storage::BitVector, storm::storage::BitVector> getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
+ static void setReward0States(ReturnType& result, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
/*!
- * Checks whether the occurring expected rewards are finite. If not, the input is rejected.
+ * Checks whether the occurring expected rewards are finite and sets the RewardFinitenessType accordingly
* Returns the set of states for which a scheduler exists that induces finite reward for all objectives
*/
- static storm::storage::BitVector ensureRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::BitVector const& nonZeroRewardMin, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
+ static void checkRewardFiniteness(ReturnType& result, storm::storage::BitVector const& finiteRewardCheckObjectives, storm::storage::SparseMatrix<ValueType> const& backwardTransitions);
};
}
diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h
similarity index 57%
rename from src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h
rename to src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h
index 8143447ed..3486e38ce 100644
--- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h
+++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h
@@ -15,27 +15,49 @@ namespace storm {
namespace multiobjective {
template <class SparseModelType>
- struct SparseMultiObjectivePreprocessorReturnType {
+ struct SparseMultiObjectivePreprocessorResult {
enum class QueryType { Achievability, Quantitative, Pareto };
+ enum class RewardFinitenessType {
+ AllFinite, // The expected reward is finite for all objectives and all schedulers
+ ExistsParetoFinite, // There is a Pareto optimal scheduler yielding finite rewards for all objectives
+ Infinite // All Pareto optimal schedulers yield infinite reward for at least one objective
+ };
+ // Original data
storm::logic::MultiObjectiveFormula const& originalFormula;
SparseModelType const& originalModel;
+
+ // The preprocessed model and objectives
std::shared_ptr<SparseModelType> preprocessedModel;
+ std::vector<Objective<typename SparseModelType::ValueType>> objectives;
+
+ // Data about the query
QueryType queryType;
+ RewardFinitenessType rewardFinitenessType;
- // The (preprocessed) objectives
- std::vector<Objective<typename SparseModelType::ValueType>> objectives;
+ // The states of the preprocessed model for which...
+ storm::storage::BitVector reward0EStates; // ... there is a scheduler such that all expected reward objectives have value zero
+ storm::storage::BitVector reward0AStates; // ... all schedulers induce value 0 for all expected reward objectives
+ boost::optional<storm::storage::BitVector> rewardLessInfinityEStates; // ... there is a scheduler yielding finite reward for all expected reward objectives
+ // Note that other types of objectives (e.g., reward bounded reachability objectives) are not considered.
- // The states for which there is a scheduler such that all objectives have value zero
- storm::storage::BitVector possibleBottomStates;
- // Overapproximation of the set of choices that are part of an end component.
- storm::storage::BitVector possibleECChoices;
+ // Encodes a superset of the set of choices of preprocessedModel that are part of an end component (if given).
+ //boost::optional<storm::storage::BitVector> ecChoicesHint;
- SparseMultiObjectivePreprocessorReturnType(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) : originalFormula(originalFormula), originalModel(originalModel) {
+ SparseMultiObjectivePreprocessorResult(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) : originalFormula(originalFormula), originalModel(originalModel) {
// Intentionally left empty
}
+ bool containsOnlyRewardObjectives() {
+ for (auto const& obj : objectives) {
+ if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula()))) {
+ return false;
+ }
+ }
+ return true;
+ }
+
void printToStream(std::ostream& out) const {
out << std::endl;
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
@@ -62,7 +84,7 @@ namespace storm {
out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
}
- friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorReturnType<SparseModelType> const& ret) {
+ friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorResult<SparseModelType> const& ret) {
ret.printToStream(out);
return out;
}
diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
index 628fbb687..dd20095f2 100644
--- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp
@@ -25,8 +25,8 @@ namespace storm {
template <class SparseModelType>
- SparseCbAchievabilityQuery<SparseModelType>::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) : SparseCbQuery<SparseModelType>(preprocessorResult) {
- STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability, "Invalid query Type");
+ SparseCbAchievabilityQuery<SparseModelType>::SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparseCbQuery<SparseModelType>(preprocessorResult) {
+ STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability, "Invalid query Type");
solver = storm::utility::solver::SmtSolverFactory().create(*this->expressionManager);
}
diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h
index 24e3c3374..2fc2f8f7d 100644
--- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h
+++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h
@@ -19,7 +19,7 @@ namespace storm {
typedef typename SparseModelType::ValueType ValueType;
- SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult);
+ SparseCbAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
virtual ~SparseCbAchievabilityQuery() = default;
diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp
index baac53b0e..529531c2d 100644
--- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp
@@ -18,11 +18,13 @@ namespace storm {
template <class SparseModelType>
- SparseCbQuery<SparseModelType>::SparseCbQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) :
+ SparseCbQuery<SparseModelType>::SparseCbQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) :
originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula),
preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)),
- possibleBottomStates(std::move(preprocessorResult.possibleBottomStates)) {
+ possibleBottomStates(std::move(preprocessorResult.reward0EStates)) {
expressionManager = std::make_shared<storm::expressions::ExpressionManager>();
+ STORM_LOG_WARN("TODO");
+ std::cout << "TODO" << std::endl;
}
diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h
index d3bc42c91..fa3e13119 100644
--- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h
+++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h
@@ -3,7 +3,7 @@
#include <memory>
#include "storm/modelchecker/results/CheckResult.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h"
+#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
#include "storm/storage/expressions/ExpressionManager.h"
namespace storm {
@@ -27,7 +27,7 @@ namespace storm {
protected:
- SparseCbQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult);
+ SparseCbQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
SparseModelType const& originalModel;
storm::logic::MultiObjectiveFormula const& originalFormula;
diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
index cdec9b7c3..a64e471ee 100644
--- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
+++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
@@ -58,13 +58,13 @@ namespace storm {
{
std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> query;
switch (preprocessorResult.queryType) {
- case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability:
+ case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaAchievabilityQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
break;
- case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Quantitative:
+ case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative:
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaQuantitativeQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
break;
- case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Pareto:
+ case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto:
query = std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> (new SparsePcaaParetoQuery<SparseModelType, storm::RationalNumber>(preprocessorResult));
break;
default:
@@ -83,7 +83,7 @@ namespace storm {
{
std::unique_ptr<SparseCbQuery<SparseModelType>> query;
switch (preprocessorResult.queryType) {
- case SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability:
+ case SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability:
query = std::unique_ptr<SparseCbQuery<SparseModelType>> (new SparseCbAchievabilityQuery<SparseModelType>(preprocessorResult));
break;
default:
diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp
index 2c276dbc8..03568318e 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.cpp
@@ -49,16 +49,6 @@ namespace storm {
return std::make_unique<SparseMaPcaaWeightVectorChecker<ModelType>>(model, objectives, possibleECActions, possibleBottomStates);
}
- template <class ModelType>
- bool WeightVectorCheckerFactory<ModelType>::onlyCumulativeOrTotalRewardObjectives(std::vector<Objective<typename ModelType::ValueType>> const& objectives) {
- for (auto const& obj : objectives) {
- if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula()))) {
- return false;
- }
- }
- return true;
- }
-
template class PcaaWeightVectorChecker<storm::models::sparse::Mdp<double>>;
template class PcaaWeightVectorChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class PcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;
diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h
index 83896c236..c6e7f96eb 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h
@@ -5,7 +5,7 @@
#include "storm/storage/Scheduler.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
-#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h"
+#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
#include "storm/modelchecker/multiobjective/Objective.h"
@@ -94,9 +94,6 @@ namespace storm {
std::vector<Objective<typename ModelType::ValueType>> const& objectives,
storm::storage::BitVector const& possibleECActions,
storm::storage::BitVector const& possibleBottomStates);
- private:
-
- static bool onlyCumulativeOrTotalRewardObjectives(std::vector<Objective<typename ModelType::ValueType>> const& objectives);
};
}
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp
index a1d457c11..fde7aa351 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp
@@ -19,8 +19,8 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType>
- SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
- STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Achievability, "Invalid query Type");
+ SparsePcaaAchievabilityQuery<SparseModelType, GeometryValueType>::SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
+ STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Achievability, "Invalid query Type");
initializeThresholdData();
// Set the precision of the weight vector checker. Will be refined during the computation
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h
index fe455e457..70531cdba 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(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult);
+ SparsePcaaAchievabilityQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
virtual ~SparsePcaaAchievabilityQuery() = default;
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
index 21e41614c..778841289 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 <class SparseModelType, typename GeometryValueType>
- SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
- STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Pareto, "Invalid query Type");
+ SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
+ STORM_LOG_ASSERT(preprocessorResult.queryType==SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Pareto, "Invalid query Type");
// Set the precision of the weight vector checker
typename SparseModelType::ValueType weightedPrecision = storm::utility::convertNumber<typename SparseModelType::ValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
index ffcf7bb3d..0e8bb2268 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(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult);
+ SparsePcaaParetoQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
virtual ~SparsePcaaParetoQuery() = default;
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp
index 0405a6022..2bbd64b37 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp
@@ -20,8 +20,8 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType>
- SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
- STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorReturnType<SparseModelType>::QueryType::Quantitative, "Invalid query Type");
+ SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) : SparsePcaaQuery<SparseModelType, GeometryValueType>(preprocessorResult) {
+ STORM_LOG_ASSERT(preprocessorResult.queryType == SparseMultiObjectivePreprocessorResult<SparseModelType>::QueryType::Quantitative, "Invalid query Type");
for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
if (!this->objectives[objIndex].formula->hasBound()) {
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h
index d28ea4e9f..89e3fd111 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(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult);
+ SparsePcaaQuantitativeQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
virtual ~SparsePcaaQuantitativeQuery() = default;
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
index 63fa840e0..55fdf5d6d 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
@@ -20,11 +20,14 @@ namespace storm {
template <class SparseModelType, typename GeometryValueType>
- SparsePcaaQuery<SparseModelType, GeometryValueType>::SparsePcaaQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult) :
+ SparsePcaaQuery<SparseModelType, GeometryValueType>::SparsePcaaQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult) :
originalModel(preprocessorResult.originalModel), originalFormula(preprocessorResult.originalFormula),
preprocessedModel(std::move(*preprocessorResult.preprocessedModel)), objectives(std::move(preprocessorResult.objectives)) {
- this->weightVectorChecker = WeightVectorCheckerFactory<SparseModelType>::create(preprocessedModel, objectives, preprocessorResult.possibleECChoices, preprocessorResult.possibleBottomStates);
+ STORM_LOG_WARN("TODO");
+ std::cout << "TODO" << std::endl;
+
+ this->weightVectorChecker = WeightVectorCheckerFactory<SparseModelType>::create(preprocessedModel, objectives, storm::storage::BitVector(preprocessedModel.getNumberOfChoices(), true), preprocessorResult.reward0EStates);
this->diracWeightVectorsToBeChecked = storm::storage::BitVector(this->objectives.size(), true);
this->overApproximation = storm::storage::geometry::Polytope<GeometryValueType>::createUniversalPolytope();
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h
index 7a5588a3d..f6996e493 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/SparseMultiObjectivePreprocessorReturnType.h"
+#include "storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h"
#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h"
#include "storm/storage/geometry/Polytope.h"
@@ -52,7 +52,7 @@ namespace storm {
* Creates a new query for the Pareto curve approximation algorithm (Pcaa)
* @param preprocessorResult the result from preprocessing
*/
- SparsePcaaQuery(SparseMultiObjectivePreprocessorReturnType<SparseModelType>& preprocessorResult);
+ SparsePcaaQuery(SparseMultiObjectivePreprocessorResult<SparseModelType>& preprocessorResult);
/*
* Returns a weight vector w that separates the under approximation from the given point p, i.e.,
diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp
index 062a7fca6..dfda0fd97 100644
--- a/src/storm/models/sparse/Model.cpp
+++ b/src/storm/models/sparse/Model.cpp
@@ -154,7 +154,7 @@ namespace storm {
template<typename ValueType, typename RewardModelType>
void Model<ValueType, RewardModelType>::addRewardModel(std::string const& rewardModelName, RewardModelType const& newRewardModel) {
- if(this->hasRewardModel(rewardModelName)) {
+ if (this->hasRewardModel(rewardModelName)) {
STORM_LOG_THROW(!(this->hasRewardModel(rewardModelName)), storm::exceptions::IllegalArgumentException, "A reward model with the given name '" << rewardModelName << "' already exists.");
}
STORM_LOG_ASSERT(newRewardModel.isCompatible(this->getNumberOfStates(), this->getTransitionMatrix().getRowCount()), "New reward model is not compatible.");
@@ -165,12 +165,25 @@ namespace storm {
bool Model<ValueType, RewardModelType>::removeRewardModel(std::string const& rewardModelName) {
auto it = this->rewardModels.find(rewardModelName);
bool res = (it != this->rewardModels.end());
- if(res) {
+ if (res) {
this->rewardModels.erase(it->first);
}
return res;
}
+ template<typename ValueType, typename RewardModelType>
+ void Model<ValueType, RewardModelType>::restrictRewardModels(std::set<std::string> const& keptRewardModels) {
+ std::set<std::string> removedRewardModels;
+ for (auto const& rewModel : this->getRewardModels()) {
+ if (keptRewardModels.find(rewModel.first) == keptRewardModels.end()) {
+ removedRewardModels.insert(rewModel.first);
+ }
+ }
+ for (auto const& rewModelName : removedRewardModels) {
+ this->removeRewardModel(rewModelName);
+ }
+ }
+
template<typename ValueType, typename RewardModelType>
bool Model<ValueType, RewardModelType>::hasUniqueRewardModel() const {
return this->getNumberOfRewardModels() == 1;
diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h
index 5e52a9e12..147cb793b 100644
--- a/src/storm/models/sparse/Model.h
+++ b/src/storm/models/sparse/Model.h
@@ -190,6 +190,11 @@ namespace storm {
* @return true, iff such a reward model existed
*/
bool removeRewardModel(std::string const& rewardModelName);
+
+ /*!
+ * Removes all reward models whose name is not in the given set
+ */
+ void restrictRewardModels(std::set<std::string> const& keptRewardModels);
/*!
* Returns the state labeling associated with this model.