From e5b526b7aef0974e40b607fac678c16a0d07a904 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 15 Feb 2017 16:23:50 +0100
Subject: [PATCH] SymbolicToSparseModel: MDPs

---
 .../SymbolicToSparseTransformer.cpp           | 50 +++++++++++++++++++
 .../transformer/SymbolicToSparseTransformer.h | 15 ++++++
 2 files changed, 65 insertions(+)
 create mode 100644 src/storm/transformer/SymbolicToSparseTransformer.cpp
 create mode 100644 src/storm/transformer/SymbolicToSparseTransformer.h

diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp
new file mode 100644
index 000000000..4cb266354
--- /dev/null
+++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp
@@ -0,0 +1,50 @@
+#include "SymbolicToSparseTransformer.h"
+
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
+#include "storm/storage/dd/Bdd.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+
+
+#include "storm/models/sparse/StandardRewardModel.h"
+
+namespace storm {
+    namespace transformer {
+
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(
+                storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp) {
+            storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd();
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd);
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) {
+                boost::optional<std::vector<ValueType>> stateRewards;
+                boost::optional<std::vector<ValueType>> stateActionRewards;
+                boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewards;
+                if (rewardModelNameAndModel.second.hasStateRewards()) {
+                    stateRewards = rewardModelNameAndModel.second.getStateRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasStateActionRewards()) {
+                    stateActionRewards = rewardModelNameAndModel.second.getStateActionRewardVector().toVector(odd);
+                }
+                if (rewardModelNameAndModel.second.hasTransitionRewards()) {
+                    transitionRewards = rewardModelNameAndModel.second.getTransitionRewardMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd);
+                }
+                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
+            }
+            storm::models::sparse::StateLabeling labelling;
+
+            labelling.addLabel("initial", symbolicMdp.getInitialStates().toVector(odd));
+            labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd));
+            for(auto const& label : symbolicMdp.getLabels()) {
+                labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
+            }
+            return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
+
+
+        }
+
+        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
+        template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
+    }
+}
\ No newline at end of file
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h
new file mode 100644
index 000000000..7ea46fff4
--- /dev/null
+++ b/src/storm/transformer/SymbolicToSparseTransformer.h
@@ -0,0 +1,15 @@
+#pragma once
+
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/symbolic/Mdp.h"
+
+namespace storm {
+    namespace transformer {
+
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicMdpToSparseMdpTransformer {
+        public:
+            static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp);
+        };
+    }
+}