From f258afa8a2cf034c3a3d5e718addb76622bfe172 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Wed, 22 May 2019 18:29:41 +0200
Subject: [PATCH] Added basis for DFT transformator

---
 .../transformations/DftTransformator.cpp      | 34 +++++++++++++++++++
 .../transformations/DftTransformator.h        | 30 ++++++++++++++++
 2 files changed, 64 insertions(+)
 create mode 100644 src/storm-dft/transformations/DftTransformator.cpp
 create mode 100644 src/storm-dft/transformations/DftTransformator.h

diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp
new file mode 100644
index 000000000..cb89c336a
--- /dev/null
+++ b/src/storm-dft/transformations/DftTransformator.cpp
@@ -0,0 +1,34 @@
+#include "DftTransformator.h"
+
+namespace storm {
+    namespace transformations {
+        namespace dft {
+            template<typename ValueType>
+            DftTransformator<ValueType>::DftTransformator(storm::storage::DFT<ValueType> const &dft) : mDft(dft) {}
+
+            template<typename ValueType>
+            storm::storage::DFT<ValueType> DftTransformator<ValueType>::transformUniqueFailedBe() {
+                // For now, this only creates an empty DFT
+                storm::builder::DFTBuilder<ValueType> builder;
+
+                for (size_t i = 0; i < mDft.nrElements(); ++i) {
+                    std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = mDft.getElement(i);
+                    //TODO SWITCH OVER ELEMENTS
+                }
+                //builder.setTopLevel(mDft.getTopLevelGate()->name());
+                return builder.build();
+            }
+
+            // Explicitly instantiate the class.
+            template
+            class DftTransformator<double>;
+
+#ifdef STORM_HAVE_CARL
+
+            template
+            class DftTransformator<RationalFunction>;
+
+#endif
+        }
+    }
+}
diff --git a/src/storm-dft/transformations/DftTransformator.h b/src/storm-dft/transformations/DftTransformator.h
new file mode 100644
index 000000000..59872ec51
--- /dev/null
+++ b/src/storm-dft/transformations/DftTransformator.h
@@ -0,0 +1,30 @@
+#include "storm-dft/storage/dft/DFT.h"
+#include "storm-dft/builder/DFTBuilder.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace transformations {
+        namespace dft {
+
+            /*!
+             * Transformator for DFT -> DFT.
+             */
+            template<typename ValueType>
+            class DftTransformator {
+
+            public:
+                /*!
+                 * Constructor.
+                 *
+                 * @param dft DFT
+                 */
+                DftTransformator(storm::storage::DFT<ValueType> const &dft);
+
+                storm::storage::DFT<ValueType> transformUniqueFailedBe();
+
+            private:
+                storm::storage::DFT<ValueType> const &mDft;
+            };
+        }
+    }
+}