From e88a83d9aa9b0bc6135e8f95c885c96ab0807a00 Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Wed, 16 Dec 2020 11:27:48 +0100
Subject: [PATCH] engine now checks smg models

---
 src/storm/utility/Engine.cpp | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp
index d431f5343..e98ccfea2 100644
--- a/src/storm/utility/Engine.cpp
+++ b/src/storm/utility/Engine.cpp
@@ -6,6 +6,7 @@
 #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
+#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h"
 
 #include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
 #include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
@@ -123,8 +124,9 @@ namespace storm {
                         case ModelType::MA:
                             return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::canHandleStatic(checkTask);
                         case ModelType::POMDP:
-                        case ModelType::SMG:
                             return false;
+                        case ModelType::SMG:
+                            return storm::modelchecker::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>>::canHandleStatic(checkTask);
                     }
                     break;
                 case Engine::Hybrid:
@@ -177,10 +179,10 @@ namespace storm {
                             return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>::canHandleStatic(checkTask);
                         case ModelType::CTMC:
                             return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>::canHandleStatic(checkTask);
+                        case ModelType::SMG:
                         case ModelType::MDP:
                         case ModelType::MA:
                         case ModelType::POMDP:
-                        case ModelType::SMG:
                             return false;
                     }
                     break;