From ead5845686126be634b747dcc809eec14d094dc2 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 17 Feb 2020 14:28:23 +0100
Subject: [PATCH] BuilderType: Using new canHandle and getSupportedJaniFeatures
 methods.

---
 src/storm/builder/BuilderType.cpp | 57 +++++++++++++++++++++++++++----
 src/storm/builder/BuilderType.h   |  1 +
 src/storm/utility/Engine.cpp      |  2 +-
 3 files changed, 52 insertions(+), 8 deletions(-)

diff --git a/src/storm/builder/BuilderType.cpp b/src/storm/builder/BuilderType.cpp
index 72e106011..6bc7e766a 100644
--- a/src/storm/builder/BuilderType.cpp
+++ b/src/storm/builder/BuilderType.cpp
@@ -1,23 +1,66 @@
 #include "storm/builder/BuilderType.h"
 
+#include "storm/storage/dd/DdType.h"
+
 #include "storm/storage/jani/ModelFeatures.h"
+#include "storm/generator/JaniNextStateGenerator.h"
+#include "storm/generator/PrismNextStateGenerator.h"
+#include "storm/builder/DdJaniModelBuilder.h"
+#include "storm/builder/DdPrismModelBuilder.h"
+#include "storm/builder/jit/ExplicitJitJaniModelBuilder.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace builder {
         
         storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType) {
-            storm::jani::ModelFeatures features;
-            features.add(storm::jani::ModelFeature::DerivedOperators);
-            features.add(storm::jani::ModelFeature::StateExitRewards);
-            if (builderType == BuilderType::Explicit) {
-                features.add(storm::jani::ModelFeature::Arrays);
+            // The supported jani features should be independent of the ValueType and Dd type. We just take sylvan and double for all.
+            storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
+            typedef double ValueType;
+            switch (builderType) {
+                case BuilderType::Explicit:
+                    return storm::generator::JaniNextStateGenerator<ValueType>::getSupportedJaniFeatures();
+                case BuilderType::Dd:
+                    return storm::builder::DdJaniModelBuilder<ddType, ValueType>::getSupportedJaniFeatures();
+                case BuilderType::Jit:
+                    return storm::builder::jit::ExplicitJitJaniModelBuilder<ValueType>::getSupportedJaniFeatures();
+                
             }
-            return features;
+            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected builder type.");
         }
         
+        template <typename ValueType>
         bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription) {
-            return true;
+            storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
+            if (!modelDescription.hasModel()) {
+                // If there is no model to be build, we assume that the task of obtaining a model is either not required or can be accomplished somehow.
+                return true;
+            }
+            STORM_LOG_THROW(modelDescription.isPrismProgram() || modelDescription.isJaniModel(), storm::exceptions::UnexpectedException, "The model is neither PRISM nor Jani which is not expected.");
+            switch (builderType) {
+                case BuilderType::Explicit:
+                    if (modelDescription.isPrismProgram()) {
+                        return storm::generator::PrismNextStateGenerator<ValueType>::canHandle(modelDescription.asPrismProgram());
+                    } else {
+                        return storm::generator::JaniNextStateGenerator<ValueType>::canHandle(modelDescription.asJaniModel());
+                    }
+                case BuilderType::Dd:
+                    if (modelDescription.isPrismProgram()) {
+                        return storm::builder::DdPrismModelBuilder<ddType, ValueType>::canHandle(modelDescription.asPrismProgram());
+                    } else {
+                        return storm::builder::DdJaniModelBuilder<ddType, ValueType>::canHandle(modelDescription.asJaniModel());
+                    }
+                case BuilderType::Jit:
+                    return storm::builder::jit::ExplicitJitJaniModelBuilder<ValueType>::canHandle(modelDescription.asJaniModel());
+            }
         }
         
+
+        
+        template bool canHandle<double>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
+        template bool canHandle<storm::RationalNumber>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
+        
     }
 }
\ No newline at end of file
diff --git a/src/storm/builder/BuilderType.h b/src/storm/builder/BuilderType.h
index 297596ce1..a5732a950 100644
--- a/src/storm/builder/BuilderType.h
+++ b/src/storm/builder/BuilderType.h
@@ -16,6 +16,7 @@ namespace storm {
         
         storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType);
         
+        template <typename ValueType>
         bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
     }
 }
\ No newline at end of file
diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp
index 4441d9a07..a2b315822 100644
--- a/src/storm/utility/Engine.cpp
+++ b/src/storm/utility/Engine.cpp
@@ -152,7 +152,7 @@ namespace storm {
                 return false;
             }
             // Check whether the model builder can handle the model description
-            return storm::builder::canHandle(getBuilderType(engine), modelDescription);
+            return storm::builder::canHandle<ValueType>(getBuilderType(engine), modelDescription);
         }
         
         // explicit template instantiations.