Added proper creation of row grouping to nondeterministic model parser and the explicit model adapter.

Former-commit-id: 723ddb2e1d

src/adapters/ExplicitModelAdapter.h

@@ -543,6 +543,7 @@ namespace storm {
                             // If the model is nondeterministic, we add all choices individually.
                             nondeterministicChoiceIndices.push_back(currentRow);
                             transitionMatrixBuilder.newRowGroup(currentRow);
+                            transitionRewardMatrixBuilder.newRowGroup(currentRow);
                             
                             // First, process all unlabeled choices.
                             for (auto const& choice : allUnlabeledChoices) {

src/parser/NondeterministicSparseTransitionParser.cpp

@@ -264,22 +264,22 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
 	 *	Those two values, as well as the number of nonzero elements, was been calculated in the first run.
 	 */
 	LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << choices << " x " << (maxnode+1) << " with " << nonzero << " entries.");
-	storm::storage::SparseMatrixBuilder<double> matrixBuilder(choices, maxnode + 1, nonzero);
-
+	storm::storage::SparseMatrixBuilder<double> matrixBuilder(choices, maxnode + 1, nonzero, true);
+    
 	/*
 	 *	Create row mapping.
 	 */
 	std::vector<uint_fast64_t> rowMapping(maxnode + 2, 0);
-
+    
 	/*
 	 *	Parse file content.
 	 */
 	int_fast64_t source, target, lastsource = -1, choice, lastchoice = -1;
-	uint_fast64_t curRow = -1;
+	int_fast64_t curRow = -1;
 	double val;
 	bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
 	bool hadDeadlocks = false;
-
+    
 	/*
 	 *	Read all transitions from file.
 	 */
@@ -300,12 +300,14 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
 			// If we skipped some states, we need to reserve empty rows for all their nondeterministic
 			// choices.
 			for (int_fast64_t i = lastsource + 1; i < source; ++i) {
+                matrixBuilder.newRowGroup(curRow + 1);
 				curRow += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
 			}
 
 			// If we advanced to the next state, but skipped some choices, we have to reserve rows
 			// for them
 			if (source != lastsource) {
+                matrixBuilder.newRowGroup(curRow + 1);
 				curRow += choice + 1;
 			} else if (choice != lastchoice) {
 				curRow += choice - lastchoice;
@@ -325,6 +327,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
 				hadDeadlocks = true;
 				if (fixDeadlocks) {
 					rowMapping.at(node) = curRow;
+                    matrixBuilder.newRowGroup(curRow);
 					matrixBuilder.addNextValue(curRow, node, 1);
 					++curRow;
 					LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
@@ -337,6 +340,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
 				 *	Add this source to rowMapping, if this is the first choice we encounter for this state.
 				 */
 				rowMapping.at(source) = curRow;
+                matrixBuilder.newRowGroup(curRow);
 			}
 		}
 
@@ -373,9 +377,21 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP
 		buf = trimWhitespaces(buf);
 	}
 
-	for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; node++) {
-		rowMapping.at(node) = curRow + 1;
-	}
+    if (isRewardFile) {
+        for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; ++node) {
+            rowMapping.at(node) = curRow + 1;
+            if (node <= maxnode) {
+                matrixBuilder.newRowGroup((*rewardMatrixInformation->nondeterministicChoiceIndices)[node]);
+            }
+        }
+    } else {
+        for (int_fast64_t node = lastsource + 1; node <= maxnode + 1; ++node) {
+            rowMapping.at(node) = curRow + 1;
+            if (node <= maxnode) {
+                matrixBuilder.newRowGroup(curRow + 1);
+            }
+        }
+    }
 
 	if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
 

src/storage/SparseMatrix.cpp

@@ -99,7 +99,9 @@ namespace storm {
         template<typename T>
         void SparseMatrixBuilder<T>::newRowGroup(uint_fast64_t startingRow) {
             if (!hasCustomRowGrouping) {
-                throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::addRowGroup: matrix was not created to have a custom row grouping.";
+                throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: matrix was not created to have a custom row grouping.";
+            } else if (rowGroupIndices.size() > 0 && startingRow < rowGroupIndices.back()) {
+                throw storm::exceptions::InvalidStateException() << "Illegal call to SparseMatrix::newRowGroup: illegal row group with negative size.";
             }
             if (rowGroupCountSet) {
                 rowGroupIndices[currentRowGroup] = startingRow;
@@ -837,9 +839,8 @@ namespace storm {
             // Check for matching sizes.
             if (this->getRowCount() != matrix.getRowCount()) return false;
             if (this->getColumnCount() != matrix.getColumnCount()) return false;
-            
             if (this->getRowGroupIndices() != matrix.getRowGroupIndices()) return false;
-            
+
             // Check the subset property for all rows individually.
             for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) {
                 for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = matrix.begin(row), ite2 = matrix.end(row); it1 != ite1; ++it1) {
@@ -866,7 +867,7 @@ namespace storm {
             
             // Iterate over all row groups.
             for (uint_fast64_t group = 0; group < matrix.getRowGroupCount(); ++group) {
-                out << "\t---- group " << group << " ----" << std::endl;
+                out << "\t---- group " << group << " ---- out of " << (matrix.getRowGroupCount() - 1) << " ---- " << std::endl;
                 for (uint_fast64_t i = matrix.getRowGroupIndices()[group]; i < matrix.getRowGroupIndices()[group + 1]; ++i) {
                     uint_fast64_t nextIndex = matrix.rowIndications[i];