From 48d5025bd91e6492834074c3a70e80ada520b0dd Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 4 Apr 2017 10:58:43 +0200
Subject: [PATCH] Fixed checking of formulas whose subformulas contain an
 OperatorFormula (like nested OperatorFormulas or conjunctions of
 Operatorformulas).

---
 .../modelchecker/AbstractModelChecker.cpp     |  4 +-
 src/storm/modelchecker/CheckTask.h            | 62 +++++++++++--------
 2 files changed, 38 insertions(+), 28 deletions(-)

diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp
index 675adbaf4..78f6e7d93 100644
--- a/src/storm/modelchecker/AbstractModelChecker.cpp
+++ b/src/storm/modelchecker/AbstractModelChecker.cpp
@@ -219,9 +219,9 @@ namespace storm {
             storm::logic::ProbabilityOperatorFormula const& stateFormula = checkTask.getFormula();
             std::unique_ptr<CheckResult> result = this->computeProbabilities(checkTask.substituteFormula(stateFormula.getSubformula()));
             
-            if (stateFormula.hasBound()) {
+            if (checkTask.isBoundSet()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->asQuantitativeCheckResult<ValueType>().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThresholdAs<ValueType>());
+                return result->asQuantitativeCheckResult<ValueType>().compareAgainstBound(checkTask.getBoundComparisonType(), checkTask.getBoundThreshold());
             } else {
                 return result;
             }
diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h
index 6221237ec..f93db2d10 100644
--- a/src/storm/modelchecker/CheckTask.h
+++ b/src/storm/modelchecker/CheckTask.h
@@ -40,8 +40,27 @@ namespace storm {
                 this->produceSchedulers = false;
                 this->qualitative = false;
                 
-                if (formula.isOperatorFormula()) {
-                    storm::logic::OperatorFormula const& operatorFormula = formula.asOperatorFormula();
+                updateOperatorInformation();
+            }
+            
+            /*!
+             * Copies the check task from the source while replacing the formula with the new one. In particular, this
+             * changes the formula type of the check task object.
+             */
+            template<typename NewFormulaType>
+            CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
+                CheckTask<NewFormulaType, ValueType> result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->resultHint);
+                result.updateOperatorInformation();
+                return result;
+            }
+            
+            /*!
+             * If the currently specified formula is an OperatorFormula, this method updates the information that is given in the Operator formula.
+             * Calling this method has no effect if the provided formula is not an operator formula.
+             */
+            void updateOperatorInformation() {
+                if (formula.get().isOperatorFormula()) {
+                    storm::logic::OperatorFormula const& operatorFormula = formula.get().asOperatorFormula();
                     if (operatorFormula.hasOptimalityType()) {
                         this->optimizationDirection = operatorFormula.getOptimalityType();
                     }
@@ -55,37 +74,28 @@ namespace storm {
                             this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize;
                         }
                     }
-                }
                 
-                if (formula.isProbabilityOperatorFormula()) {
-                    storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
-                    
-                    if (probabilityOperatorFormula.hasBound()) {
-                        if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs<ValueType>()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs<ValueType>())) {
-                            this->qualitative = true;
+                    if (formula.get().isProbabilityOperatorFormula()) {
+                        storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.get().asProbabilityOperatorFormula();
+                        
+                        if (probabilityOperatorFormula.hasBound()) {
+                            if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs<ValueType>()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs<ValueType>())) {
+                                this->qualitative = true;
+                            }
                         }
-                    }
-                } else if (formula.isRewardOperatorFormula()) {
-                    storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
-                    this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
-                    
-                    if (rewardOperatorFormula.hasBound()) {
-                        if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs<ValueType>())) {
-                            this->qualitative = true;
+                    } else if (formula.get().isRewardOperatorFormula()) {
+                        storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.get().asRewardOperatorFormula();
+                        this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
+                        
+                        if (rewardOperatorFormula.hasBound()) {
+                            if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs<ValueType>())) {
+                                this->qualitative = true;
+                            }
                         }
                     }
                 }
             }
             
-            /*!
-             * Copies the check task from the source while replacing the formula with the new one. In particular, this
-             * changes the formula type of the check task object.
-             */
-            template<typename NewFormulaType>
-            CheckTask<NewFormulaType, ValueType> substituteFormula(NewFormulaType const& newFormula) const {
-                return CheckTask<NewFormulaType, ValueType>(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->resultHint);
-            }
-            
             /*!
              * Retrieves the formula from this task.
              */