From 78c0245d16d1acc602ca27435e690ef957785a81 Mon Sep 17 00:00:00 2001
From: gereon <gereon.kremer@rwth-aachen.de>
Date: Sat, 12 Jan 2013 20:30:36 +0100
Subject: [PATCH] Added rowMapping to MDP transition parser.

the rowMapping is a bijective mapping (-> boost::bimap) between the row number and the (node,choice) pair.
---
 .../NonDeterministicSparseTransitionParser.cpp      | 13 +++++++++++--
 src/parser/NonDeterministicSparseTransitionParser.h | 10 +++++++++-
 2 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp
index c0029834d..e632b3dd9 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NonDeterministicSparseTransitionParser.cpp
@@ -209,6 +209,11 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 	}
 	this->matrix->initialize(nonzero);
 	
+	/*
+	 *	Create row mapping.
+	 */
+	this->rowMapping = std::shared_ptr<RowMapping>(new RowMapping());
+	
 	/*
 	 *	Parse file content.
 	 */
@@ -234,11 +239,12 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 		/*
 		 *	Check if we have skipped any source node, i.e. if any node has no
 		 *	outgoing transitions. If so, insert a self-loop.
+		 *	Also add self-loops to rowMapping.
 		 */
 		for (uint_fast64_t node = lastsource + 1; node < source; node++) {
 			hadDeadlocks = true;
 			if (fixDeadlocks) {
-				// TODO: add (curRow <-> (node,"")) to rowMapping
+				this->rowMapping->insert( RowMapping::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.");
@@ -248,7 +254,10 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 		}
 		lastsource = source;
 		
-		// TODO: add (curRow <-> (node,choice)) to rowMapping
+		/*
+		 *	Add this source-choice pair to rowMapping.
+		 */
+		this->rowMapping->insert( RowMapping::value_type( curRow, std::pair<uint_fast64_t,std::string>(source, choice)) );
 
 		/*
 		 *	Skip name of choice.
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h
index 004885a42..5b487d5a2 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NonDeterministicSparseTransitionParser.h
@@ -6,6 +6,8 @@
 #include "src/parser/Parser.h"
 #include "src/utility/OsDetection.h"
 
+#include <boost/bimap.hpp>
+#include <utility>
 #include <memory>
 #include <vector>
 
@@ -20,12 +22,18 @@ class NonDeterministicSparseTransitionParser : public Parser {
 	public:
 		NonDeterministicSparseTransitionParser(std::string const &filename);
 		
-		std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
+		inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
 			return this->matrix;
 		}
+		
+		typedef boost::bimap<uint_fast64_t, std::pair<uint_fast64_t,std::string>> RowMapping;
+		inline std::shared_ptr<RowMapping> getRowMapping() const {
+			return this->rowMapping;
+		}
 	
 	private:
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
+		std::shared_ptr<RowMapping> rowMapping;
 		
 		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode);