diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp index a3da9b1d4..f091b364b 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp +++ b/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 + void SparseMultiObjectivePreprocessor::preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName) { + std::vector objectiveRewards = data.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : "").getTotalRewardVector(data.preprocessedModel.getTransitionMatrix()); + if(!currentObjective.rewardsArePositive){ + storm::utility::vector::scaleVectorInPlace(objectiveRewards, -storm::utility::one()); + } + data.preprocessedModel.addRewardModel(currentObjective.rewardModelName, RewardModelType(boost::none, objectiveRewards)); + } + template class SparseMultiObjectivePreprocessor>; diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h index 580fbeef0..10ce6f9bb 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h +++ b/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 const& optionalRewardModelName = boost::none); static void preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessFormula(storm::logic::TotalRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional const& optionalRewardModelName = boost::none); }; diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index bbd3f0b0c..0f1b88684 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/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 void SparseMultiObjectiveWeightVectorChecker::unboundedWeightedPhase(std::vector const& weightVector) { + bool hasUnboundedObjective; std::vector weightedRewardVector(data.preprocessedModel.getTransitionMatrix().getRowCount(), storm::utility::zero()); 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(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); + this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates()); + return; + } // TODO check for +/- infty reward... @@ -163,7 +171,9 @@ namespace storm { template void SparseMultiObjectiveWeightVectorChecker::boundedPhase(std::vector 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."); + } }