Browse Source

added functionalities in MultiObjectivePreprocessorResult to capture lra objectives

tempestpy_adaptions
TimQu 4 years ago
parent
commit
a5342d8b83
  1. 14
      src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h

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

Loading…
Cancel
Save