diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 4410254d7..03b94c78c 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -28,19 +28,18 @@ namespace storm { namespace parser { -/*! - * @brief Perform first pass through the file and obtain number of - * non-zero cells and maximum node id. - * - * This method does the first pass through the .tra file and computes - * the number of non-zero elements. - * It also calculates the maximum node id and stores it in maxnode. - * - * @return The number of non-zero elements - * @param buf Data to scan. Is expected to be some char array. - * @param maxnode Is set to highest id of all nodes. - */ +storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) { + + return DeterministicSparseTransitionParser::parse(filename, false, insertDiagonalEntriesIfMissing); +} + +storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) { + + return DeterministicSparseTransitionParser::parse(filename, true, false, rewardMatrixInformation); +} + DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing) { + DeterministicSparseTransitionParser::FirstPassResult result; // Skip the format hint if it is there. @@ -107,220 +106,156 @@ DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransiti return result; } -/*! - * Reads a .tra file and produces a sparse matrix representing the described Markov Chain. - * - * Matrices created with this method have to be freed with the delete operator. - * @param filename input .tra file's name. - * @return a pointer to the created sparse matrix. - */ - -storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) { - +storm::storage::SparseMatrix DeterministicSparseTransitionParser::parse(std::string const& filename, bool rewardFile, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct const& rewardMatrixInformation) { // Enforce locale where decimal point is '.'. - setlocale(LC_NUMERIC, "C"); - - if (!fileExistsAndIsReadable(filename.c_str())) { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; - } + setlocale(LC_NUMERIC, "C"); - // Find out about the used line endings. - SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); - - // Open file. - MappedFile file(filename.c_str()); - char* buf = file.data; - - // Perform first pass, i.e. count entries that are not zero. - - DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing); - - LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); - - // If first pass returned zero, the file format was wrong. - if (firstPass.numberOfNonzeroEntries == 0) { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format."); - throw storm::exceptions::WrongFormatException(); - } - - // Perform second pass. - - // Skip the format hint if it is there. - buf = trimWhitespaces(buf); - if(buf[0] != '0') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); - } + if (!fileExistsAndIsReadable(filename.c_str())) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); + throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; + } - // Creating matrix builder here. - // The number of non-zero elements is computed by firstPass(). - // The contents are inserted during the readout of the file, below. - // The actual matrix will be build once all contents are inserted. - storm::storage::SparseMatrixBuilder resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries); + // Find out about the used line endings. + SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); - uint_fast64_t row, col, lastRow = 0; - double val; - bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); - bool hadDeadlocks = false; - bool rowHadDiagonalEntry = false; + // Open file. + MappedFile file(filename.c_str()); + char* buf = file.data; + // Perform first pass, i.e. count entries that are not zero. - // Read all transitions from file. Note that we assume that the - // transitions are listed in canonical order, otherwise this will not - // work, i.e. the values in the matrix will be at wrong places. - while (buf[0] != '\0') { + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing); - // Read next transition. - row = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - val = checked_strtod(buf, &buf); + LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); - // Read probability of this transition. - // Check, if the value is a probability, i.e. if it is between 0 and 1. - if ((val < 0.0) || (val > 1.0)) { - LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); + // If first pass returned zero, the file format was wrong. + if (firstPass.numberOfNonzeroEntries == 0) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format."); throw storm::exceptions::WrongFormatException(); } - // Test if we moved to a new row. - // Handle all incomplete or skipped rows. - if (lastRow != row) { - if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); - 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()); - 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; - } + // Perform second pass. - if (col == row) { - rowHadDiagonalEntry = true; + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] != '0') { + buf = storm::parser::forwardToNextLine(buf, lineEndings); } - if (col > row && !rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(row, row, storm::utility::constantZero()); - LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); + if(rewardFile) { + // The reward matrix should match the size of the transition matrix. + if (firstPass.highestStateIndex + 1 > rewardMatrixInformation.rowCount || firstPass.highestStateIndex + 1 > rewardMatrixInformation.columnCount) { + LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix."); + throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix."; } else { - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself."); + // If we found the right number of states or less, we set it to the number of states represented by the transition matrix. + firstPass.highestStateIndex = rewardMatrixInformation.rowCount - 1; } - rowHadDiagonalEntry = true; } - resultMatrix.addNextValue(row, col, val); - buf = trimWhitespaces(buf); - } - - if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); - LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); - } else { - 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."; - - return resultMatrix.build(); -} - -/*! - * Reads a .tra file and produces a sparse matrix representing the described Markov Chain. - * - * Matrices created with this method have to be freed with the delete operator. - * @param filename input .tra file's name. - * @return a pointer to the created sparse matrix. - */ - -storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) { - // Enforce locale where decimal point is '.'. - setlocale(LC_NUMERIC, "C"); - - if (!fileExistsAndIsReadable(filename.c_str())) { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); - throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; - } + // Creating matrix builder here. + // The actual matrix will be build once all contents are inserted. + storm::storage::SparseMatrixBuilder resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries); - // Find out about the used line endings. - SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + uint_fast64_t row, col, lastRow = 0; + double val; + bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); + bool hadDeadlocks = false; + bool rowHadDiagonalEntry = false; - // Open file. - MappedFile file(filename.c_str()); - char* buf = file.data; - // Perform first pass, i.e. count entries that are not zero. + // Read all transitions from file. Note that we assume that the + // transitions are listed in canonical order, otherwise this will not + // work, i.e. the values in the matrix will be at wrong places. - DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, false); + // Different parsing routines for transition systems and transition rewards. + if(rewardFile) { + while (buf[0] != '\0') { - LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); - - // If first pass returned zero, the file format was wrong. - if (firstPass.numberOfNonzeroEntries == 0) { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format."); - throw storm::exceptions::WrongFormatException(); - } - - // Perform second pass. - - // Skip the format hint if it is there. - buf = trimWhitespaces(buf); - if(buf[0] != '0') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); - } + // Read next transition. + row = checked_strtol(buf, &buf); + col = checked_strtol(buf, &buf); + val = checked_strtod(buf, &buf); - // The reward matrix should match the size of the transition matrix. - if (firstPass.highestStateIndex + 1 > rewardMatrixInformation.rowCount || firstPass.highestStateIndex + 1 > rewardMatrixInformation.columnCount) { - LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix."); - throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix."; - } else { - // If we found the right number of states or less, we set it to the number of states represented by the transition matrix. - firstPass.highestStateIndex = rewardMatrixInformation.rowCount - 1; - } + resultMatrix.addNextValue(row, col, val); + buf = trimWhitespaces(buf); + } + } else { + while (buf[0] != '\0') { + + // Read next transition. + row = checked_strtol(buf, &buf); + col = checked_strtol(buf, &buf); + val = checked_strtod(buf, &buf); + + // Read probability of this transition. + // Check, if the value is a probability, i.e. if it is between 0 and 1. + if ((val < 0.0) || (val > 1.0)) { + LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); + throw storm::exceptions::WrongFormatException(); + } + // Test if we moved to a new row. + // Handle all incomplete or skipped rows. + if (lastRow != row) { + if (!rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + 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()); + 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; + } - // Creating matrix builder here. - // The number of non-zero elements is computed by firstPass(). - // The contents are inserted during the readout of the file, below. - // The actual matrix will be build once all contents are inserted. - storm::storage::SparseMatrixBuilder resultMatrix(firstPass.highestStateIndex + 1, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries); + if (col == row) { + rowHadDiagonalEntry = true; + } - uint_fast64_t row, col; - double val; + if (col > row && !rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { + resultMatrix.addNextValue(row, row, storm::utility::constantZero()); + 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; + } - // Read all transitions from file. Note that we assume that the - // transitions are listed in canonical order, otherwise this will not - // work, i.e. the values in the matrix will be at wrong places. - while (buf[0] != '\0') { + resultMatrix.addNextValue(row, col, val); + buf = trimWhitespaces(buf); + } - // Read next transition. - row = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - val = checked_strtod(buf, &buf); + if (!rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { + resultMatrix.addNextValue(lastRow, lastRow, storm::utility::constantZero()); + LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); + } else { + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); + } + } - resultMatrix.addNextValue(row, col, val); - buf = trimWhitespaces(buf); - } + // 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."; + } - return resultMatrix.build(); + // Finally, build the actual matrix and return it. + return resultMatrix.build(); } } // namespace parser diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index c44583b97..45ce9ac26 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -27,21 +27,35 @@ public: }; /*! - * @brief Load a deterministic transition system from file and create a - * sparse adjacency matrix whose entries represent the weights of the edges + * Load a deterministic transition system from file and create a + * sparse adjacency matrix whose entries represent the weights of the edges. + * + * @param filename The path of file to be parsed. + * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. + * @return A SparseMatrix containing the parsed transition system. */ static storm::storage::SparseMatrix parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing = true); /*! - * @brief Load the transition rewards for a deterministic transition system from file and create a - * sparse adjacency matrix whose entries represent the rewards of the respective transitions. + * Load the transition rewards for a deterministic transition system from file and create a + * sparse adjacency matrix whose entries represent the rewards of the respective transitions. + */ + + /*! + * Load the transition rewards for a deterministic transition system from file and create a + * sparse adjacency matrix whose entries represent the rewards of the respective transitions. + * + * @param filename The path of file to be parsed. + * @param rewardMatrixInformation A struct containing information that is used to check if the transition reward matrix fits to the rest of the model. + * @return A SparseMatrix containing the parsed transition rewards. */ static storm::storage::SparseMatrix parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation); private: /* - * Performs the first pass on the input pointed to by the given buffer. + * Performs the first pass on the input pointed to by the given buffer to obtain the number of + * transitions and the maximum node id. * * @param buffer The buffer that cointains the input. * @param lineEndings The line endings that are to be used while parsing. @@ -50,6 +64,18 @@ private: */ static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing = true); + /* + * The main parsing routine. + * Opens the given file, calls the first pass and performs the second pass, parsing the content of the file into a SparseMatrix. + * + * @param filename The path of file to be parsed. + * @param rewardFile A flag set iff the file to be parsed contains transition rewards. + * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. + * @param rewardMatrixInformation A struct containing information that is used to check if the transition reward matrix fits to the rest of the model. + * @return A SparseMatrix containing the parsed file contents. + */ + static storm::storage::SparseMatrix parse(std::string const& filename, bool rewardFile, bool insertDiagonalEntriesIfMissing = false, RewardMatrixInformationStruct const& rewardMatrixInformation = nullptr); + }; } // namespace parser diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index 4003b6a5a..cf98ded11 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -18,16 +18,19 @@ storm::models::MarkovAutomaton MarkovAutomatonParser::parseMarkovAutomat // Parse the state labeling. storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser(transitionMatrix.getColumnCount(), labelingFilename)); + // If given, parse the state rewards file. boost::optional> stateRewards; if (stateRewardFilename != "") { stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename)); } + // Since Markov Automata do not support transition rewards no path should be given here. if (transitionRewardFilename != "") { LOG4CPLUS_ERROR(logger, "Transition rewards are unsupported for Markov automata."); throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata."; } + // Put the pieces together to generate the Markov Automaton. storm::models::MarkovAutomaton resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.nondeterministicChoiceIndices), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(stateRewards), boost::optional>(), boost::optional>>()); return resultingAutomaton; diff --git a/src/parser/MarkovAutomatonParser.h b/src/parser/MarkovAutomatonParser.h index 53354ba55..ae8005006 100644 --- a/src/parser/MarkovAutomatonParser.h +++ b/src/parser/MarkovAutomatonParser.h @@ -20,7 +20,7 @@ public: * @param transitionsFilename The name of the file containing the transitions of the Markov automaton. * @param labelingFilename The name of the file containing the labels for the states of the Markov automaton. * @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton. - * @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. + * @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. This should be empty as transition rewards are not supported by Markov Automata. */ static storm::models::MarkovAutomaton parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename); }; diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 54c6aae6a..ef89371e0 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -30,7 +30,7 @@ public: // The highest state index that appears in the model. uint_fast64_t highestStateIndex; - // The total number of choices in the model. + // The total number of nondeterministic choices in the model. uint_fast64_t numberOfChoices; };