From 19839036af3c26b3d348e6ceb883f4f0bdcef2ff Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Wed, 16 Dec 2020 11:47:01 +0100
Subject: [PATCH] AbstractMC passes game formula to the rpatl MC

---
 src/storm/modelchecker/AbstractModelChecker.cpp | 12 ++++++++++++
 src/storm/modelchecker/AbstractModelChecker.h   |  8 +++++---
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp
index 67f03bc9a..8ec5df265 100644
--- a/src/storm/modelchecker/AbstractModelChecker.cpp
+++ b/src/storm/modelchecker/AbstractModelChecker.cpp
@@ -15,6 +15,7 @@
 #include "storm/models/sparse/Ctmc.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/Pomdp.h"
+#include "storm/models/sparse/Smg.h"
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Ctmc.h"
 #include "storm/models/symbolic/Mdp.h"
@@ -53,6 +54,8 @@ namespace storm {
                 return this->checkMultiObjectiveFormula(env, checkTask.substituteFormula(formula.asMultiObjectiveFormula()));
             } else if (formula.isQuantileFormula()){
                 return this->checkQuantileFormula(env, checkTask.substituteFormula(formula.asQuantileFormula()));
+            } else if(formula.isGameFormula()){
+                return this->checkGameFormula(env, checkTask.substituteFormula(formula.asGameFormula()));
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << formula << "' is invalid.");
         }
@@ -321,6 +324,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>::checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker (" << getClassName() << ") does not support the formula: " << checkTask.getFormula() << ".");
+        }
+
         ///////////////////////////////////////////////
         // Explicitly instantiate the template class.
         ///////////////////////////////////////////////
@@ -331,9 +339,11 @@ namespace storm {
         template class AbstractModelChecker<storm::models::sparse::Mdp<double>>;
         template class AbstractModelChecker<storm::models::sparse::Pomdp<double>>;
         template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
+        template class AbstractModelChecker<storm::models::sparse::Smg<double>>;
 
 #ifdef STORM_HAVE_CARL
         template class AbstractModelChecker<storm::models::sparse::Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>>;
+        template class AbstractModelChecker<storm::models::sparse::Smg<double, storm::models::sparse::StandardRewardModel<storm::Interval>>>;
 
         template class AbstractModelChecker<storm::models::sparse::Model<storm::RationalNumber>>;
         template class AbstractModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
@@ -341,12 +351,14 @@ namespace storm {
         template class AbstractModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
         template class AbstractModelChecker<storm::models::sparse::Pomdp<storm::RationalNumber>>;
         template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>;
+        template class AbstractModelChecker<storm::models::sparse::Smg<storm::RationalNumber>>;
 
         template class AbstractModelChecker<storm::models::sparse::Model<storm::RationalFunction>>;
         template class AbstractModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
         template class AbstractModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>;
         template class AbstractModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>>;
         template class AbstractModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>;
+        template class AbstractModelChecker<storm::models::sparse::Smg<storm::RationalFunction>>;
 #endif
         // DD
         template class AbstractModelChecker<storm::models::symbolic::Model<storm::dd::DdType::CUDD, double>>;
diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h
index 80bf18fb6..59149711c 100644
--- a/src/storm/modelchecker/AbstractModelChecker.h
+++ b/src/storm/modelchecker/AbstractModelChecker.h
@@ -88,13 +88,15 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> checkTimeOperatorFormula(Environment const& env, CheckTask<storm::logic::TimeOperatorFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(Environment const& env, CheckTask<storm::logic::LongRunAverageOperatorFormula, ValueType> const& checkTask);
             virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(Environment const& env, CheckTask<storm::logic::UnaryBooleanStateFormula, ValueType> const& checkTask);
-  
+
             // The methods to check multi-objective formulas.
             virtual std::unique_ptr<CheckResult> checkMultiObjectiveFormula(Environment const& env, CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask);
-  
+
             // The methods to check quantile formulas.
             virtual std::unique_ptr<CheckResult> checkQuantileFormula(Environment const& env, CheckTask<storm::logic::QuantileFormula, ValueType> const& checkTask);
-            
+
+            // The methods to check game formulas.
+            virtual std::unique_ptr<CheckResult> checkGameFormula(Environment const& env, CheckTask<storm::logic::GameFormula, ValueType> const& checkTask);
         };
     }
 }