From a5342d8b83dd6c3bf633dbfa39a3c3f16b210644 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 9 Sep 2020 10:56:13 +0200 Subject: [PATCH] added functionalities in MultiObjectivePreprocessorResult to capture lra objectives --- .../SparseMultiObjectivePreprocessorResult.h | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) 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())) {