diff --git a/src/models/Mdp.h b/src/models/Mdp.h index dc58782a2..26922b573 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -20,6 +20,7 @@ #include "src/utility/CommandLine.h" #include "src/utility/Settings.h" #include "src/models/AbstractModel.h" +#include "src/parser/NonDeterministicSparseTransitionParser.h" namespace storm { @@ -44,9 +45,10 @@ public: */ Mdp(std::shared_ptr> probabilityMatrix, std::shared_ptr stateLabeling, + std::shared_ptr rowMapping, std::shared_ptr> stateRewards = nullptr, std::shared_ptr> transitionRewardMatrix = nullptr) - : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), + : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping), stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), backwardTransitions(nullptr) { if (!this->checkValidityOfProbabilityMatrix()) { @@ -61,7 +63,7 @@ public: * @param mdp A reference to the MDP that is to be copied. */ Mdp(const Mdp &mdp) : probabilityMatrix(mdp.probabilityMatrix), - stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards), + stateLabeling(mdp.stateLabeling), rowMapping(mdp.rowMapping), stateRewards(mdp.stateRewards), transitionRewardMatrix(mdp.transitionRewardMatrix) { if (mdp.backwardTransitions != nullptr) { this->backwardTransitions = new storm::models::GraphTransitions(*mdp.backwardTransitions); @@ -225,6 +227,9 @@ private: /*! The labeling of the states of the MDP. */ std::shared_ptr stateLabeling; + + /*! The mapping from rows to (state,choice) pairs. */ + std::shared_ptr rowMapping; /*! The state-based rewards of the MDP. */ std::shared_ptr> stateRewards; diff --git a/src/parser/MdpParser.cpp b/src/parser/MdpParser.cpp index f73c0b515..ac73b4e40 100644 --- a/src/parser/MdpParser.cpp +++ b/src/parser/MdpParser.cpp @@ -45,7 +45,7 @@ MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const transitionRewards = trp.getMatrix(); } - mdp = std::shared_ptr>(new storm::models::Mdp(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); + mdp = std::shared_ptr>(new storm::models::Mdp(tp.getMatrix(), lp.getLabeling(), tp.getRowMapping(), stateRewards, transitionRewards)); } } /* namespace parser */ diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp index 1eb270739..93c8d779d 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.cpp +++ b/src/parser/NonDeterministicSparseTransitionParser.cpp @@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s /* * Create row mapping. */ - this->rowMapping = std::shared_ptr(new RowMapping()); + this->rowMapping = std::shared_ptr(new RowStateMapping()); /* * Parse file content. @@ -245,7 +245,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s for (int_fast64_t node = lastsource + 1; node < source; node++) { hadDeadlocks = true; if (fixDeadlocks) { - this->rowMapping->insert(RowMapping::value_type(curRow, std::pair(node, ""))); + this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair(node, ""))); this->matrix->addNextValue(curRow, node, 1); curRow++; LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); @@ -258,7 +258,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s /* * Add this source-choice pair to rowMapping. */ - this->rowMapping->insert(RowMapping::value_type(curRow, std::pair(source, choice))); + this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair(source, choice))); /* * Skip name of choice. diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h index 592e2814f..5edc0a72e 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.h +++ b/src/parser/NonDeterministicSparseTransitionParser.h @@ -14,6 +14,8 @@ namespace storm { namespace parser { +typedef boost::bimap> RowStateMapping; + /*! * @brief Load a nondeterministic transition system from file and create a * sparse adjacency matrix whose entries represent the weights of the edges @@ -26,14 +28,13 @@ class NonDeterministicSparseTransitionParser : public Parser { return this->matrix; } - typedef boost::bimap> RowMapping; - inline std::shared_ptr getRowMapping() const { + inline std::shared_ptr getRowMapping() const { return this->rowMapping; } private: std::shared_ptr> matrix; - std::shared_ptr rowMapping; + std::shared_ptr rowMapping; uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);