From 0a65e4aa7bab828345d2eca7e6b10e921837e6dc Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Wed, 16 Dec 2020 11:42:54 +0100
Subject: [PATCH] verification now handles SMGs

---
 src/storm/api/verification.h | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h
index 3e5f916a5..b878a6a7a 100644
--- a/src/storm/api/verification.h
+++ b/src/storm/api/verification.h
@@ -18,6 +18,7 @@
 #include "storm/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h"
 #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
 #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
+#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h"
 
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/symbolic/Mdp.h"
@@ -25,6 +26,7 @@
 
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/Smg.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
@@ -251,6 +253,28 @@ namespace storm {
             return verifyWithSparseEngine(env, ma, task);
         }
 
+        template<typename ValueType>
+        typename std::enable_if<std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& smg, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
+            std::unique_ptr<storm::modelchecker::CheckResult> result;
+            storm::modelchecker::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>> modelchecker(*smg);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(env, task);
+            }
+            return result;
+        }
+
+        template<typename ValueType>
+        typename std::enable_if<!std::is_same<ValueType, double>::value, std::unique_ptr<storm::modelchecker::CheckResult>>::type verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& mdp, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify SMGs with this data type.");
+        }
+
+        template<typename ValueType>
+        std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Smg<ValueType>> const& smg, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
+            Environment env;
+            return verifyWithSparseEngine(env, smg, task);
+        }
+
+
         template<typename ValueType>
         std::unique_ptr<storm::modelchecker::CheckResult> verifyWithSparseEngine(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task) {
             std::unique_ptr<storm::modelchecker::CheckResult> result;
@@ -262,6 +286,8 @@ namespace storm {
                 result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Ctmc<ValueType>>(), task);
             } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
                 result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(), task);
+            } else if (model->getType() == storm::models::ModelType::Smg) {
+                result = verifyWithSparseEngine(env, model->template as<storm::models::sparse::Smg<ValueType>>(), task);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported by the sparse engine.");
             }