From d60afed273dcef7be7ac6de77c35941ca276c745 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 11 Feb 2016 10:45:20 +0100
Subject: [PATCH] MA model checking can be called now for doubles

Former-commit-id: a20f2babc4e950e720a8e5f346de5921d6843592
---
 src/utility/storm.h | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/utility/storm.h b/src/utility/storm.h
index 11dfe6d91..f297d9e41 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -59,6 +59,7 @@
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/helper/SparseCtmcCslHelper.h"
+#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
 #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
@@ -297,6 +298,13 @@ namespace storm {
 
             storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
             result = modelchecker.check(task);
+        } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) {
+            std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
+
+            storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>> modelchecker(*ma);
+            result = modelchecker.check(task);
+        } else {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported.");
         }
         return result;