more on total rewards

Former-commit-id: f25801534a

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp

@@ -128,6 +128,8 @@ namespace storm {
                     preprocessFormula(formula.getSubformula().asEventuallyFormula(), data, currentObjective, formula.getOptionalRewardModelName());
                 } else if(formula.getSubformula().isCumulativeRewardFormula()) {
                     preprocessFormula(formula.getSubformula().asCumulativeRewardFormula(), data, currentObjective, formula.getOptionalRewardModelName());
+                } else if(formula.getSubformula().isTotalRewardFormula()) {
+                    preprocessFormula(formula.getSubformula().asTotalRewardFormula(), data, currentObjective, formula.getOptionalRewardModelName());
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported.");
                 }
@@ -240,6 +242,15 @@ namespace storm {
                 data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards));
             }
             
+            template<typename SparseModelType>
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
+                std::vector<ValueType> objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix());
+                if(!currentObjective.rewardsArePositive){
+                    storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one<ValueType>());
+                }
+                data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards));
+            }
+            
             template class SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<double>>;
 
             

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h

@@ -45,6 +45,7 @@ namespace storm {
                 static void preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
                 static void preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
                 static void preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
+                static void preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
                 
             };
             

src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp

@@ -10,6 +10,7 @@
 #include "src/utility/macros.h"
 #include "src/utility/solver.h"
 #include "src/utility/vector.h"
+
 #include "src/exceptions/IllegalFunctionCallException.h"
 
 namespace storm {
@@ -61,12 +62,19 @@ namespace storm {
             
             template <class SparseModelType>
             void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(std::vector<ValueType> const& weightVector) {
+                bool hasUnboundedObjective;
                 std::vector<ValueType> weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
                 for(uint_fast64_t objIndex = 0; objIndex < weightVector.size(); ++objIndex) {
                     if(!data.objectives[objIndex].stepBound){
+                        hasUnboundedObjective = true;
                         storm::utility::vector::addScaledVector(weightedRewardVector, data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector(), weightVector[objIndex]);
                     }
                 }
+                if(!hasUnboundedObjective) {
+                    this->weightedResult = std::vector<ValueType>(data.preprocessedModel.getNumberOfStates(), storm::utility::zero<ValueType>());
+                    this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates());
+                    return;
+                }
                 
                 // TODO check for +/- infty reward...
                 
@@ -163,7 +171,9 @@ namespace storm {
             
             template <class SparseModelType>
             void SparseMultiObjectiveWeightVectorChecker<SparseModelType>::boundedPhase(std::vector<ValueType> const& weightVector) {
-                STORM_LOG_WARN("bounded properties not yet implemented");
+                for(uint_fast64_t objIndex = 0; objIndex < weightVector.size(); ++objIndex) {
+                    STORM_LOG_THROW(!data.objectives[objIndex].stepBound, storm::exceptions::IllegalFunctionCallException, "Bounded objectives not yet implemented.");
+                }
             }