sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added symbolicToSparse transformers for DTMCs and CTMCs

tempestpy_adaptions
TimQu 8 years ago
parent
acd486f0f2
commit
44ab16d126
2 changed files with 81 additions and 2 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 67
      src/storm/transformer/SymbolicToSparseTransformer.cpp
  2. 16
      src/storm/transformer/SymbolicToSparseTransformer.h

67
src/storm/transformer/SymbolicToSparseTransformer.cpp
View File

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

16
src/storm/transformer/SymbolicToSparseTransformer.h
View File

@ -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);
};
}
}
Write Preview
Loading…
Cancel
Save