From 277faf6673e2c6d0df5e1a884dbe0f43a3575a6c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 1 Aug 2017 12:49:56 +0200
Subject: [PATCH] started on MDP partition refiner

---
 .../dd/bisimulation/MdpPartitionRefiner.cpp   | 29 +++++++++++++++++++
 .../dd/bisimulation/PartitionRefiner.h        |  4 +--
 .../dd/bisimulation/PreservationInformation.h |  1 -
 3 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp

diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
new file mode 100644
index 000000000..033f5f5f0
--- /dev/null
+++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp
@@ -0,0 +1,29 @@
+#include "storm/storage/dd/bisimulation/MdpPartitionRefiner.h"
+
+namespace storm {
+    namespace dd {
+        namespace bisimulation {
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            MdpPartitionRefiner<DdType, ValueType>::MdpPartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition) : PartitionRefiner<DdType, ValueType>(model, initialStatePartition) {
+                // Start by initializing the choice signature refiner.
+                std::set<storm::expressions::Variable> choiceSignatureVariables;
+                std::set_union(model.getRowMetaVariables().begin(), model.getRowMetaVariables().end(), model.getNondeterminismVariables().begin(), model.getNondeterminismVariables().end(), std::inserter(choiceSignatureVariables, choiceSignatureVariables.begin()));
+                choiceSignatureRefiner = SignatureRefiner<DdType, ValueType>(model.getManager(), this->statePartition.getBlockVariable(), choiceSignatureVariables);
+                
+                // Create dummy choice partition that is refined to the right result in the first call to refine.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            bool MdpPartitionRefiner<DdType, ValueType>::refine(bisimulation::SignatureMode const& mode) {
+                // Magic here.
+            }
+            
+            template<storm::dd::DdType DdType, typename ValueType>
+            Partition<DdType, ValueType> const& MdpPartitionRefiner<DdType, ValueType>::getChoicePartition() const {
+                return choicePartition;
+            }
+            
+        }
+    }
+}
diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h
index 413889300..c5ccae949 100644
--- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h
+++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h
@@ -40,7 +40,7 @@ namespace storm {
                  */
                 Status getStatus() const;
                 
-            private:
+            protected:
                 // The current status.
                 Status status;
                 
@@ -53,7 +53,7 @@ namespace storm {
                 // The object used to compute the signatures.
                 SignatureComputer<DdType, ValueType> signatureComputer;
                 
-                // The object used to refine the partition(s) based on the signatures.
+                // The object used to refine the state partition based on the signatures.
                 SignatureRefiner<DdType, ValueType> signatureRefiner;
                 
                 // Time measurements.
diff --git a/src/storm/storage/dd/bisimulation/PreservationInformation.h b/src/storm/storage/dd/bisimulation/PreservationInformation.h
index e936d3b0d..1aa2620bd 100644
--- a/src/storm/storage/dd/bisimulation/PreservationInformation.h
+++ b/src/storm/storage/dd/bisimulation/PreservationInformation.h
@@ -11,7 +11,6 @@ namespace storm {
             
             class PreservationInformation {
             public:
-                
                 PreservationInformation() = default;
                 
                 void addLabel(std::string const& label);