diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index 67e31484f..47546c036 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -21,6 +21,8 @@
#include "src/exceptions/WrongFormatException.h"
#include "src/settings/Settings.h"
+#include "ReadValues.h"
+
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
@@ -32,9 +34,9 @@ namespace storm {
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename) {
- storm::storage::SparseMatrix<double> emptyMatrix;
-
+ storm::storage::SparseMatrix<double> emptyMatrix;
return DeterministicSparseTransitionParser::parse(filename, false, emptyMatrix);
+
}
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & transitionMatrix) {
@@ -42,7 +44,8 @@ namespace storm {
return DeterministicSparseTransitionParser::parse(filename, true, transitionMatrix);
}
- storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & transitionMatrix) {
+ template<typename T>
+ storm::storage::SparseMatrix<T> DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<T> const & transitionMatrix) {
// Enforce locale where decimal point is '.'.
setlocale(LC_NUMERIC, "C");
@@ -67,15 +70,7 @@ namespace storm {
throw storm::exceptions::WrongFormatException();
}
- // Perform second pass.
-
- // Skip the format hint if it is there.
- buf = trimWhitespaces(buf);
- if(buf[0] < '0' || buf[0] > '9') {
- buf = forwardToLineEnd(buf);
- buf = trimWhitespaces(buf);
- }
-
+
if(isRewardFile) {
// The reward matrix should match the size of the transition matrix.
if (firstPass.highestStateIndex + 1 > transitionMatrix.getRowCount() || firstPass.highestStateIndex + 1 > transitionMatrix.getColumnCount()) {
@@ -86,13 +81,18 @@ namespace storm {
firstPass.highestStateIndex = transitionMatrix.getRowCount() - 1;
}
}
+ // Perform second pass.
+
+ // Skip the format hint if it is there.
+ buf = skipFormatHint(buf);
+
// Creating matrix builder here.
// The actual matrix will be build once all contents are inserted.
storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries);
- uint_fast64_t row, col, lastRow = 0;
- double val;
+ uint_fast64_t lastRow = 0;
+ DeterministicTransitionEntry<double> trans;
bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
bool hadDeadlocks = false;
bool rowHadDiagonalEntry = false;
@@ -105,84 +105,75 @@ namespace storm {
// Different parsing routines for transition systems and transition rewards.
if(isRewardFile) {
while (buf[0] != '\0') {
-
// Read next transition.
- row = checked_strtol(buf, &buf);
- col = checked_strtol(buf, &buf);
- val = checked_strtod(buf, &buf);
-
- resultMatrix.addNextValue(row, col, val);
- buf = trimWhitespaces(buf);
+ readNextTransition(&buf, &trans);
+ addTransitionToMatrix(trans, &resultMatrix);
}
} else {
while (buf[0] != '\0') {
// Read next transition.
- row = checked_strtol(buf, &buf);
- col = checked_strtol(buf, &buf);
- val = checked_strtod(buf, &buf);
+ readNextTransition(&buf, &trans);
// 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::constantZero<double>());
- LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
- } else {
- LOG4CPLUS_WARN(logger, "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 (fixDeadlocks) {
- resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<double>());
- rowHadDiagonalEntry = true;
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
- } else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
- // Before throwing the appropriate exception we will give notice of all deadlock states.
- }
- }
- lastRow = row;
- rowHadDiagonalEntry = false;
- }
-
- if (col == row) {
- rowHadDiagonalEntry = true;
- }
-
- if (col > row && !rowHadDiagonalEntry) {
- if (insertDiagonalEntriesIfMissing) {
- resultMatrix.addNextValue(row, row, storm::utility::constantZero<double>());
- LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
- } else {
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
- }
- rowHadDiagonalEntry = true;
- }
-
- resultMatrix.addNextValue(row, col, val);
- buf = trimWhitespaces(buf);
+ if (lastRow != trans.row) {
+ if (!rowHadDiagonalEntry) {
+ if (insertDiagonalEntriesIfMissing) {
+ resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<T>());
+ LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
+ } else {
+ LOG4CPLUS_WARN(logger, "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 < trans.row; ++skippedRow) {
+ hadDeadlocks = true;
+ if (fixDeadlocks) {
+ resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne<T>());
+ rowHadDiagonalEntry = true;
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
+ } else {
+ LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
+ // Before throwing the appropriate exception we will give notice of all deadlock states.
+ }
+ }
+ lastRow = trans.row;
+ rowHadDiagonalEntry = false;
+ }
+
+ if (trans.col == trans.row) {
+ rowHadDiagonalEntry = true;
+ }
+
+ if (trans.col > trans.row && !rowHadDiagonalEntry) {
+ if (insertDiagonalEntriesIfMissing) {
+ resultMatrix.addNextValue(trans.row, trans.row, storm::utility::constantZero<T>());
+ LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << trans.row << " has no transition to itself. Inserted a 0-transition. (2)");
+ } else {
+ LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << trans.row << " has no transition to itself.");
+ }
+ rowHadDiagonalEntry = true;
+ }
+ addTransitionToMatrix(trans, &resultMatrix);
}
if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
- resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<double>());
+ resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero<T>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
} else {
LOG4CPLUS_WARN(logger, "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 (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
+ // If we encountered deadlock and did not fix them, now is the time to throw the exception.
+ if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the nodes had deadlocks. You can use --fixDeadlocks to insert self-loops on the fly.";
}
// Finally, build the actual matrix, test and return it.
- storm::storage::SparseMatrix<double> result = resultMatrix.build();
+ storm::storage::SparseMatrix<T> result = resultMatrix.build();
// Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
if(isRewardFile && !result.isSubmatrixOf(transitionMatrix)) {
@@ -198,11 +189,7 @@ namespace storm {
DeterministicSparseTransitionParser::FirstPassResult result;
// Skip the format hint if it is there.
- buf = trimWhitespaces(buf);
- if(buf[0] < '0' || buf[0] > '9') {
- buf = forwardToLineEnd(buf);
- buf = trimWhitespaces(buf);
- }
+ buf = skipFormatHint(buf);
// Check all transitions for non-zero diagonal entries and deadlock states.
uint_fast64_t row, col, lastRow = 0, lastCol = -1;
@@ -213,7 +200,8 @@ namespace storm {
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
// The actual read value is not needed here.
- checked_strtod(buf, &buf);
+ buf = forwardToLineEnd(buf);
+ buf = trimWhitespaces(buf);
// Compensate for missing diagonal entries if desired.
if (insertDiagonalEntriesIfMissing) {
@@ -254,7 +242,7 @@ namespace storm {
lastRow = row;
lastCol = col;
- buf = trimWhitespaces(buf);
+
}
if(insertDiagonalEntriesIfMissing) {
@@ -270,6 +258,36 @@ namespace storm {
return result;
}
+
+ template<typename T>
+ void DeterministicSparseTransitionParser::readNextTransition(char** buf, DeterministicTransitionEntry<T>* trans)
+ {
+ trans->row = checked_strtol(*buf, buf);
+ trans->col = checked_strtol(*buf, buf);
+ trans->val = checked_strtod(*buf, buf);
+
+ *buf = trimWhitespaces(*buf);
+ }
+
+
+
+ template<typename T>
+ void DeterministicSparseTransitionParser::addTransitionToMatrix(DeterministicTransitionEntry<T> const& trans, storm::storage::SparseMatrixBuilder<T>* mat)
+ {
+ mat->addNextValue(trans.row, trans.col, trans.val);
+ }
+
+ char* DeterministicSparseTransitionParser::skipFormatHint(char* buf)
+ {
+ // Skip the format hint if it is there.
+ buf = trimWhitespaces(buf);
+ if(buf[0] < '0' || buf[0] > '9') {
+ buf = forwardToLineEnd(buf);
+ buf = trimWhitespaces(buf);
+ }
+ return buf;
+ }
+
} // namespace parser
} // namespace storm
diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h
index e31ef2291..cddf1420c 100644
--- a/src/parser/DeterministicSparseTransitionParser.h
+++ b/src/parser/DeterministicSparseTransitionParser.h
@@ -5,7 +5,8 @@
namespace storm {
namespace parser {
-
+
+
/*!
* This class can be used to parse a file containing either transitions or transition rewards of a deterministic model.
*
@@ -16,6 +17,13 @@ namespace storm {
class DeterministicSparseTransitionParser {
public:
+ template<typename T>
+ struct DeterministicTransitionEntry
+ {
+ uint_fast64_t row = 0;
+ uint_fast64_t col = 0;
+ T val;
+ };
/*!
* A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model and the highest state index.
*/
@@ -80,9 +88,22 @@ namespace storm {
* The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed file contents.
*/
- static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & transitionMatrix);
+ template<typename T>
+ static storm::storage::SparseMatrix<T> parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<T> const & transitionMatrix);
+ // Helper methods.
+ /*
+ */
+ template<typename T>
+ static void readNextTransition(char** buf, DeterministicTransitionEntry<T>* trans );
+
+
+ template<typename T>
+ static void addTransitionToMatrix(DeterministicTransitionEntry<T> const& trans, storm::storage::SparseMatrixBuilder<T>* mat);
+
+ static char* skipFormatHint(char*);
};
+
} // namespace parser
} // namespace storm
diff --git a/src/parser/ReadValues.h b/src/parser/ReadValues.h
new file mode 100644
index 000000000..dad3b42b2
--- /dev/null
+++ b/src/parser/ReadValues.h
@@ -0,0 +1,24 @@
+#ifndef _STORM_PARSER_READVALUES_H
+#define _STORM_PARSER_READVALUES_H
+
+#include "src/utility/cstring.h"
+
+namespace storm
+{
+ namespace parser
+ {
+
+ template<typename T>
+ T readValue(char* buf);
+
+ template<>
+ double readValue<double>(char* buf)
+ {
+ return utility::cstring::checked_strtod(buf, &buf);
+ }
+
+ }
+}
+
+#endif
+
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 21814b643..28fa2dc5b 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -85,7 +85,7 @@ namespace storm {
// Finally, set the element and increase the current size.
if (storagePreallocated) {
- columnsAndValues[currentEntryCount] = std::make_pair(column, value);
+ columnsAndValues.at(currentEntryCount) = std::make_pair(column, value);
} else {
columnsAndValues.emplace_back(column, value);
if (!columnCountSet) {