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 + std::shared_ptr> SymbolicMdpToSparseMdpTransformer::translate( + storm::models::symbolic::Mdp const& symbolicMdp) { + storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd(); + storm::storage::SparseMatrix transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd); + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicMdp.getRewardModels()) { + boost::optional> stateRewards; + boost::optional> stateActionRewards; + boost::optional> 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(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>(transitionMatrix, labelling, rewardModels); + + + } + + template class SymbolicMdpToSparseMdpTransformer; + template class SymbolicMdpToSparseMdpTransformer; + } +} \ 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 + class SymbolicMdpToSparseMdpTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::Mdp const& symbolicMdp); + }; + } +}