started to make multi-objective preprocessing more flexible w.r.t. different checkers

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>>;

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);
                 
             };
         }

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h → 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;
                 }

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);
             }
 

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;
 

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;
             }
             
             

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;

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:

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>>;

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);
             };
 
         }

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

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;
 

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());

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;
 

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()) {

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;
 

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();

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.,

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;

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.