diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 2372cde3e..2300ad74d 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -45,7 +45,7 @@ DeterministicModelParser::DeterministicModelParser(std::string const & transitio this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { - storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile); + storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile, false, true); this->transitionRewards = trp.getMatrix(); } this->dtmc = nullptr; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index a91c61525..031087b88 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) { +uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode, bool rewardFile) { uint_fast64_t nonZeroEntryCount = 0; /* * Check file header and extract number of transitions. */ - buf = strchr(buf, '\n') + 1; // skip format hint + if (!rewardFile) { + buf = strchr(buf, '\n') + 1; // skip format hint + } /* * Check all transitions for non-zero diagonal entries and deadlock states. @@ -66,24 +68,26 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast row = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf); - if (lastRow != row) { - if ((lastRow != -1) && (!rowHadDiagonalEntry)) { - ++nonZeroEntryCount; - rowHadDiagonalEntry = true; + if (!rewardFile) { + if (lastRow != row) { + if ((lastRow != -1) && (!rowHadDiagonalEntry)) { + ++nonZeroEntryCount; + rowHadDiagonalEntry = true; + } + for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { + ++nonZeroEntryCount; + } + lastRow = row; + rowHadDiagonalEntry = false; } - for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { + + if (col == row) { + rowHadDiagonalEntry = true; + } else if (col > row && !rowHadDiagonalEntry) { + rowHadDiagonalEntry = true; ++nonZeroEntryCount; } - lastRow = row; - rowHadDiagonalEntry = false; - } - - if (col == row) { - rowHadDiagonalEntry = true; - } else if (col > row && !rowHadDiagonalEntry) { - rowHadDiagonalEntry = true; - ++nonZeroEntryCount; - } + } /* * Check if one is larger than the current maximum id. @@ -105,7 +109,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast buf = trimWhitespaces(buf); } - if (!rowHadDiagonalEntry) { + if (!rowHadDiagonalEntry && !rewardFile) { ++nonZeroEntryCount; } @@ -122,7 +126,7 @@ 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) +DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, bool rewardFile) : matrix(nullptr) { /* * Enforce locale where decimal point is '.'. @@ -139,7 +143,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); + uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId, rewardFile); LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros."); @@ -160,7 +164,9 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st /* * Read file header, extract number of states. */ - buf = strchr(buf, '\n') + 1; // skip format hint + if (!rewardFile) { + buf = strchr(buf, '\n') + 1; // skip format hint + } /* * Creating matrix here. @@ -198,7 +204,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st if (insertDiagonalEntriesIfMissing) { 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 { + } else if (!rewardFile) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); } // No increment for lastRow @@ -206,11 +212,11 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } for (int_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; - if (fixDeadlocks) { + if (fixDeadlocks && !rewardFile) { 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 { + } else if (!rewardFile) { 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. } @@ -223,10 +229,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st rowHadDiagonalEntry = true; } else if (col > row && !rowHadDiagonalEntry) { rowHadDiagonalEntry = true; - if (insertDiagonalEntriesIfMissing) { + if (insertDiagonalEntriesIfMissing && !rewardFile) { 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 { + } else if (!rewardFile) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); } } @@ -236,10 +242,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { + if (insertDiagonalEntriesIfMissing && !rewardFile) { 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 { + } else if (!rewardFile) { LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); } } diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 2407f3398..a023debb7 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); + DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, bool rewardFile = false); 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); + uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode, bool rewardFile); }; diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index e1f677239..303789a99 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -38,7 +38,7 @@ NondeterministicModelParser::NondeterministicModelParser(std::string const & tra this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { - storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile); + storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile, true, tp.getRowMapping()); this->transitionRewardMatrix = trp.getMatrix(); } diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 97acfa1b3..1019240c7 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) { +uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr> const nondeterministicChoiceIndices) { /* * Check file header and extract number of transitions. */ - buf = strchr(buf, '\n') + 1; // skip format hint + if (!rewardFile) { + buf = strchr(buf, '\n') + 1; // skip format hint + } /* * Read all transitions. @@ -78,15 +80,37 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ maxnode = source; } - // If we have skipped some states, we need to reserve the space for the self-loop insertion - // in the second pass. - if (source > lastsource + 1) { - nonzero += source - lastsource - 1; - choices += source - lastsource - 1; - } else if (source != lastsource || choice != lastchoice) { - // If we have switched the source state or the nondeterministic choice, we need to - // reserve one row more. - ++choices; + if (rewardFile) { + // 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); + } + + // 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]); + } + + // If we advanced to the next state, but skipped some choices, we have to reserve rows + // for them + if (source != lastsource) { + choices += choice + 1; + } else if (choice != lastchoice) { + choices += choice - lastchoice; + } + } else { + // If we have skipped some states, we need to reserve the space for the self-loop insertion + // in the second pass. + if (source > lastsource + 1) { + nonzero += source - lastsource - 1; + choices += source - lastsource - 1; + } else if (source != lastsource || choice != lastchoice) { + // If we have switched the source state or the nondeterministic choice, we need to + // reserve one row more. + ++choices; + } } // Read target and check if we encountered a state index that is bigger than all previously @@ -127,6 +151,17 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ buf = trimWhitespaces(buf); } + if (rewardFile) { + // If not all rows were filled for the last state, we need to insert them. + choices += lastchoice - ((*nondeterministicChoiceIndices)[lastsource + 1] - (*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]); + } + } + return nonzero; } @@ -140,7 +175,7 @@ uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_ * @return a pointer to the created sparse matrix. */ -NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename) +NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile, std::shared_ptr> const nondeterministicChoiceIndices) : matrix(nullptr) { /* * Enforce locale where decimal point is '.'. @@ -158,7 +193,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s */ int_fast64_t maxnode; uint_fast64_t choices; - uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode); + uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode, rewardFile, nondeterministicChoiceIndices); /* * If first pass returned zero, the file format was wrong. @@ -177,7 +212,9 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s /* * Skip file header. */ - buf = strchr(buf, '\n') + 1; // skip format hint + if (!rewardFile) { + buf = strchr(buf, '\n') + 1; // skip format hint + } /* * Create and initialize matrix. @@ -216,33 +253,54 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s source = checked_strtol(buf, &buf); choice = checked_strtol(buf, &buf); - // Increase line count if we have either finished reading the transitions of a certain state - // or we have finished reading one nondeterministic choice of a state. - if ((source != lastsource || choice != lastchoice)) { - ++curRow; - } + if (rewardFile) { + // 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); + } - /* - * Check if we have skipped any source node, i.e. if any node has no - * outgoing transitions. If so, insert a self-loop. - * Also add self-loops to rowMapping. - */ - for (int_fast64_t node = lastsource + 1; node < source; node++) { - hadDeadlocks = true; - if (fixDeadlocks) { - this->rowMapping->at(node) = curRow; - this->matrix->addNextValue(curRow, node, 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]); + } + + // If we advanced to the next state, but skipped some choices, we have to reserve rows + // for them + if (source != lastsource) { + curRow += choice + 1; + } else if (choice != lastchoice) { + curRow += choice - lastchoice; + } + } else { + // Increase line count if we have either finished reading the transitions of a certain state + // or we have finished reading one nondeterministic choice of a state. + if ((source != lastsource || choice != lastchoice)) { ++curRow; - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); - } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); } - } - if (source != lastsource) { /* - * Add this source to rowMapping, if this is the first choice we encounter for this state. + * Check if we have skipped any source node, i.e. if any node has no + * outgoing transitions. If so, insert a self-loop. + * Also add self-loops to rowMapping. */ - this->rowMapping->at(source) = curRow; + for (int_fast64_t node = lastsource + 1; node < source; node++) { + hadDeadlocks = true; + if (!rewardFile && 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) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); + } + } + if (source != lastsource) { + /* + * Add this source to rowMapping, if this is the first choice we encounter for this state. + */ + this->rowMapping->at(source) = curRow; + } } // Read target and value and write it to the matrix. @@ -265,7 +323,7 @@ NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(s this->rowMapping->at(maxnode+1) = curRow + 1; - 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 && !rewardFile) 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 209c0e7a0..79947dd93 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); + NondeterministicSparseTransitionParser(std::string const &filename, bool rewardFile = false, std::shared_ptr> const nondeterministicChoiceIndices = 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); + uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, bool rewardFile, std::shared_ptr> const nondeterministicChoiceIndices); };