sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

refactoring of DetSparseTrans Parser to support parameters in future 

Former-commit-id: cf451cdf61
tempestpy_adaptions
sjunges 11 years ago
parent
32ad2ae1a0
commit
0afb73bba1
4 changed files with 143 additions and 80 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 172
      src/parser/DeterministicSparseTransitionParser.cpp
  2. 25
      src/parser/DeterministicSparseTransitionParser.h
  3. 24
      src/parser/ReadValues.h
  4. 2
      src/storage/SparseMatrix.cpp

172
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -21,6 +21,8 @@
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
#include "src/settings/Settings.h" #include "src/settings/Settings.h"
#include "ReadValues.h"
#include "log4cplus/logger.h" #include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h" #include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger; extern log4cplus::Logger logger;
@ -32,9 +34,9 @@ namespace storm {
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename) { 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); return DeterministicSparseTransitionParser::parse(filename, false, emptyMatrix);
} }
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & transitionMatrix) { 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); 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 '.'. // Enforce locale where decimal point is '.'.
setlocale(LC_NUMERIC, "C"); setlocale(LC_NUMERIC, "C");
@ -67,15 +70,7 @@ namespace storm {
throw storm::exceptions::WrongFormatException(); 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) { if(isRewardFile) {
// The reward matrix should match the size of the transition matrix. // The reward matrix should match the size of the transition matrix.
if (firstPass.highestStateIndex + 1 > transitionMatrix.getRowCount() || firstPass.highestStateIndex + 1 > transitionMatrix.getColumnCount()) { if (firstPass.highestStateIndex + 1 > transitionMatrix.getRowCount() || firstPass.highestStateIndex + 1 > transitionMatrix.getColumnCount()) {
@ -86,13 +81,18 @@ namespace storm {
firstPass.highestStateIndex = transitionMatrix.getRowCount() - 1; firstPass.highestStateIndex = transitionMatrix.getRowCount() - 1;
} }
} }
// Perform second pass.
// Skip the format hint if it is there.
buf = skipFormatHint(buf);
// Creating matrix builder here. // Creating matrix builder here.
// The actual matrix will be build once all contents are inserted. // The actual matrix will be build once all contents are inserted.
storm::storage::SparseMatrixBuilder<double> resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries); 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 fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks");
bool hadDeadlocks = false; bool hadDeadlocks = false;
bool rowHadDiagonalEntry = false; bool rowHadDiagonalEntry = false;
@ -105,84 +105,75 @@ namespace storm {
// Different parsing routines for transition systems and transition rewards. // Different parsing routines for transition systems and transition rewards.
if(isRewardFile) { if(isRewardFile) {
while (buf[0] != '\0') { while (buf[0] != '\0') {
// Read next transition. // 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 { } else {
while (buf[0] != '\0') { while (buf[0] != '\0') {
// Read next transition. // 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. // Test if we moved to a new row.
// Handle all incomplete or skipped rows. // 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 (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) { 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)"); LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
} else { } else {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); 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. // 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. // 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)) { if(isRewardFile && !result.isSubmatrixOf(transitionMatrix)) {
@ -198,11 +189,7 @@ namespace storm {
DeterministicSparseTransitionParser::FirstPassResult result; DeterministicSparseTransitionParser::FirstPassResult result;
// Skip the format hint if it is there. // 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. // Check all transitions for non-zero diagonal entries and deadlock states.
uint_fast64_t row, col, lastRow = 0, lastCol = -1; uint_fast64_t row, col, lastRow = 0, lastCol = -1;
@ -213,7 +200,8 @@ namespace storm {
row = checked_strtol(buf, &buf); row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf);
// The actual read value is not needed here. // 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. // Compensate for missing diagonal entries if desired.
if (insertDiagonalEntriesIfMissing) { if (insertDiagonalEntriesIfMissing) {
@ -254,7 +242,7 @@ namespace storm {
lastRow = row; lastRow = row;
lastCol = col; lastCol = col;
buf = trimWhitespaces(buf);
} }
if(insertDiagonalEntriesIfMissing) { if(insertDiagonalEntriesIfMissing) {
@ -270,6 +258,36 @@ namespace storm {
return result; 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 parser
} // namespace storm } // namespace storm

25
src/parser/DeterministicSparseTransitionParser.h
View File

@ -5,7 +5,8 @@
namespace storm { namespace storm {
namespace parser { namespace parser {
/*! /*!
* This class can be used to parse a file containing either transitions or transition rewards of a deterministic model. * 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 { class DeterministicSparseTransitionParser {
public: 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. * 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. * The dimensions (rows and columns) of the two matrices should match.
* @return A SparseMatrix containing the parsed file contents. * @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 parser
} // namespace storm } // namespace storm

24
src/parser/ReadValues.h
View File

@ -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

2
src/storage/SparseMatrix.cpp
View File

@ -85,7 +85,7 @@ namespace storm {
// Finally, set the element and increase the current size. // Finally, set the element and increase the current size.
if (storagePreallocated) { if (storagePreallocated) {
columnsAndValues[currentEntryCount] = std::make_pair(column, value);
columnsAndValues.at(currentEntryCount) = std::make_pair(column, value);
} else { } else {
columnsAndValues.emplace_back(column, value); columnsAndValues.emplace_back(column, value);
if (!columnCountSet) { if (!columnCountSet) {

Write Preview
Loading…
Cancel
Save