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 + std::shared_ptr> SymbolicDtmcToSparseDtmcTransformer::translate( + storm::models::symbolic::Dtmc const& symbolicDtmc) { + storm::dd::Odd odd = symbolicDtmc.getReachableStates().createOdd(); + storm::storage::SparseMatrix transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(odd, odd); + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicDtmc.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(odd, odd); + } + rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel(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>(transitionMatrix, labelling, rewardModels); + } + template std::shared_ptr> SymbolicMdpToSparseMdpTransformer::translate( storm::models::symbolic::Mdp const& symbolicMdp) { @@ -40,11 +70,44 @@ namespace storm { labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd)); } return std::make_shared>(transitionMatrix, labelling, rewardModels); + } + template + std::shared_ptr> SymbolicCtmcToSparseCtmcTransformer::translate( + storm::models::symbolic::Ctmc const& symbolicCtmc) { + storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd(); + storm::storage::SparseMatrix transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd); + std::unordered_map> rewardModels; + for (auto const& rewardModelNameAndModel : symbolicCtmc.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(odd, odd); + } + rewardModels.emplace(rewardModelNameAndModel.first,storm::models::sparse::StandardRewardModel(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>(transitionMatrix, labelling, rewardModels); } + template class SymbolicDtmcToSparseDtmcTransformer; + template class SymbolicDtmcToSparseDtmcTransformer; template class SymbolicMdpToSparseMdpTransformer; template class SymbolicMdpToSparseMdpTransformer; + template class SymbolicCtmcToSparseCtmcTransformer; + template class SymbolicCtmcToSparseCtmcTransformer; } -} \ 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 + class SymbolicDtmcToSparseDtmcTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::Dtmc const& symbolicDtmc); + }; + template class SymbolicMdpToSparseMdpTransformer { public: static std::shared_ptr> translate(storm::models::symbolic::Mdp const& symbolicMdp); }; + + template + class SymbolicCtmcToSparseCtmcTransformer { + public: + static std::shared_ptr> translate(storm::models::symbolic::Ctmc const& symbolicCtmc); + }; } }