Fixed a few things in the parsers and implemented proper treatment of reward files by these parsers.

src/parser/DeterministicModelParser.cpp

@@ -45,7 +45,7 @@ DeterministicModelParser::DeterministicModelParser(std::string const & transitio
 		this->stateRewards = srp.getStateRewards();
 	}
 	if (transitionRewardFile != "") {
-		storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile);
+		storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, true);
 		this->transitionRewards = trp.getMatrix();
 	}
 	this->dtmc = nullptr;

src/parser/DeterministicSparseTransitionParser.cpp

@@ -44,12 +44,14 @@ namespace parser {
  *	@param buf Data to scan. Is expected to be some char array.
  *	@param maxnode Is set to highest id of all nodes.
  */
-uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) {
+uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, bool rewardFile) {
 	uint_fast64_t nonZeroEntryCount = 0;
 	/*
 	 *	Check file header and extract number of transitions.
 	 */
+	if (!rewardFile) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
+	}
 
     /*
      * Check all transitions for non-zero diagonal entries and deadlock states.
@@ -66,6 +68,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
             row = checked_strtol(buf, &buf);
             col = checked_strtol(buf, &buf);
 
+            if (!rewardFile) {
 				if (lastRow != row) {
 					if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
 						++nonZeroEntryCount;
@@ -84,6 +87,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
 					rowHadDiagonalEntry = true;
 					++nonZeroEntryCount;
 				}
+            }
 
             /*
              *      Check if one is larger than the current maximum id.
@@ -105,7 +109,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
             buf = trimWhitespaces(buf);
     }
 
-    if (!rowHadDiagonalEntry) {
+    if (!rowHadDiagonalEntry && !rewardFile) {
     	++nonZeroEntryCount;
     }
 
@@ -122,7 +126,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
  *	@return a pointer to the created sparse matrix.
  */
 
-DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing)
+DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, bool rewardFile)
 	: matrix(nullptr) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
@@ -139,7 +143,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	 *	Perform first pass, i.e. count entries that are not zero.
 	 */
 	int_fast64_t maxStateId;
-	uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId);
+	uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardFile);
 
 	LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros.");
 
@@ -160,7 +164,9 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	/*
 	 *	Read file header, extract number of states.
 	 */
+	if (!rewardFile) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
+	}
 
 	/*
 	 *	Creating matrix here.
@@ -198,7 +204,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 				if (insertDiagonalEntriesIfMissing) {
 					this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
 					LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
-				} else {
+				} else if (!rewardFile) {
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
 				}
 				// No increment for lastRow
@@ -206,11 +212,11 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 			}
 			for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
 				hadDeadlocks = true;
-				if (fixDeadlocks) {
+				if (fixDeadlocks && !rewardFile) {
 					this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<double>());
 					rowHadDiagonalEntry = true;
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
-				} else {
+				} else if (!rewardFile) {
 					LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
 					// FIXME Why no exception at this point? This will break the App.
 				}
@@ -223,10 +229,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 			rowHadDiagonalEntry = true;
 		} else if (col > row && !rowHadDiagonalEntry) {
 			rowHadDiagonalEntry = true;
-			if (insertDiagonalEntriesIfMissing) {
+			if (insertDiagonalEntriesIfMissing && !rewardFile) {
 				this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
 				LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
-			} else {
+			} else if (!rewardFile) {
 				LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
 			}
 		}
@@ -236,10 +242,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
 	}
 
 	if (!rowHadDiagonalEntry) {
-		if (insertDiagonalEntriesIfMissing) {
+		if (insertDiagonalEntriesIfMissing && !rewardFile) {
 			this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
 			LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
-		} else {
+		} else if (!rewardFile) {
 			LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
 		}
 	}

src/parser/DeterministicSparseTransitionParser.h

@@ -17,7 +17,7 @@ namespace parser {
  */
 class DeterministicSparseTransitionParser : public Parser {
 	public:
-		DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true);
+		DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, bool rewardFile = false);
 		
 		std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
 			return this->matrix;
@@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser {
 	private:
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
 		
-		uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode);
+		uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, bool rewardFile);
 	
 };
 		

src/parser/NondeterministicModelParser.cpp

