diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp index 6396af48d..4a4b37d60 100644 --- a/src/models/sparse/Mdp.cpp +++ b/src/models/sparse/Mdp.cpp @@ -2,6 +2,7 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/utility/constants.h" +#include "src/utility/vector.h" #include "src/adapters/CarlAdapter.h" #include "src/models/sparse/StandardRewardModel.h" @@ -81,7 +82,13 @@ namespace storm { for (auto const& rewardModel : this->getRewardModels()) { newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices)); } - return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getOptionalChoiceLabeling()); + if(this->hasChoiceLabeling()) { + return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional>(storm::utility::vector::filterVector(this->getChoiceLabeling(), enabledChoices))); + } else { + return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional>()); + } + + } template diff --git a/src/models/sparse/StateAnnotation.h b/src/models/sparse/StateAnnotation.h new file mode 100644 index 000000000..42067bf76 --- /dev/null +++ b/src/models/sparse/StateAnnotation.h @@ -0,0 +1,16 @@ +#ifndef STORM_STATEANNOTATION_H +#define STORM_STATEANNOTATION_H + +namespace storm { + namespace models { + namespace sparse { + class StateAnnotation { + public: + virtual std::string stateInfo(uint_fast64_t s) const = 0; + }; + } + } + +} + +#endif //STORM_STATEANNOTATION_H \ No newline at end of file