From 44ab16d126f917f5fc9785e19d579dd0089ee466 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 24 Mar 2017 11:58:20 +0100
Subject: [PATCH] Added symbolicToSparse transformers for DTMCs and CTMCs

---
 .../SymbolicToSparseTransformer.cpp           | 67 ++++++++++++++++++-
 .../transformer/SymbolicToSparseTransformer.h | 16 +++++
 2 files changed, 81 insertions(+), 2 deletions(-)

diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp
index 5dfbd2b4a..9dcd7f1ea 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.cpp
+++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp
@@ -5,12 +5,42 @@
 #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::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(
+                storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
+            storm::dd::Odd odd = symbolicDtmc.getReachableStates().createOdd();
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(odd, odd);
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            for (auto const& rewardModelNameAndModel : symbolicDtmc.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(odd, odd);
+                }
+                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
+            }
+            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());
+
+            labelling.addLabel("init", symbolicDtmc.getInitialStates().toVector(odd));
+            labelling.addLabel("deadlock", symbolicDtmc.getDeadlockStates().toVector(odd));
+            for(auto const& label : symbolicDtmc.getLabels()) {
+                labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(odd));
+            }
+            return std::make_shared<storm::models::sparse::Dtmc<ValueType>>(transitionMatrix, labelling, rewardModels);
+        }
+
         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) {
@@ -40,11 +70,44 @@ namespace storm {
                 labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
             }
             return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
+        }
 
+        template<storm::dd::DdType Type, typename ValueType>
+        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(
+                storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc) {
+            storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd();
+            storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd);
+            std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
+            for (auto const& rewardModelNameAndModel : symbolicCtmc.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(odd, odd);
+                }
+                rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel<ValueType>(stateRewards, stateActionRewards, transitionRewards));
+            }
+            storm::models::sparse::StateLabeling labelling(transitionMatrix.getRowGroupCount());
 
+            labelling.addLabel("init", symbolicCtmc.getInitialStates().toVector(odd));
+            labelling.addLabel("deadlock", symbolicCtmc.getDeadlockStates().toVector(odd));
+            for(auto const& label : symbolicCtmc.getLabels()) {
+                labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
+            }
+            return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
 
+        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::CUDD, double>;
+        template class SymbolicDtmcToSparseDtmcTransformer<storm::dd::DdType::Sylvan, double>;
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::CUDD, double>;
         template class SymbolicMdpToSparseMdpTransformer<storm::dd::DdType::Sylvan, double>;
+        template class SymbolicCtmcToSparseCtmcTransformer<storm::dd::DdType::CUDD, double>;
+        template class SymbolicCtmcToSparseCtmcTransformer<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
index 7ea46fff4..414d4454b 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.h
+++ b/src/storm/transformer/SymbolicToSparseTransformer.h
@@ -1,15 +1,31 @@
 #pragma once
 
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/symbolic/Mdp.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/symbolic/Ctmc.h"
 
 namespace storm {
     namespace transformer {
 
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicDtmcToSparseDtmcTransformer {
+        public:
+            static std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc);
+        };
+        
         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);
         };
+        
+        template<storm::dd::DdType Type, typename ValueType>
+        class SymbolicCtmcToSparseCtmcTransformer {
+        public:
+            static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc);
+        };
     }
 }