From b8f1ddd5da36f3932d4ef456d584e6b416366751 Mon Sep 17 00:00:00 2001 From: gereon Date: Sat, 12 Jan 2013 19:30:13 +0100 Subject: [PATCH] Implemented first run for NonDeterministicTransitionParser the first run checks the syntax and calculates * overall number of nondeterministic choices, i.e. number of rows * overall number of transitions, i.e. nonzero elements * maximum node id, i.e. number of columns --- ...NonDeterministicSparseTransitionParser.cpp | 128 +++++++++++------- .../NonDeterministicSparseTransitionParser.h | 2 +- 2 files changed, 81 insertions(+), 49 deletions(-) diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp index ad2654f98..cf3aee4b9 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.cpp +++ b/src/parser/NonDeterministicSparseTransitionParser.cpp @@ -6,9 +6,12 @@ */ #include "src/parser/NonDeterministicSparseTransitionParser.h" + +#include "src/utility/Settings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFileFormatException.h" #include "boost/integer/integer_mask.hpp" + #include #include #include @@ -25,34 +28,33 @@ extern log4cplus::Logger logger; namespace storm { -namespace parser{ +namespace parser { /*! - * @brief Perform first pass through the file and obtain number of - * non-zero cells and maximum node id. + * @brief Perform first pass through the file and obtain overall number of + * choices, number of non-zero cells and maximum node id. + * + * This method does the first pass through the transition file. * - * This method does the first pass through the .tra file and computes - * the number of non-zero elements that are not diagonal elements, - * which correspondents to the number of transitions that are not - * self-loops. - * (Diagonal elements are treated in a special way). - * It also calculates the maximum node id and stores it in maxnode. - * It also stores the maximum number of nondeterministic choices for a - * single single node in maxchoices. + * It computes the overall number of nondeterministic choices, i.e. the + * number of rows in the matrix that should be created. + * It also calculates the overall number of non-zero cells, i.e. the number + * of elements the matrix has to hold, and the maximum node id, i.e. the + * number of columns of the matrix. * - * @return The number of non-zero elements that are not on the diagonal * @param buf Data to scan. Is expected to be some char array. + * @param choices Overall number of choices. * @param maxnode Is set to highest id of all nodes. + * @return The number of non-zero elements. */ -std::unique_ptr> NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice) { - std::unique_ptr> non_zero = std::unique_ptr>(new std::vector()); - +uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode) { /* - * check file header and extract number of transitions + * Check file header and extract number of transitions. */ + buf = strchr(buf, '\n') + 1; // skip format hint if (strncmp(buf, "STATES ", 7) != 0) { LOG4CPLUS_ERROR(logger, "Expected \"STATES\" but got \"" << std::string(buf, 0, 16) << "\"."); - return nullptr; + return 0; } buf += 7; // skip "STATES " if (strtol(buf, &buf, 10) == 0) return 0; @@ -62,49 +64,79 @@ std::unique_ptr> NonDeterministicSparseTransitionPars return 0; } buf += 12; // skip "TRANSITIONS " - strtol(buf, &buf, 10); + /* + * Parse number of transitions. + * We will not actually use this value, but we will compare it to the + * number of transitions we count and issue a warning if this parsed + * vlaue is wrong. + */ + uint_fast64_t parsed_nonzero = strtol(buf, &buf, 10); /* - * check all transitions for non-zero diagonal entrys + * Read all transitions. */ - uint_fast64_t row, col, ndchoice; + uint_fast64_t source, target; + uint_fast64_t lastsource = 0; + uint_fast64_t nonzero = 0; double val; + choices = 0; maxnode = 0; - maxchoice = 0; while (buf[0] != '\0') { /* - * read row and column + * Read source node and choice. + * Check if current source node is larger than current maximum node id. + * Increase number of choices. + * Check if we have skipped any source node, i.e. if any node has no + * outgoing transitions. If so, increase nonzero (and + * parsed_nonzero). */ - row = checked_strtol(buf, &buf); - ndchoice = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - /* - * check if one is larger than the current maximum id - */ - if (row > maxnode) maxnode = row; - if (col > maxnode) maxnode = col; - /* - * check if nondeterministic choice is larger than current maximum - */ - if (ndchoice > maxchoice) - { - maxchoice = ndchoice; - while (non_zero->size() < maxchoice) non_zero->push_back(0); + source = checked_strtol(buf, &buf); + if (source > maxnode) maxnode = source; + choices++; + if (source > lastsource + 1) { + nonzero += source - lastsource - 1; + parsed_nonzero += source - lastsource - 1; } + buf += strcspn(buf, " \t\n\r"); // Skip name of choice. + /* - * read value. - * if row == col, we have a diagonal element which is treated separately and this non_zero must be decreased. + * Read all targets for this choice. */ - val = checked_strtod(buf, &buf); - if ((val < 0.0) || (val > 1.0)) { - LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\"."); - return 0; - } - if (row != col) (*non_zero)[ndchoice-1]++; buf = trimWhitespaces(buf); + while (buf[0] == '*') { + buf++; + /* + * Read target node and transition value. + * Check if current target node is larger than current maximum node id. + * Check if the transition value is a valid probability. + */ + target = checked_strtol(buf, &buf); + if (target > maxnode) maxnode = target; + val = checked_strtod(buf, &buf); + if ((val < 0.0) || (val > 1.0)) { + LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\"."); + return 0; + } + + /* + * Increase number of non-zero values. + */ + nonzero++; + + /* + * Proceed to beginning of next line. + */ + buf = trimWhitespaces(buf); + } } - return non_zero; + /* + * Check if the number of transitions given in the file is correct. + */ + if (nonzero != parsed_nonzero) { + LOG4CPLUS_WARN(logger, "File states to have " << parsed_nonzero << " transitions, but I counted " << nonzero << ". Maybe want to fix your file?"); + } + return nonzero; } @@ -135,12 +167,12 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s * perform first pass, i.e. count entries that are not zero and not on the diagonal */ uint_fast64_t maxnode, maxchoices; - std::unique_ptr> non_zero = this->firstPass(file.data, maxnode, maxchoices); + uint_fast64_t non_zero = this->firstPass(file.data, maxnode, maxchoices); /* * if first pass returned zero, the file format was wrong */ - if (non_zero == nullptr) + if (non_zero == 0) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); throw storm::exceptions::WrongFileFormatException(); diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h index bd46b2593..004885a42 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.h +++ b/src/parser/NonDeterministicSparseTransitionParser.h @@ -27,7 +27,7 @@ class NonDeterministicSparseTransitionParser : public Parser { private: std::shared_ptr> matrix; - std::unique_ptr> firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice); + uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode); };