From 7795ce5f35e28366d79e4f4681d0e0cc10965de1 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 6 Aug 2020 14:51:29 +0200
Subject: [PATCH] ModelCheckerHelper: Added utility function that copies model
 checking information from one helper to another.

---
 .../modelchecker/helper/ModelCheckerHelper.h  |  6 ++--
 .../utility/SetInformationFromOtherHelper.h   | 31 +++++++++++++++++++
 2 files changed, 35 insertions(+), 2 deletions(-)
 create mode 100644 src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h

diff --git a/src/storm/modelchecker/helper/ModelCheckerHelper.h b/src/storm/modelchecker/helper/ModelCheckerHelper.h
index 05169ae17..02ee35531 100644
--- a/src/storm/modelchecker/helper/ModelCheckerHelper.h
+++ b/src/storm/modelchecker/helper/ModelCheckerHelper.h
@@ -14,12 +14,14 @@ namespace storm {
             
             /*!
              * Helper class for solving a model checking query.
-             * @tparam ValueType The type of a single value.
+             * @tparam VT The value type of a single value.
              * @tparam DdType The used library for Dds (or None in case of a sparse representation).
              */
-            template <typename ValueType, storm::dd::DdType DdType = storm::dd::DdType::None>
+            template <typename VT, storm::dd::DdType DdType = storm::dd::DdType::None>
             class ModelCheckerHelper {
             public:
+                typedef VT ValueType;
+
                 ModelCheckerHelper() = default;
                 ~ModelCheckerHelper() = default;
                 
diff --git a/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h b/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h
new file mode 100644
index 000000000..44dcc467c
--- /dev/null
+++ b/src/storm/modelchecker/helper/utility/SetInformationFromOtherHelper.h
@@ -0,0 +1,31 @@
+#pragma once
+
+#include "storm/modelchecker/CheckTask.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+            
+            /*!
+             * Forwards relevant information stored in another helper to the given helper
+             */
+            template <typename TargetHelperType, typename SourceHelperType>
+            void setInformationFromOtherHelperNondeterministic(TargetHelperType& targetHelper, SourceHelperType const& sourceHelperType, std::function<typename TargetHelperType::StateSet(typename SourceHelperType::StateSet const&)> const& stateSetTransformer) {
+                // Relevancy of initial states.
+			    if (sourceHelperType.hasRelevantStates()) {
+			        targetHelper.setRelevantStates(stateSetTransformer(sourceHelperType.getRelevantStates()));
+			    }
+                // Value threshold to which the result will be compared
+			    if (sourceHelperType.isValueThresholdSet()) {
+			        targetHelper.setValueThreshold(sourceHelperType.getValueThresholdComparisonType(), storm::utility::convertNumber<typename TargetHelperType::ValueType>(sourceHelperType.getValueThresholdValue()));
+			    }
+			    // Optimization direction
+                if (sourceHelperType.isOptimizationDirectionSet()) {
+                    targetHelper.setOptimizationDirection(sourceHelperType.getOptimizationDirection());
+                }
+                // Scheduler Production
+			    targetHelper.setProduceScheduler(sourceHelperType.isProduceSchedulerSet());
+            }
+        }
+    }
+}
\ No newline at end of file