From d6c141b336b116fee293adea67e92e6c2f335f27 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 2 Feb 2016 16:59:56 +0100
Subject: [PATCH] started working on class to capture check-specific settings
 for model checkers

Former-commit-id: b293d25f1cf9ee3f92aed6b53f389bdf45c92d9d
---
 src/modelchecker/CheckSettings.cpp |  9 ++++++
 src/modelchecker/CheckSettings.h   | 49 ++++++++++++++++++++++++++++++
 2 files changed, 58 insertions(+)
 create mode 100644 src/modelchecker/CheckSettings.cpp
 create mode 100644 src/modelchecker/CheckSettings.h

diff --git a/src/modelchecker/CheckSettings.cpp b/src/modelchecker/CheckSettings.cpp
new file mode 100644
index 000000000..93098d1a3
--- /dev/null
+++ b/src/modelchecker/CheckSettings.cpp
@@ -0,0 +1,9 @@
+#include "src/modelchecker/CheckSettings.h"
+
+namespace storm {
+    namespace modelchecker {
+        class CheckSettings {
+            
+        };
+    }
+}
\ No newline at end of file
diff --git a/src/modelchecker/CheckSettings.h b/src/modelchecker/CheckSettings.h
new file mode 100644
index 000000000..cc01800a6
--- /dev/null
+++ b/src/modelchecker/CheckSettings.h
@@ -0,0 +1,49 @@
+#ifndef STORM_MODELCHECKER_CHECKSETTINGS_H_
+#define STORM_MODELCHECKER_CHECKSETTINGS_H_
+
+#include <boost/optional.hpp>
+
+#include "src/solver/OptimizationDirection.h"
+#include "src/logic/ComparisonType.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        /*
+         * This class is used to customize the checking process of a formula.
+         */
+        template<typename ValueType>
+        class CheckSettings {
+        public:
+            /*!
+             * Creates a settings object with the default options.
+             */
+            CheckSettings();
+            
+            /*!
+             * Creates a settings object with the given options.
+             *
+             * @param optimizationDirection If set, the probabilities will be minimized/maximized.
+             * @param onlyInitialStatesRelevant If set to true, the model checker may decide to only compute the values
+             * for the initial states.
+             * @param initialStatesBound The bound with which the initial states will be compared. This may only be set
+             * together with the flag that indicates only initial states of the model are relevant.
+             * @param qualitative A flag specifying whether the property needs to be checked qualitatively, i.e. compared
+             * with bounds 0/1.
+             * @param produceStrategies If supported by the model checker and the model formalism, strategies to achieve
+             * a value will be produced if this flag is set.
+             */
+            CheckSettings(boost::optional<storm::OptimizationDirection> const& optimizationDirection, bool onlyInitialStatesRelevant, boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> const& initialStatesBound, bool qualitative, bool produceStrategies);
+            
+        private:
+            boost::optional<std::pair<storm::logic::ComparisonType, ValueType>> initialStatesBound;
+            boost::optional<storm::OptimizationDirection> optimizationDirection;
+            bool qualitative;
+            bool produceStrategies;
+            bool onlyInitialStatesRelevant;
+        };
+        
+    }
+}
+
+#endif /* STORM_MODELCHECKER_CHECKSETTINGS_H_ */
\ No newline at end of file