diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 2300ad74d..35818ffbf 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -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; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 031087b88..60957a17a 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -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()); 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()); 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()); 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()); 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. diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index a023debb7..cb91901f8 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -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> getMatrix() { return this->matrix; @@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser { private: std::shared_ptr> 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); }; diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 303789a99..a0ce35674 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -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(); } diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 1019240c7..79bb9f3f5 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -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> 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> 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. diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index 79947dd93..5731017ec 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -19,7 +19,7 @@ namespace parser { */ class NondeterministicSparseTransitionParser : public Parser { public: - NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile = false, std::shared_ptr> const nondeterministicChoiceIndices = nullptr); + NondeterministicSparseTransitionParser(std::string const &filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); inline std::shared_ptr> getMatrix() const { return this->matrix; @@ -33,7 +33,7 @@ class NondeterministicSparseTransitionParser : public Parser { std::shared_ptr> matrix; std::shared_ptr> rowMapping; - uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr> const nondeterministicChoiceIndices); + uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation); }; diff --git a/src/parser/Parser.h b/src/parser/Parser.h index ef6c38c84..6cb4abe65 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -14,6 +14,8 @@ #include #include #include +#include +#include #include #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> nondeterministicChoiceIndices) + : rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) { + // Intentionally left empty. + } + + uint_fast64_t rowCount; + uint_fast64_t columnCount; + std::shared_ptr> nondeterministicChoiceIndices; + }; + /*! * @brief Opens a file and maps it to memory providing a char* * containing the file content.