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

Modified parsers such that the reward matrices are of the same size as the transition matrices.

main
dehnert 12 years ago
parent
abae304719
commit
c7f58ed5f5
7 changed files with 92 additions and 40 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/parser/DeterministicModelParser.cpp
  2. 47
      src/parser/DeterministicSparseTransitionParser.cpp
  3. 4
      src/parser/DeterministicSparseTransitionParser.h
  4. 4
      src/parser/NondeterministicModelParser.cpp
  5. 52
      src/parser/NondeterministicSparseTransitionParser.cpp
  6. 4
      src/parser/NondeterministicSparseTransitionParser.h
  7. 17
      src/parser/Parser.h

4
src/parser/DeterministicModelParser.cpp
View File

@ -45,7 +45,9 @@ DeterministicModelParser::DeterministicModelParser(std::string const & transitio
this->stateRewards = srp.getStateRewards();
}
if (transitionRewardFile != "") {
storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, true);
RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(stateCount, stateCount, nullptr);
storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, rewardMatrixInfo);
delete rewardMatrixInfo;
this->transitionRewards = trp.getMatrix();
}
this->dtmc = nullptr;

47
src/parser/DeterministicSparseTransitionParser.cpp
View File

@ -44,12 +44,14 @@ namespace parser {
* @param buf Data to scan. Is expected to be some char array.
* @param maxnode Is set to highest id of all nodes.
*/
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, bool rewardFile) {
uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
bool isRewardMatrix = rewardMatrixInformation != nullptr;
uint_fast64_t nonZeroEntryCount = 0;
/*
* Check file header and extract number of transitions.
*/
if (!rewardFile) {
if (!isRewardMatrix) {
buf = strchr(buf, '\n') + 1; // skip format hint
}
@ -68,7 +70,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
row = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
if (!rewardFile) {
if (!isRewardMatrix) {
if (lastRow != row) {
if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
++nonZeroEntryCount;
@ -109,7 +111,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
buf = trimWhitespaces(buf);
}
if (!rowHadDiagonalEntry && !rewardFile) {
if (!rowHadDiagonalEntry && !isRewardMatrix) {
++nonZeroEntryCount;
}
@ -126,13 +128,15 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast
* @return a pointer to the created sparse matrix.
*/
DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, bool rewardFile)
DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation)
: matrix(nullptr) {
/*
* Enforce locale where decimal point is '.'.
*/
setlocale(LC_NUMERIC, "C");
bool isRewardMatrix = rewardMatrixInformation != nullptr;
/*
* Open file.
*/
@ -143,7 +147,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
* Perform first pass, i.e. count entries that are not zero.
*/
int_fast64_t maxStateId;
uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardFile);
uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardMatrixInformation);
LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros.");
@ -164,10 +168,21 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
/*
* Read file header, extract number of states.
*/
if (!rewardFile) {
if (!isRewardMatrix) {
buf = strchr(buf, '\n') + 1; // skip format hint
}
// If the matrix that is being parsed is a reward matrix, it should match the size of the
// transition matrix.
if (isRewardMatrix) {
if (maxStateId + 1 > rewardMatrixInformation->rowCount || maxStateId + 1 > rewardMatrixInformation->columnCount) {
LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix.");
throw storm::exceptions::WrongFileFormatException() << "Reward matrix has more rows or columns than transition matrix.";
} else {
maxStateId = rewardMatrixInformation->rowCount - 1;
}
}
/*
* Creating matrix here.
* The number of non-zero elements is computed by firstPass().
@ -201,10 +216,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
if (lastRow != row) {
if ((lastRow != -1) && (!rowHadDiagonalEntry)) {
if (insertDiagonalEntriesIfMissing) {
if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
} else if (!rewardFile) {
} else if (!isRewardMatrix) {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
}
// No increment for lastRow
@ -212,11 +227,11 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
}
for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) {
hadDeadlocks = true;
if (fixDeadlocks && !rewardFile) {
if (fixDeadlocks && !isRewardMatrix) {
this->matrix->addNextValue(skippedRow, skippedRow, storm::utility::constGetOne<double>());
rowHadDiagonalEntry = true;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else if (!rewardFile) {
} else if (!isRewardMatrix) {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// FIXME Why no exception at this point? This will break the App.
}
@ -229,10 +244,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
rowHadDiagonalEntry = true;
} else if (col > row && !rowHadDiagonalEntry) {
rowHadDiagonalEntry = true;
if (insertDiagonalEntriesIfMissing && !rewardFile) {
if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
this->matrix->addNextValue(row, row, storm::utility::constGetZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
} else if (!rewardFile) {
} else if (!isRewardMatrix) {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
}
}
@ -242,15 +257,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st
}
if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing && !rewardFile) {
if (insertDiagonalEntriesIfMissing && !isRewardMatrix) {
this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero<double>());
LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
} else if (!rewardFile) {
} else if (!isRewardMatrix) {
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
}
}
if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
if (!fixDeadlocks && hadDeadlocks && !isRewardMatrix) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
/*
* Finalize Matrix.

4
src/parser/DeterministicSparseTransitionParser.h
View File

@ -17,7 +17,7 @@ namespace parser {
*/
class DeterministicSparseTransitionParser : public Parser {
public:
DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, bool rewardFile = false);
DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() {
return this->matrix;
@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser {
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, bool rewardFile);
uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
};

4
src/parser/NondeterministicModelParser.cpp
View File

@ -38,7 +38,9 @@ NondeterministicModelParser::NondeterministicModelParser(std::string const & tra
this->stateRewards = srp.getStateRewards();
}
if (transitionRewardFile != "") {
storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, true, tp.getRowMapping());
RewardMatrixInformationStruct* rewardMatrixInfo = new RewardMatrixInformationStruct(tp.getMatrix()->getRowCount(), tp.getMatrix()->getColumnCount(), tp.getRowMapping());
storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, rewardMatrixInfo);
delete rewardMatrixInfo;
this->transitionRewardMatrix = trp.getMatrix();
}

52
src/parser/NondeterministicSparseTransitionParser.cpp
View File

@ -49,11 +49,13 @@ namespace parser {
* @param maxnode Is set to highest id of all nodes.
* @return The number of non-zero elements.
*/
uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices) {
uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) {
bool isRewardFile = rewardMatrixInformation != nullptr;
/*
* Check file header and extract number of transitions.
*/
if (!rewardFile) {
if (!isRewardFile) {
buf = strchr(buf, '\n') + 1; // skip format hint
}
@ -80,17 +82,17 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
maxnode = source;
}
if (rewardFile) {
if (isRewardFile) {
// If we have switched the source state, we possibly need to insert the rows of the last
// last source state.
if (source != lastsource && lastsource != -1) {
choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
}
// If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices.
for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
}
// If we advanced to the next state, but skipped some choices, we have to reserve rows
@ -151,14 +153,14 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
buf = trimWhitespaces(buf);
}
if (rewardFile) {
if (isRewardFile) {
// If not all rows were filled for the last state, we need to insert them.
choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
choices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
// If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices.
for (uint_fast64_t i = lastsource + 1; i < nondeterministicChoiceIndices->size() - 1; ++i) {
choices += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
for (uint_fast64_t i = lastsource + 1; i < rewardMatrixInformation->nondeterministicChoiceIndices->size() - 1; ++i) {
choices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
}
}
@ -175,13 +177,15 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_
* @return a pointer to the created sparse matrix.
*/
NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices)
NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation)
: matrix(nullptr) {
/*
* Enforce locale where decimal point is '.'.
*/
setlocale(LC_NUMERIC, "C");
bool isRewardFile = rewardMatrixInformation != nullptr;
/*
* Open file.
*/
@ -193,7 +197,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
*/
int_fast64_t maxnode;
uint_fast64_t choices;
uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardFile, nondeterministicChoiceIndices);
uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardMatrixInformation);
/*
* If first pass returned zero, the file format was wrong.
@ -212,10 +216,22 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
/*
* Skip file header.
*/
if (!rewardFile) {
if (!isRewardFile) {
buf = strchr(buf, '\n') + 1; // skip format hint
}
if (isRewardFile) {
if (choices > rewardMatrixInformation->rowCount || maxnode + 1 > rewardMatrixInformation->columnCount) {
LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size.");
throw storm::exceptions::WrongFileFormatException() << "Reward matrix size exceeds transition matrix size.";
} else if (choices != rewardMatrixInformation->rowCount) {
LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count.");
throw storm::exceptions::WrongFileFormatException() << "Reward matrix row count does not match transition matrix row count.";
} else {
maxnode = rewardMatrixInformation->columnCount - 1;
}
}
/*
* Create and initialize matrix.
* The matrix should have as many columns as we have nodes and as many rows as we have choices.
@ -253,17 +269,17 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
source = checked_strtol(buf, &buf);
choice = checked_strtol(buf, &buf);
if (rewardFile) {
if (isRewardFile) {
// If we have switched the source state, we possibly need to insert the rows of the last
// last source state.
if (source != lastsource && lastsource != -1) {
curRow += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*nondeterministicChoiceIndices)[lastsource] - 1);
curRow += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
}
// If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices.
for (uint_fast64_t i = lastsource + 1; i < source; ++i) {
curRow += ((*nondeterministicChoiceIndices)[i + 1] - (*nondeterministicChoiceIndices)[i]);
curRow += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
}
// If we advanced to the next state, but skipped some choices, we have to reserve rows
@ -286,12 +302,12 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
*/
for (int_fast64_t node = lastsource + 1; node < source; node++) {
hadDeadlocks = true;
if (!rewardFile && fixDeadlocks) {
if (fixDeadlocks) {
this->rowMapping->at(node) = curRow;
this->matrix->addNextValue(curRow, node, 1);
++curRow;
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
} else if (!rewardFile) {
} else {
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
}
}
@ -323,7 +339,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s
this->rowMapping->at(maxnode+1) = curRow + 1;
if (!fixDeadlocks && hadDeadlocks && !rewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
if (!fixDeadlocks && hadDeadlocks && !isRewardFile) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
/*
* Finalize matrix.

4
src/parser/NondeterministicSparseTransitionParser.h
View File

@ -19,7 +19,7 @@ namespace parser {
*/
class NondeterministicSparseTransitionParser : public Parser {
public:
NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile = false, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices = nullptr);
NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
return this->matrix;
@ -33,7 +33,7 @@ class NondeterministicSparseTransitionParser : public Parser {
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr<std::vector<uint_fast64_t>> const nondeterministicChoiceIndices);
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation);
};

17
src/parser/Parser.h
View File

@ -14,6 +14,8 @@
#include <fcntl.h>
#include <errno.h>
#include <iostream>
#include <memory>
#include <vector>
#include <boost/integer/integer_mask.hpp>
#include "src/exceptions/FileIoException.h"
@ -30,6 +32,21 @@ namespace storm {
*/
namespace parser {
struct RewardMatrixInformationStruct {
RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) {
// Intentionally left empty.
}
RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices)
: rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
// Intentionally left empty.
}
uint_fast64_t rowCount;
uint_fast64_t columnCount;
std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;
};
/*!
* @brief Opens a file and maps it to memory providing a char*
* containing the file content.

Write Preview
Loading…
Cancel
Save