@@ -38,7 +38,7 @@ NondeterministicModelParser::NondeterministicModelParser(std::string const & tra
 		this->stateRewards = srp.getStateRewards();
 	}
 	if (transitionRewardFile != "") {
-		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile);
+		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, true, tp.getRowMapping());
 		this->transitionRewardMatrix = trp.getMatrix();
 	}
 

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -49,11 +49,13 @@ namespace parser {
  *	@param maxnode Is set to highest id of all nodes.
  *	@return The number of non-zero elements.
  */
-uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
+uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices) {
 	/*
 	 *	Check file header and extract number of transitions.
 	 */
+	if (!rewardFile) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
+	}
 
 	/*
 	 *	Read all transitions.
@@ -78,6 +80,27 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 			maxnode = source;
 		}
 
+		if (rewardFile) {
+			// If we have switched the source state, we possibly need to insert the rows of the last
+			// last source state.
+			if (source != lastsource && lastsource != -1) {
+				choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
+			}
+
+			// If we skipped some states, we need to reserve empty rows for all their nondeterministic
+			// choices.
+			for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
+				choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
+			}
+
+			// If we advanced to the next state, but skipped some choices, we have to reserve rows
+			// for them
+			if (source != lastsource) {
+				choices += choice + 1;
+			} else if (choice != lastchoice) {
+				choices += choice - lastchoice;
+			}
+		} else {
 			// If we have skipped some states, we need to reserve the space for the self-loop insertion
 			// in the second pass.
 			if (source > lastsource + 1) {
@@ -88,6 +111,7 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 				// reserve one row more.
 				++choices;
 			}
+		}
 
 		// Read target and check if we encountered a state index that is bigger than all previously
 		// seen.
@@ -127,6 +151,17 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
 		buf = trimWhitespaces(buf);
 	}
 
+	if (rewardFile) {
+		// If not all rows were filled for the last state, we need to insert them.
+		choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
+
+		// If we skipped some states, we need to reserve empty rows for all their nondeterministic
+		// choices.
+		for (uint_fast64_t i = lastsource + 1; i < nondeterministicChoiceIndices->size() - 1; ++i) {
+			choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
+		}
+	}
+
 	return nonzero;
 }
 
@@ -140,7 +175,7 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
  *	@return a pointer to the created sparse matrix.
  */
 
-NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename)
+NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices)
 	: matrix(nullptr) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
@@ -158,7 +193,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	 */
 	int_fast64_t maxnode;
 	uint_fast64_t choices;
-	uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode);
+	uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardFile, nondeterministicChoiceIndices);
 
 	/*
 	 *	If first pass returned zero, the file format was wrong.
@@ -177,7 +212,9 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 	/*
 	 *	Skip file header.
 	 */
+	if (!rewardFile) {
 		buf = strchr(buf, '\n') + 1;  // skip format hint
+	}
 
 	/*
 	 *	Create and initialize matrix.
@@ -216,12 +253,32 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 		source = checked_strtol(buf, &buf);
 		choice = checked_strtol(buf, &buf);
 
+		if (rewardFile) {
+			// If we have switched the source state, we possibly need to insert the rows of the last
+			// last source state.
+			if (source != lastsource && lastsource != -1) {
+				curRow += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
+			}
+
+			// If we skipped some states, we need to reserve empty rows for all their nondeterministic
+			// choices.
+			for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
+				curRow += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
+			}
+
+			// If we advanced to the next state, but skipped some choices, we have to reserve rows
+			// for them
+			if (source != lastsource) {
+				curRow += choice + 1;
+			} else if (choice != lastchoice) {
+				curRow += choice - lastchoice;
+			}
+		} else {
 			// Increase line count if we have either finished reading the transitions of a certain state
 			// or we have finished reading one nondeterministic choice of a state.
 			if ((source != lastsource || choice != lastchoice)) {
 				++curRow;
 			}
-
 			/*
 			 *	Check if we have skipped any source node, i.e. if any node has no
 			 *	outgoing transitions. If so, insert a self-loop.
@@ -229,12 +286,12 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 			 */
 			for (int_fast64_t node = lastsource + 1; node < source; node++) {
 				hadDeadlocks = true;
-			if (fixDeadlocks) {
+				if (!rewardFile && fixDeadlocks) {
 					this->rowMapping->at(node) = curRow;
 					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.");
-			} else {
+				} else if (!rewardFile) {
 					LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
 				}
 			}
@@ -244,6 +301,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 				 */
 				this->rowMapping->at(source) = curRow;
 			}
+		}
 
 		// Read target and value and write it to the matrix.
 		target = checked_strtol(buf, &buf);
@@ -265,7 +323,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
 
 	this->rowMapping->at(maxnode+1) = curRow + 1;
 
-	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
+	if (!fixDeadlocks && hadDeadlocks && !rewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*
 	 * Finalize matrix.

src/parser/NondeterministicSparseTransitionParser.h

@@ -19,7 +19,7 @@ namespace parser {
  */
 class NondeterministicSparseTransitionParser : public Parser {
 	public:
-		NondeterministicSparseTransitionParser(std::string const &filename);
+		NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile = false, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices = nullptr);
 		
 		inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
 			return this->matrix;
@@ -33,7 +33,7 @@ class NondeterministicSparseTransitionParser : public Parser {
 		std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
 		std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
 		
-		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode);
+		uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices);
 	
 };