started on MDP partition refiner

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;
+            }
+            
+        }
+    }
+}

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.

src/storm/storage/dd/bisimulation/PreservationInformation.h

@@ -11,7 +11,6 @@ namespace storm {
             
             class PreservationInformation {
             public:
-                
                 PreservationInformation() = default;
                 
                 void addLabel(std::string const& label);