From 45803c547e096f3ecf9f37a7ed09d78093b08b4e Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 3 Sep 2020 16:59:04 +0200
Subject: [PATCH] storm-pars: Fixed an issue in the instantiation model
 checkers where maybestates were cached incorrectly.

---
 .../SparseDtmcInstantiationModelChecker.cpp   | 68 +++++++++++-----
 .../SparseMdpInstantiationModelChecker.cpp    | 80 +++++++++++--------
 src/storm/modelchecker/CheckTask.h            |  8 ++
 3 files changed, 100 insertions(+), 56 deletions(-)

diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
index 5de3d8fd3..9ea15c4f9 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
@@ -42,8 +42,31 @@ namespace storm {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
             }
             ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-            std::unique_ptr<CheckResult> result;
             
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Perform purely qualitative analysis once
+                std::vector<ConstantType> qualitativeResult;
+                if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                    auto newCheckTask = *this->currentCheckTask;
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                } else {
+                    auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                }
+                std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl;
+                storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
+                                [] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value)); });
+                std::cout <<maybeStates << std::endl;
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setResultHint(std::move(qualitativeResult));
+                hint.setComputeOnlyMaybeStates(true);
+            }
+            
+            std::unique_ptr<CheckResult> result;
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
             if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
@@ -56,15 +79,6 @@ namespace storm {
                 hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
             }
             
-            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                // Extract the maybe states from the current result.
-                assert(hint.hasResultHint());
-                storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
-                                [] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
-                hint.setMaybeStates(std::move(maybeStates));
-                hint.setComputeOnlyMaybeStates(true);
-            }
-            
             return result;
         }
         
@@ -75,6 +89,28 @@ namespace storm {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
             }
             ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
+            
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Perform purely qualitative analysis once
+                std::vector<ConstantType> qualitativeResult;
+                if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                    auto newCheckTask = *this->currentCheckTask;
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                } else {
+                    auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                }
+                storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
+                                [] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isInfinity<ConstantType>(value)); });
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setResultHint(std::move(qualitativeResult));
+                hint.setComputeOnlyMaybeStates(true);
+            }
+            
             std::unique_ptr<CheckResult> result;
             
             // Check the formula and store the result as a hint for the next call.
@@ -89,18 +125,6 @@ namespace storm {
                 this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
             }
             
-            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                // Extract the maybe states from the current result.
-                assert(hint.hasResultHint());
-                storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
-                // We need to exclude the target states from the maybe states.
-                // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
-                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
-                maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                hint.setMaybeStates(std::move(maybeStates));
-                hint.setComputeOnlyMaybeStates(true);
-            }
-            
             return result;
         }
         
diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
index 3dc4866d3..0f1e8b9ac 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
@@ -47,8 +47,31 @@ namespace storm {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
             }
             ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-            std::unique_ptr<CheckResult> result;
             
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Perform purely qualitative analysis once
+                std::vector<ConstantType> qualitativeResult;
+                if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                    auto newCheckTask = *this->currentCheckTask;
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                } else {
+                    auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.computeProbabilities(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                }
+                std::cout << storm::utility::vector::toString(qualitativeResult) << std::endl;
+                storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
+                                [] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value)); });
+                std::cout <<maybeStates << std::endl;
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setResultHint(std::move(qualitativeResult));
+                hint.setComputeOnlyMaybeStates(true);
+            }
+            
+            std::unique_ptr<CheckResult> result;
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
             if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
@@ -65,21 +88,6 @@ namespace storm {
                 hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
             }
             
-            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                // Extract the maybe states from the current result.
-                assert(hint.hasResultHint());
-                storm::storage::BitVector maybeStates = ~storm::utility::vector::filter<ConstantType>(hint.getResultHint(),
-                                [] (ConstantType const& value) -> bool { return storm::utility::isZero<ConstantType>(value) || storm::utility::isOne<ConstantType>(value); });
-                hint.setMaybeStates(std::move(maybeStates));
-                hint.setComputeOnlyMaybeStates(true);
-                
-                // Check if there can be end components within the maybestates
-                if (storm::solver::minimize(this->currentCheckTask->getOptimizationDirection()) ||
-                storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
-                    hint.setNoEndComponentsInMaybeStates(true);
-                }
-            }
-            
             return result;
         }
         
@@ -92,8 +100,29 @@ namespace storm {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
             }
             ExplicitModelCheckerHint<ConstantType>& hint = this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>();
-            std::unique_ptr<CheckResult> result;
             
+            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
+                // Perform purely qualitative analysis once
+                std::vector<ConstantType> qualitativeResult;
+                if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                    auto newCheckTask = *this->currentCheckTask;
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.check(env, newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                } else {
+                    auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula());
+                    newCheckTask.setQualitative(true);
+                    newCheckTask.setOnlyInitialStatesRelevant(false);
+                    qualitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask)->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector();
+                }
+                storm::storage::BitVector maybeStates = storm::utility::vector::filter<ConstantType>(qualitativeResult,
+                                [] (ConstantType const& value) -> bool { return !(storm::utility::isZero<ConstantType>(value) || storm::utility::isInfinity<ConstantType>(value)); });
+                hint.setMaybeStates(std::move(maybeStates));
+                hint.setResultHint(std::move(qualitativeResult));
+                hint.setComputeOnlyMaybeStates(true);
+            }
+            
+            std::unique_ptr<CheckResult> result;
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
             if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
@@ -110,23 +139,6 @@ namespace storm {
                 hint.setSchedulerHint(std::move(dynamic_cast<storm::storage::Scheduler<ConstantType>&>(scheduler)));
             }
             
-            if (this->getInstantiationsAreGraphPreserving() && !hint.hasMaybeStates()) {
-                // Extract the maybe states from the current result.
-                assert(hint.hasResultHint());
-                storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
-                // We need to exclude the target states from the maybe states.
-                // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
-                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
-                maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
-                hint.setMaybeStates(std::move(maybeStates));
-                hint.setComputeOnlyMaybeStates(true);
-                
-                // Check if there can be end components within the maybestates
-                if (storm::solver::maximize(this->currentCheckTask->getOptimizationDirection()) ||
-                storm::utility::graph::performProb1A(instantiatedModel.getTransitionMatrix(), instantiatedModel.getTransitionMatrix().getRowGroupIndices(), instantiatedModel.getBackwardTransitions(), hint.getMaybeStates(), ~hint.getMaybeStates()).full()) {
-                    hint.setNoEndComponentsInMaybeStates(true);
-                }
-            }
             return result;
         }
         
diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h
index 45f2a9bc3..898795fda 100644
--- a/src/storm/modelchecker/CheckTask.h
+++ b/src/storm/modelchecker/CheckTask.h
@@ -207,6 +207,14 @@ namespace storm {
             bool isQualitativeSet() const {
                 return qualitative;
             }
+
+            /*!
+             * sets whether the computation only needs to be performed qualitatively, because the values will only
+             * be compared to 0/1.
+             */
+            void setQualitative(bool value) {
+                qualitative = value;
+            }
             
             /*!
              * Sets whether to produce schedulers (if supported).