diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 32063b293..4440f1ba3 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -52,7 +52,6 @@ namespace storm { template CheckTask substituteFormula(NewFormulaType const& newFormula) const { CheckTask result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); - result.updateOperatorInformation(); return result; } @@ -68,13 +67,13 @@ namespace storm { } if (operatorFormula.hasBound()) { - if (onlyInitialStatesRelevant) { - this->bound = operatorFormula.getBound(); - } - - if (!optimizationDirection) { - this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; - } + this->bound = operatorFormula.getBound(); + } + + if (operatorFormula.hasOptimalityType()) { + this->optimizationDirection = operatorFormula.getOptimalityType(); + } else if (operatorFormula.hasBound()) { + this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; } if (formula.get().isProbabilityOperatorFormula()) {