diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h index 460ba3ec2..523098148 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h @@ -48,12 +48,24 @@ namespace storm { return true; } + bool containsLongRunAverageRewardFormulas() const { + for (auto const& obj : objectives) { + if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isLongRunAverageRewardFormula()) { + return true; + } + } + return false; + } + bool containsOnlyTrivialObjectives() const { - // Trivial objectives are either total reward formulas or single-dimensional step or time bounded cumulative reward formulas + // Trivial objectives are either total reward formulas, LRA reward formulas or single-dimensional step or time bounded cumulative reward formulas for (auto const& obj : objectives) { if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) { continue; } + if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isLongRunAverageRewardFormula()) { + continue; + } if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isCumulativeRewardFormula()) { auto const& subf = obj.formula->getSubformula().asCumulativeRewardFormula(); if (!subf.isMultiDimensional() && (subf.getTimeBoundReference().isTimeBound() || subf.getTimeBoundReference().isStepBound())) {