diff --git a/src/storm/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index 38226702d..f0c17576d 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -37,22 +37,6 @@ namespace storm { // Intentionally left empty } - template - Mdp Mdp::restrictChoices(storm::storage::BitVector const& enabledChoices) const { - storm::storage::sparse::ModelComponents newComponents(this->getTransitionMatrix().restrictRows(enabledChoices)); - newComponents.stateLabeling = this->getStateLabeling(); - for (auto const& rewardModel : this->getRewardModels()) { - newComponents.rewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices)); - } - if (this->hasChoiceLabeling()) { - newComponents.choiceLabeling = this->getChoiceLabeling().getSubLabeling(enabledChoices); - } - newComponents.stateValuations = this->getOptionalStateValuations(); - if (this->hasChoiceOrigins()) { - newComponents.choiceOrigins = this->getChoiceOrigins()->selectChoices(enabledChoices); - } - return Mdp(std::move(newComponents)); - } template uint_least64_t Mdp::getChoiceIndex(storm::storage::StateActionPair const& stateactPair) const { diff --git a/src/storm/models/sparse/Mdp.h b/src/storm/models/sparse/Mdp.h index e65770275..9ee06fc22 100644 --- a/src/storm/models/sparse/Mdp.h +++ b/src/storm/models/sparse/Mdp.h @@ -51,13 +51,6 @@ namespace storm { Mdp(Mdp&& other) = default; Mdp& operator=(Mdp&& other) = default; - /*! - * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector. - * - * @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept. - * @return A subMDP. - */ - Mdp restrictChoices(storm::storage::BitVector const& enabledActions) const; /*! * For a state/action pair, get the choice index referring to the state-action pair. diff --git a/src/storm/permissivesched/PermissiveSchedulers.h b/src/storm/permissivesched/PermissiveSchedulers.h index eb09d4b24..cc29f7113 100644 --- a/src/storm/permissivesched/PermissiveSchedulers.h +++ b/src/storm/permissivesched/PermissiveSchedulers.h @@ -2,6 +2,7 @@ #ifndef PERMISSIVESCHEDULERS_H #define PERMISSIVESCHEDULERS_H +#include #include "../logic/ProbabilityOperatorFormula.h" #include "../models/sparse/Mdp.h" #include "../models/sparse/StandardRewardModel.h" @@ -38,7 +39,8 @@ namespace storm { storm::models::sparse::Mdp apply() const { - return mdp.restrictChoices(enabledChoices); + storm::transformer::ChoiceSelector cs(mdp); + return *(cs.transform(enabledChoices)->template as>()); } template diff --git a/src/storm/transformer/ChoiceSelector.cpp b/src/storm/transformer/ChoiceSelector.cpp new file mode 100644 index 000000000..1044cb42c --- /dev/null +++ b/src/storm/transformer/ChoiceSelector.cpp @@ -0,0 +1,26 @@ +#include "storm/transformer/ChoiceSelector.h" +#include "storm/models/sparse/Mdp.h" + +namespace storm { + namespace transformer { + template + std::shared_ptr> ChoiceSelector::transform(storm::storage::BitVector const& enabledActions) const + { + storm::storage::sparse::ModelComponents newComponents(inputModel.getTransitionMatrix().restrictRows(enabledActions)); + newComponents.stateLabeling = inputModel.getStateLabeling(); + for (auto const& rewardModel : inputModel.getRewardModels()) { + newComponents.rewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledActions)); + } + if (inputModel.hasChoiceLabeling()) { + newComponents.choiceLabeling = inputModel.getChoiceLabeling().getSubLabeling(enabledActions); + } + newComponents.stateValuations = inputModel.getOptionalStateValuations(); + if (inputModel.hasChoiceOrigins()) { + newComponents.choiceOrigins = inputModel.getChoiceOrigins()->selectChoices(enabledActions); + } + return std::make_shared>(std::move(newComponents)); + } + + template class ChoiceSelector; + } +} diff --git a/src/storm/transformer/ChoiceSelector.h b/src/storm/transformer/ChoiceSelector.h new file mode 100644 index 000000000..70ed20974 --- /dev/null +++ b/src/storm/transformer/ChoiceSelector.h @@ -0,0 +1,30 @@ +#pragma once + +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/NondeterministicModel.h" + + +namespace storm { + namespace transformer { + + template> + class ChoiceSelector { + public: + ChoiceSelector(storm::models::sparse::NondeterministicModel const& inputModel) : inputModel(inputModel) { + + } + + /*! + * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector. + * + * @param enabledActions A BitVector of lenght numberOfChoices(), which is one iff the action should be kept. + * @return A subMDP. + */ + std::shared_ptr> transform(storm::storage::BitVector const& enabledActions) const; + private: + + storm::models::sparse::NondeterministicModel const& inputModel; + }; + + } +} \ No newline at end of file