made rowMapping from NDSTParser available in MDP model class

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<storm::storage::SparseMatrix<T>> probabilityMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+			std::shared_ptr<storm::parser::RowStateMapping> rowMapping,
 			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> 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<T> &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<T>(*mdp.backwardTransitions);
@@ -226,6 +228,9 @@ private:
 	/*! The labeling of the states of the MDP. */
 	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
 	
+	/*! The mapping from rows to (state,choice) pairs. */
+	std::shared_ptr<storm::parser::RowStateMapping> rowMapping;
+
 	/*! The state-based rewards of the MDP. */
 	std::shared_ptr<std::vector<T>> stateRewards;
 

src/parser/MdpParser.cpp

@@ -45,7 +45,7 @@ MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const
 		transitionRewards = trp.getMatrix();
 	}
 
-	mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards));
+	mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), tp.getRowMapping(), stateRewards, transitionRewards));
 }
 
 } /* namespace parser */

src/parser/NonDeterministicSparseTransitionParser.cpp

@@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 	/*
 	 *	Create row mapping.
 	 */
-	this->rowMapping = std::shared_ptr<RowMapping>(new RowMapping());
+	this->rowMapping = std::shared_ptr<RowStateMapping>(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<uint_fast64_t, std::string>(node, "")));
+				this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(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<uint_fast64_t, std::string>(source, choice)));
+		this->rowMapping->insert(RowStateMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice)));
 
 		/*
 		 *	Skip name of choice.

src/parser/NonDeterministicSparseTransitionParser.h

@@ -14,6 +14,8 @@
 namespace storm {
 namespace parser {
 	
+typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> 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<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowMapping;
-		inline std::shared_ptr<RowMapping> getRowMapping() const {
+		inline std::shared_ptr<RowStateMapping> getRowMapping() const {
 			return this->rowMapping;
 		}
 	
 	private:
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
-		std::shared_ptr<RowMapping> rowMapping;
+		std::shared_ptr<RowStateMapping> rowMapping;
 		
 		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);