From 2ba70e964c24e91f3b7834344f8b299eaf1f4c8b Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 18 May 2018 13:45:25 +0200
Subject: [PATCH] Added hasParameters() and supportsParameters() for symbolic
 models

---
 src/storm/models/sparse/Model.cpp   |  4 ----
 src/storm/models/symbolic/Model.cpp | 21 +++++++++++++++++++++
 src/storm/models/symbolic/Model.h   | 10 ++++++++++
 3 files changed, 31 insertions(+), 4 deletions(-)

diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp
index 4bece4dcf..9ee91b5dd 100644
--- a/src/storm/models/sparse/Model.cpp
+++ b/src/storm/models/sparse/Model.cpp
@@ -423,11 +423,7 @@ namespace storm {
             
             template<typename ValueType, typename RewardModelType>
             bool Model<ValueType, RewardModelType>::supportsParameters() const {
-#ifdef STORM_HAVE_CARL
                 return std::is_same<ValueType, storm::RationalFunction>::value;
-#else
-		return false;
-#endif
             }
             
             template<typename ValueType, typename RewardModelType>
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index ee90118cb..f7a9f367f 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -15,6 +15,7 @@
 
 #include "storm/models/symbolic/StandardRewardModel.h"
 
+#include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/dd.h"
 
@@ -362,6 +363,26 @@ namespace storm {
             bool Model<Type, ValueType>::isSymbolicModel() const {
                 return true;
             }
+
+            template<storm::dd::DdType Type, typename ValueType>
+            bool Model<Type, ValueType>::supportsParameters() const {
+                return std::is_same<ValueType, storm::RationalFunction>::value;
+            }
+            
+            template<storm::dd::DdType Type, typename ValueType>
+            bool Model<Type, ValueType>::hasParameters() const {
+                if (!this->supportsParameters()) {
+                    return false;
+                }
+                // Check for parameters
+                for (auto it = this->getTransitionMatrix().begin(false); it != this->getTransitionMatrix().end(); ++it) {
+                    if (!storm::utility::isConstant((*it).second)) {
+                        return true;
+                    }
+                }
+                // Only constant values present
+                return false;
+            }
             
             template<storm::dd::DdType Type, typename ValueType>
             void Model<Type, ValueType>::addParameters(std::set<storm::RationalFunctionVariable> const& parameters) {
diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h
index 1dca3dc6d..7b3500bd1 100644
--- a/src/storm/models/symbolic/Model.h
+++ b/src/storm/models/symbolic/Model.h
@@ -321,6 +321,16 @@ namespace storm {
                 
                 virtual bool isSymbolicModel() const override;
 
+                virtual bool supportsParameters() const override;
+                
+                /*!
+                 * Checks whether the model has parameters.
+                 * Performance warning: the worst-case complexity is linear in the number of transitions.
+                 *
+                 * @return True iff the model has parameters.
+                 */
+                virtual bool hasParameters() const override;
+
                 std::vector<std::string> getLabels() const;
                 
                 void addParameters(std::set<storm::RationalFunctionVariable> const& parameters);