diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index aebbd1fcf..5a10795b6 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/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) {
diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
index 02a1e94f1..cc7d99bfa 100644
--- a/src/parser/NondeterministicSparseTransitionParser.cpp
+++ b/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.";
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index cb62d529c..f9178b275 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/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];