From aed8e53a29d7294a87ccfcadee3e889e0fd822c8 Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Mon, 24 Aug 2020 22:24:56 +0200
Subject: [PATCH] (HOA-path) AbstractModelChecker: default handling for
 HOAPathFormulas (= reject)

 Conflicts:
	src/storm/modelchecker/AbstractModelChecker.h
---
 src/storm/modelchecker/AbstractModelChecker.cpp |  7 +++++++
 src/storm/modelchecker/AbstractModelChecker.h   | 17 +++++++++--------
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp
index 803ddc711..c4e485d89 100644
--- a/src/storm/modelchecker/AbstractModelChecker.cpp
+++ b/src/storm/modelchecker/AbstractModelChecker.cpp
@@ -73,6 +73,8 @@ namespace storm {
                 return this->computeGloballyProbabilities(env, checkTask.substituteFormula(formula.asGloballyFormula()));
             } else if (formula.isUntilFormula()) {
                 return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula()));
+            } else if (formula.isHOAPathFormula()) {
+                return this->computeHOAPathProbabilities(env, checkTask.substituteFormula(formula.asHOAPathFormula()));
             } else if (formula.isNextFormula()) {
                 return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula()));
             } else if (formula.isConditionalProbabilityFormula()) {
@@ -118,6 +120,11 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
         }
 
+        template<typename ModelType>
+        std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << ".");
+        }
+
         template<typename ModelType>
         std::unique_ptr<CheckResult> AbstractModelChecker<ModelType>::computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
             storm::logic::Formula const& rewardFormula = checkTask.getFormula();
diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h
index 578b83f15..29a5735f5 100644
--- a/src/storm/modelchecker/AbstractModelChecker.h
+++ b/src/storm/modelchecker/AbstractModelChecker.h
@@ -9,12 +9,12 @@
 #include "storm/solver/OptimizationDirection.h"
 
 namespace storm {
-    
+
     class Environment;
-    
+
     namespace modelchecker {
         class CheckResult;
-        
+
         enum class RewardType { Expectation, Variance };
 
         template<typename ModelType>
@@ -39,7 +39,7 @@ namespace storm {
              * @return True iff the model checker can check the given task.
              */
             virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const = 0;
-            
+
             /*!
              * Checks the provided formula.
              *
@@ -47,13 +47,13 @@ namespace storm {
              * @return The verification result.
              */
             virtual std::unique_ptr<CheckResult> check(Environment const& env, CheckTask<storm::logic::Formula, ValueType> const& checkTask);
-            
+
             /*!
              * Checks the provided formula with the default environment.
              * TODO This function is obsolete as soon as the Environment is fully integrated.
              */
             std::unique_ptr<CheckResult> check(CheckTask<storm::logic::Formula, ValueType> const& checkTask);
-            
+
             // The methods to compute probabilities for path formulas.
             virtual std::unique_ptr<CheckResult> computeProbabilities(Environment const& env, CheckTask<storm::logic::Formula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(Environment const& env, CheckTask<storm::logic::ConditionalFormula, ValueType> const& checkTask);
@@ -63,6 +63,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(Environment const& env, CheckTask<storm::logic::GloballyFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(Environment const& env, CheckTask<storm::logic::NextFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask);
+            virtual std::unique_ptr<CheckResult> computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask);
 
             // The methods to compute the rewards for path formulas.
             virtual std::unique_ptr<CheckResult> computeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> const& checkTask);
@@ -72,12 +73,12 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::TotalRewardFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::LongRunAverageRewardFormula, ValueType> const& checkTask);
-            
+
             // The methods to compute the long-run average probabilities and timing measures.
             virtual std::unique_ptr<CheckResult> computeLongRunAverageProbabilities(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::Formula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask<storm::logic::EventuallyFormula, ValueType> const& checkTask);
-            
+
             // The methods to check state formulas.
             virtual std::unique_ptr<CheckResult> checkStateFormula(Environment const& env, CheckTask<storm::logic::StateFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(Environment const& env, CheckTask<storm::logic::AtomicExpressionFormula, ValueType> const& checkTask);