diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp
index 9aacb7e4c..94a66b066 100644
--- a/src/storm/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp
@@ -46,8 +46,7 @@ namespace storm {
char const* buf = file.getData();
// Perform first pass, i.e. count entries that are not zero.
- bool insertDiagonalEntriesIfMissing = !isRewardFile;
- DeterministicSparseTransitionParser<ValueType>::FirstPassResult firstPass = DeterministicSparseTransitionParser<ValueType>::firstPass(file.getData(), insertDiagonalEntriesIfMissing);
+ DeterministicSparseTransitionParser<ValueType>::FirstPassResult firstPass = DeterministicSparseTransitionParser<ValueType>::firstPass(file.getData());
STORM_LOG_TRACE("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " non-zeros.");
@@ -85,7 +84,6 @@ namespace storm {
double val;
bool dontFixDeadlocks = storm::settings::getModule<storm::settings::modules::CoreSettings>().isDontFixDeadlocksSet();
bool hadDeadlocks = false;
- bool rowHadDiagonalEntry = false;
// Read all transitions from file. Note that we assume that the
// transitions are listed in canonical order, otherwise this will not
@@ -131,16 +129,6 @@ namespace storm {
// Test if we moved to a new row.
// Handle all incomplete or skipped rows.
if (lastRow != row) {
- if (!rowHadDiagonalEntry) {
- if (insertDiagonalEntriesIfMissing) {
- resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero<ValueType>());
- STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
- } else {
- STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
- }
- // No increment for lastRow.
- rowHadDiagonalEntry = true;
- }
for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
hadDeadlocks = true;
if (!dontFixDeadlocks) {
@@ -152,36 +140,12 @@ namespace storm {
}
}
lastRow = row;
- rowHadDiagonalEntry = false;
- }
-
- if (col == row) {
- rowHadDiagonalEntry = true;
- }
-
- if (col > row && !rowHadDiagonalEntry) {
- if (insertDiagonalEntriesIfMissing) {
- resultMatrix.addNextValue(row, row, storm::utility::zero<ValueType>());
- STORM_LOG_DEBUG("While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
- } else {
- STORM_LOG_WARN("Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
- }
- rowHadDiagonalEntry = true;
}
resultMatrix.addNextValue(row, col, val);
buf = trimWhitespaces(buf);
}
- if (!rowHadDiagonalEntry) {
- if (insertDiagonalEntriesIfMissing) {
- resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero<ValueType>());
- STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
- } else {
- STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
- }
- }
-
// If we encountered deadlock and did not fix them, now is the time to throw the exception.
if (dontFixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the states do not have outgoing transitions.";
}
@@ -199,7 +163,7 @@ namespace storm {
}
template<typename ValueType>
- typename DeterministicSparseTransitionParser<ValueType>::FirstPassResult DeterministicSparseTransitionParser<ValueType>::firstPass(char const* buf, bool insertDiagonalEntriesIfMissing) {
+ typename DeterministicSparseTransitionParser<ValueType>::FirstPassResult DeterministicSparseTransitionParser<ValueType>::firstPass(char const* buf) {
DeterministicSparseTransitionParser<ValueType>::FirstPassResult result;
@@ -231,30 +195,6 @@ namespace storm {
// The actual read value is not needed here.
checked_strtod(buf, &buf);
- // Compensate for missing diagonal entries if desired.
- if (insertDiagonalEntriesIfMissing) {
- if (lastRow != row) {
- if (!rowHadDiagonalEntry) {
- ++result.numberOfNonzeroEntries;
- }
-
- // Compensate for missing rows.
- for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
- ++result.numberOfNonzeroEntries;
- }
- rowHadDiagonalEntry = false;
- }
-
- if (col == row) {
- rowHadDiagonalEntry = true;
- }
-
- if (col > row && !rowHadDiagonalEntry) {
- rowHadDiagonalEntry = true;
- ++result.numberOfNonzeroEntries;
- }
- }
-
// Check if a higher state id was found.
if (row > result.highestStateIndex) result.highestStateIndex = row;
if (col > result.highestStateIndex) result.highestStateIndex = col;
@@ -273,17 +213,6 @@ namespace storm {
buf = trimWhitespaces(buf);
}
- if (insertDiagonalEntriesIfMissing) {
- if (!rowHadDiagonalEntry) {
- ++result.numberOfNonzeroEntries;
- }
-
- //Compensate for missing rows at the end of the file.
- for (uint_fast64_t skippedRow = (uint_fast64_t) (lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) {
- ++result.numberOfNonzeroEntries;
- }
- }
-
return result;
}
diff --git a/src/storm/parser/DeterministicSparseTransitionParser.h b/src/storm/parser/DeterministicSparseTransitionParser.h
index 0515e120a..0d830d2f9 100644
--- a/src/storm/parser/DeterministicSparseTransitionParser.h
+++ b/src/storm/parser/DeterministicSparseTransitionParser.h
@@ -65,10 +65,9 @@ namespace storm {
* transitions and the maximum node id.
*
* @param buffer The buffer that contains the input.
- * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file.
* @return A structure representing the result of the first pass.
*/
- static FirstPassResult firstPass(char const* buffer, bool insertDiagonalEntriesIfMissing = true);
+ static FirstPassResult firstPass(char const* buffer);
/*
* The main parsing routine.