diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index c0a058381..aaca0d7a3 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -6,12 +6,13 @@ */ #include "src/parser/AtomicPropositionLabelingParser.h" -#include "src/parser/Parser.h" #include #include #include +#include "src/parser/Parser.h" +#include "src/parser/MappedFile.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" @@ -31,7 +32,7 @@ namespace storm { } // Find out about the used line endings. - SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + SupportedLineEndings lineEndings = findUsedLineEndings(filename, true); MappedFile file(filename.c_str()); char* buf = file.data; diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index ba9ec8323..91e28c9d2 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -8,6 +8,7 @@ #include "src/parser/AutoParser.h" #include "src/parser/Parser.h" +#include "src/parser/MappedFile.h" #include "src/parser/DeterministicModelParser.h" #include "src/parser/NondeterministicModelParser.h" @@ -68,7 +69,7 @@ namespace storm { storm::models::ModelType hintType = storm::models::Unknown; // Find out the line endings used within the file. - storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename); + storm::parser::SupportedLineEndings lineEndings = storm::parser::findUsedLineEndings(filename); // Open the file. MappedFile file(filename.c_str()); @@ -90,5 +91,5 @@ namespace storm { return hintType; } - } -} + } // namespace parser +} // namespace storm diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index d09897922..2e52fad59 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -9,38 +9,38 @@ namespace storm { namespace parser { class AutoParser { - public: - - /*! - * Checks the given files and parses the model within these files. - * - * This parser analyzes the format hint in the first line of the transition - * file. If this is a valid format, it will use the parser for this format, - * otherwise it will throw an exception. - * - * When the files are parsed successfully, a shared pointer owning the resulting model is returned. - * The concrete model can be obtained using the as() member of the AbstractModel class. - * - * @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. - * @return A shared_ptr containing the resulting model. - */ - static std::shared_ptr> parseModel(std::string const & transitionSystemFile, - std::string const & labelingFile, - std::string const & stateRewardFile = "", - std::string const & transitionRewardFile = ""); - - private: - - /*! - * Opens the given file and parses the file format hint. - * - * @param filename The path and name of the file that is to be analysed. - * @return The type of the model as an enum value. - */ - static storm::models::ModelType analyzeHint(const std::string& filename); + public: + + /*! + * Checks the given files and parses the model within these files. + * + * This parser analyzes the format hint in the first line of the transition + * file. If this is a valid format, it will use the parser for this format, + * otherwise it will throw an exception. + * + * When the files are parsed successfully, a shared pointer owning the resulting model is returned. + * The concrete model can be obtained using the as() member of the AbstractModel class. + * + * @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. + * @return A shared_ptr containing the resulting model. + */ + static std::shared_ptr> parseModel(std::string const & transitionSystemFile, + std::string const & labelingFile, + std::string const & stateRewardFile = "", + std::string const & transitionRewardFile = ""); + + private: + + /*! + * Opens the given file and parses the file format hint. + * + * @param filename The path and name of the file that is to be analysed. + * @return The type of the model as an enum value. + */ + static storm::models::ModelType analyzeHint(const std::string& filename); }; } // namespace parser diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index ca841396a..48b613644 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -28,24 +28,25 @@ namespace parser { */ DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { - storm::storage::SparseMatrix resultTransitionSystem(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile))); + // Parse the transitions. + storm::storage::SparseMatrix transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionSystemFile))); - uint_fast64_t stateCount = resultTransitionSystem.getColumnCount(); - uint_fast64_t rowCount = resultTransitionSystem.getRowCount(); + uint_fast64_t stateCount = transitions.getColumnCount(); + // Parse the state labeling. storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile))); - DeterministicModelParser::Result result(std::move(resultTransitionSystem), std::move(labeling)); + // Construct the result. + DeterministicModelParser::Result result(std::move(transitions), std::move(labeling)); - // Only parse state rewards of a file is given. + // Only parse state rewards if a file is given. if (stateRewardFile != "") { - result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile)); + result.stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile); } - // Only parse transition rewards of a file is given. + // Only parse transition rewards if a file is given. if (transitionRewardFile != "") { - RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, nullptr); - result.transitionRewards.reset(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo))); + result.transitionRewards = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFile, result.transitionSystem); } return result; diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 2ac9098bd..666a45039 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -15,7 +15,7 @@ #include #include "src/utility/constants.h" - +#include "src/parser/MappedFile.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" #include "src/settings/Settings.h" @@ -25,241 +25,239 @@ extern log4cplus::Logger logger; namespace storm { + namespace parser { -namespace parser { + storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename) { -storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename, bool insertDiagonalEntriesIfMissing) { + storm::storage::SparseMatrix emptyMatrix; - RewardMatrixInformationStruct nullInformation; + return DeterministicSparseTransitionParser::parse(filename, false, emptyMatrix); + } - return DeterministicSparseTransitionParser::parse(filename, false, nullInformation, insertDiagonalEntriesIfMissing); -} + storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const & transitionMatrix) { -storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) { + return DeterministicSparseTransitionParser::parse(filename, true, transitionMatrix); + } - return DeterministicSparseTransitionParser::parse(filename, true, rewardMatrixInformation); -} + storm::storage::SparseMatrix DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & transitionMatrix) { + // Enforce locale where decimal point is '.'. + setlocale(LC_NUMERIC, "C"); -DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing) { + 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."; + } - DeterministicSparseTransitionParser::FirstPassResult result; + // Find out about the used line endings. + SupportedLineEndings lineEndings = findUsedLineEndings(filename, true); - // Skip the format hint if it is there. - buf = trimWhitespaces(buf); - if(buf[0] < '0' || buf[0] > '9') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); - } + // Open file. + MappedFile file(filename.c_str()); + char* buf = file.data; - // Check all transitions for non-zero diagonal entries and deadlock states. - uint_fast64_t row, col, lastRow = 0; - bool rowHadDiagonalEntry = false; - while (buf[0] != '\0') { + // Perform first pass, i.e. count entries that are not zero. + bool insertDiagonalEntriesIfMissing = !isRewardFile; + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing); - // Read the transition. - row = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - // The actual read value is not needed here. - checked_strtod(buf, &buf); + LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); - // Compensate for missing diagonal entries if desired. - if (insertDiagonalEntriesIfMissing) { - if (lastRow != row) { - if(!rowHadDiagonalEntry) { - ++result.numberOfNonzeroEntries; + // 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(); } - // Compensate for missing rows. - for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { - ++result.numberOfNonzeroEntries; + // Perform second pass. + + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] < '0' || buf[0] > '9') { + buf = storm::parser::forwardToNextLine(buf, lineEndings); } - lastRow = row; - rowHadDiagonalEntry = false; - } - if (col == row) { - rowHadDiagonalEntry = true; - } + if(isRewardFile) { + // The reward matrix should match the size of the transition matrix. + if (firstPass.highestStateIndex + 1 > transitionMatrix.getRowCount() || firstPass.highestStateIndex + 1 > transitionMatrix.getColumnCount()) { + 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 = transitionMatrix.getRowCount() - 1; + } + } - if (col > row && !rowHadDiagonalEntry) { - rowHadDiagonalEntry = true; - ++result.numberOfNonzeroEntries; - } - } + // 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); - // Check if a higher state id was found. - if (row > result.highestStateIndex) result.highestStateIndex = row; - if (col > result.highestStateIndex) result.highestStateIndex = col; + uint_fast64_t row, col, lastRow = 0; + double val; + bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); + bool hadDeadlocks = false; + bool rowHadDiagonalEntry = false; - ++result.numberOfNonzeroEntries; - buf = trimWhitespaces(buf); - } - if(insertDiagonalEntriesIfMissing) { - if (!rowHadDiagonalEntry) { - ++result.numberOfNonzeroEntries; - } + // 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. - //Compensate for missing rows at the end of the file. - for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { - ++result.numberOfNonzeroEntries; - } - } + // Different parsing routines for transition systems and transition rewards. + if(isRewardFile) { + while (buf[0] != '\0') { - return result; -} + // Read next transition. + row = checked_strtol(buf, &buf); + col = checked_strtol(buf, &buf); + val = checked_strtod(buf, &buf); -storm::storage::SparseMatrix DeterministicSparseTransitionParser::parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation, bool insertDiagonalEntriesIfMissing) { - // Enforce locale where decimal point is '.'. - setlocale(LC_NUMERIC, "C"); + 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(); + } - 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."; - } + // 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; + } - // Find out about the used line endings. - SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + if (col == row) { + rowHadDiagonalEntry = true; + } - // Open file. - MappedFile file(filename.c_str()); - char* buf = file.data; + 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; + } - // Perform first pass, i.e. count entries that are not zero. + resultMatrix.addNextValue(row, col, val); + buf = trimWhitespaces(buf); + } - DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing); + 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."); + } + } - LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); + // 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."; + } - // 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(); + // Finally, build the actual matrix and return it. + return resultMatrix.build(); } - // Perform second pass. + DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings, bool insertDiagonalEntriesIfMissing) { - // Skip the format hint if it is there. - buf = trimWhitespaces(buf); - if(buf[0] < '0' || buf[0] > '9') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); - } + DeterministicSparseTransitionParser::FirstPassResult result; - if(isRewardFile) { - // 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; + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] < '0' || buf[0] > '9') { + buf = storm::parser::forwardToNextLine(buf, lineEndings); } - } - - // 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); - uint_fast64_t row, col, lastRow = 0; - double val; - bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); - bool hadDeadlocks = false; - bool rowHadDiagonalEntry = false; - - - // 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. - - // Different parsing routines for transition systems and transition rewards. - if(isRewardFile) { - while (buf[0] != '\0') { - - // Read next transition. - row = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - val = checked_strtod(buf, &buf); - - resultMatrix.addNextValue(row, col, val); - buf = trimWhitespaces(buf); - } - } else { + // Check all transitions for non-zero diagonal entries and deadlock states. + uint_fast64_t row, col, lastRow = 0; + bool rowHadDiagonalEntry = false; while (buf[0] != '\0') { - // Read next transition. + // Read the transition. row = checked_strtol(buf, &buf); col = checked_strtol(buf, &buf); - val = checked_strtod(buf, &buf); + // The actual read value is not needed here. + 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."); + // Compensate for missing diagonal entries if desired. + if (insertDiagonalEntriesIfMissing) { + if (lastRow != row) { + if(!rowHadDiagonalEntry) { + ++result.numberOfNonzeroEntries; } - // 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. + + // Compensate for missing rows. + for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { + ++result.numberOfNonzeroEntries; } + lastRow = row; + rowHadDiagonalEntry = false; } - lastRow = row; - rowHadDiagonalEntry = false; - } - if (col == row) { - rowHadDiagonalEntry = true; - } + if (col == row) { + rowHadDiagonalEntry = true; + } - 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."); + if (col > row && !rowHadDiagonalEntry) { + rowHadDiagonalEntry = true; + ++result.numberOfNonzeroEntries; } - rowHadDiagonalEntry = true; } - resultMatrix.addNextValue(row, col, val); + // Check if a higher state id was found. + if (row > result.highestStateIndex) result.highestStateIndex = row; + if (col > result.highestStateIndex) result.highestStateIndex = col; + + ++result.numberOfNonzeroEntries; 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(insertDiagonalEntriesIfMissing) { + if (!rowHadDiagonalEntry) { + ++result.numberOfNonzeroEntries; + } + + //Compensate for missing rows at the end of the file. + for (uint_fast64_t skippedRow = (uint_fast64_t)(lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { + ++result.numberOfNonzeroEntries; } } - // 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 result; } - // Finally, build the actual matrix and return it. - return resultMatrix.build(); -} - -} // namespace parser - + } // namespace parser } // namespace storm diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 004210aa1..a9147f763 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -34,7 +34,7 @@ public: * @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); + static storm::storage::SparseMatrix parseDeterministicTransitions(std::string const& filename); /*! * Load the transition rewards for a deterministic transition system from file and create a @@ -46,10 +46,11 @@ public: * 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. + * @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in. + * The dimensions (rows and columns) of the two matrices should match. * @return A SparseMatrix containing the parsed transition rewards. */ - static storm::storage::SparseMatrix parseDeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation); + static storm::storage::SparseMatrix parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix const & transitionMatrix); private: @@ -62,7 +63,7 @@ private: * @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 structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool insertDiagonalEntriesIfMissing = true); + static FirstPassResult firstPass(char* buffer, SupportedLineEndings lineEndings, bool insertDiagonalEntriesIfMissing = true); /* * The main parsing routine. @@ -71,10 +72,11 @@ private: * @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. + * @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in. + * The dimensions (rows and columns) of the two matrices should match. * @return A SparseMatrix containing the parsed file contents. */ - static storm::storage::SparseMatrix parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation, bool insertDiagonalEntriesIfMissing = false); + static storm::storage::SparseMatrix parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix const & transitionMatrix); }; diff --git a/src/parser/MappedFile.cpp b/src/parser/MappedFile.cpp new file mode 100644 index 000000000..69d9fd4a9 --- /dev/null +++ b/src/parser/MappedFile.cpp @@ -0,0 +1,101 @@ +/* + * MappedFile.cpp + * + * Created on: Jan 21, 2014 + * Author: Manuel Sascha Weiand + */ + +#include "src/parser/MappedFile.h" + +#include +#include +#include + +#include +#include + +#include + +#include "src/exceptions/FileIoException.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +namespace storm { + namespace parser { + + MappedFile::MappedFile(const char* filename) { + #if defined LINUX || defined MACOSX + /* + * Do file mapping for reasonable systems. + * stat64(), open(), mmap() + */ + #ifdef MACOSX + if (stat(filename, &(this->st)) != 0) { + #else + if (stat64(filename, &(this->st)) != 0) { + #endif + LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << "): Probably, this file does not exist."); + throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist."; + } + this->file = open(filename, O_RDONLY); + + if (this->file < 0) { + LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file."); + throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file."; + } + + this->data = reinterpret_cast(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0)); + if (this->data == reinterpret_cast(-1)) { + close(this->file); + LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno)); + throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno); + } + this->dataend = this->data + this->st.st_size; + #elif defined WINDOWS + /* + * Do file mapping for windows. + * _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile() + */ + if (_stat64(filename, &(this->st)) != 0) { + LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << "): Probably, this file does not exist."); + throw exceptions::FileIoException("MappedFile Error in stat(): Probably, this file does not exist."); + } + + this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL); + if (this->file == INVALID_HANDLE_VALUE) { + LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << "): Probably, we may not read this file."); + throw exceptions::FileIoException("MappedFile Error in CreateFileA(): Probably, we may not read this file."); + } + + this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL); + if (this->mapping == NULL) { + CloseHandle(this->file); + LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ")."); + throw exceptions::FileIoException("MappedFile Error in CreateFileMappingA()."); + } + + this->data = static_cast(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size)); + if (this->data == NULL) { + CloseHandle(this->mapping); + CloseHandle(this->file); + LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ")."); + throw exceptions::FileIoException("MappedFile Error in MapViewOfFile()."); + } + this->dataend = this->data + this->st.st_size; + #endif + } + + MappedFile::~MappedFile() { + #if defined LINUX || defined MACOSX + munmap(this->data, this->st.st_size); + close(this->file); + #elif defined WINDOWS + CloseHandle(this->mapping); + CloseHandle(this->file); + #endif + } + } // namespace parser +} // namespace storm + diff --git a/src/parser/MappedFile.h b/src/parser/MappedFile.h new file mode 100644 index 000000000..8b66b0fde --- /dev/null +++ b/src/parser/MappedFile.h @@ -0,0 +1,95 @@ +/* + * MappedFile.h + * + * Created on: Jan 21, 2014 + * Author: Manuel Sascha Weiand + */ + +#ifndef STORM_PARSER_MAPPEDFILE_H_ +#define STORM_PARSER_MAPPEDFILE_H_ + +#include + +#include "src/utility/OsDetection.h" + +namespace storm { + namespace parser { + /*! + * @brief Opens a file and maps it to memory providing a char* + * containing the file content. + * + * This class is a very simple interface to read files efficiently. + * The given file is opened and mapped to memory using mmap(). + * The public member data is a pointer to the actual file content. + * Using this method, the kernel will take care of all buffering. This is + * most probably much more efficient than doing this manually. + */ + + #if !defined LINUX && !defined MACOSX && !defined WINDOWS + #error Platform not supported + #endif + + class MappedFile { + + public: + + /*! + * Constructor of MappedFile. + * Will stat the given file, open it and map it to memory. + * If anything of this fails, an appropriate exception is raised + * and a log entry is written. + * @param filename file to be opened + */ + MappedFile(const char* filename); + + /*! + * Destructor of MappedFile. + * Will unmap the data and close the file. + */ + ~MappedFile(); + + /*! + * @brief pointer to actual file content. + */ + char* data; + + /*! + * @brief pointer to end of file content. + */ + char* dataend; + + private: + + #if defined LINUX || defined MACOSX + /*! + * @brief file descriptor obtained by open(). + */ + int file; + #elif defined WINDOWS + HANDLE file; + HANDLE mapping; + #endif + + #if defined LINUX + /*! + * @brief stat information about the file. + */ + struct stat64 st; + #elif defined MACOSX + /*! + * @brief stat information about the file. + */ + struct stat st; + #elif defined WINDOWS + /*! + * @brief stat information about the file. + */ + struct __stat64 st; + #endif + }; + } // namespace parser +} // namespace storm + + + +#endif /* STORM_PARSER_MAPPEDFILE_H_ */ diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 15a7c5809..de950aab8 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -2,12 +2,13 @@ #include "src/settings/Settings.h" #include "src/exceptions/WrongFormatException.h" +#include "MappedFile.h" namespace storm { namespace parser { -MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings) { +MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -142,7 +143,7 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran return result; } -MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult) { +MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndings lineEndings, FirstPassResult const& firstPassResult) { ResultType result(firstPassResult); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -252,7 +253,7 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio } // Determine used line endings. - SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + SupportedLineEndings lineEndings = findUsedLineEndings(filename, true); // Open file and prepare pointer to buffer. MappedFile file(filename.c_str()); diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index ef89371e0..25f9291dc 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -80,7 +80,7 @@ private: * @param lineEndings The line endings that are to be used while parsing. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings); + static FirstPassResult firstPass(char* buffer, SupportedLineEndings lineEndings); /* * Performs the second pass on the input pointed to by the given buffer with the information of the first pass. @@ -90,7 +90,7 @@ private: * @param firstPassResult The result of the first pass performed on the same input. * @return A structure representing the result of the second pass. */ - static ResultType secondPass(char* buffer, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult); + static ResultType secondPass(char* buffer, SupportedLineEndings lineEndings, FirstPassResult const& firstPassResult); }; } // namespace parser diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index 528f62f51..82a7f3085 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -29,26 +29,31 @@ namespace storm { NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { - NondeterministicSparseTransitionParser::Result transitionParserResult(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile))); - storm::storage::SparseMatrix transitions(std::move(transitionParserResult.transitionMatrix)); + // Parse the transitions. + NondeterministicSparseTransitionParser::Result transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionSystemFile))); - uint_fast64_t stateCount = transitions.getColumnCount(); - uint_fast64_t rowCount = transitions.getRowCount(); + uint_fast64_t stateCount = transitions.transitionMatrix.getColumnCount(); + // Parse the state labeling. storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile))); - Result result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling)); - - // Only parse state rewards of a file is given. + // Only parse state rewards if a file is given. + boost::optional> stateRewards; if (stateRewardFile != "") { - result.stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile)); + stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFile); } - // Only parse transition rewards of a file is given. + // Only parse transition rewards if a file is given. + boost::optional> transitionRewards; if (transitionRewardFile != "") { - RewardMatrixInformationStruct rewardMatrixInfo(rowCount, stateCount, &result.rowMapping); - result.transitionRewards.reset(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, rewardMatrixInfo).transitionMatrix); + transitionRewards = storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFile, transitions).transitionMatrix; } + + // Construct the result. + Result result(std::move(transitions.transitionMatrix), std::move(transitions.rowMapping), std::move(labeling)); + result.stateRewards = stateRewards; + result.transitionRewards = transitionRewards; + return result; } diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index fa20585ec..3c7ebbaab 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -9,6 +9,7 @@ #include +#include "src/parser/MappedFile.h" #include "src/settings/Settings.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" @@ -22,125 +23,17 @@ namespace storm { NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) { - RewardMatrixInformationStruct nullInformation; + Result emptyResult; - return NondeterministicSparseTransitionParser::parse(filename, false, nullInformation); + return NondeterministicSparseTransitionParser::parse(filename, false, emptyResult); } - NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, RewardMatrixInformationStruct const& rewardMatrixInformation) { + NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(std::string const& filename, Result const & modelInformation) { - return NondeterministicSparseTransitionParser::parse(filename, true, rewardMatrixInformation); + return NondeterministicSparseTransitionParser::parse(filename, true, modelInformation); } - NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation) { - - // Check file header and extract number of transitions. - - // Skip the format hint if it is there. - buf = trimWhitespaces(buf); - if(buf[0] < '0' || buf[0] > '9') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); - } - - // Read all transitions. - uint_fast64_t source = 0, target = 0, choice = 0, lastchoice = 0, lastsource = 0; - double val = 0.0; - NondeterministicSparseTransitionParser::FirstPassResult result; - - // Since the first line is already a new choice but is not covered below, that has to be covered here. - result.choices = 1; - - while (buf[0] != '\0') { - - // Read source state and choice. - source = checked_strtol(buf, &buf); - - // Read the name of the nondeterministic choice. - choice = checked_strtol(buf, &buf); - - // Check if we encountered a state index that is bigger than all previously seen. - if (source > result.highestStateIndex) { - result.highestStateIndex = source; - } - - if (isRewardFile) { - // If we have switched the source state, we possibly need to insert rows for skipped choices of the last - // source state. - if (source != lastsource) { - // number of choices skipped = number of choices of last state - number of choices read - result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource]) - (lastchoice + 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) { - result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[i]); - } - - // If we advanced to the next state, but skipped some choices, we have to reserve rows - // for them. - if (source != lastsource) { - result.choices += choice + 1; - } else if (choice != lastchoice) { - result.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) { - result.numberOfNonzeroEntries += source - lastsource - 1; - result.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. - ++result.choices; - } - } - - // Read target and check if we encountered a state index that is bigger than all previously - // seen. - target = checked_strtol(buf, &buf); - if (target > result.highestStateIndex) { - result.highestStateIndex = target; - } - - // Read value and check whether it's positive. - 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) << "\"."); - NondeterministicSparseTransitionParser::FirstPassResult nullResult; - return nullResult; - } - - lastchoice = choice; - lastsource = source; - - // Increase number of non-zero values. - result.numberOfNonzeroEntries++; - - // The PRISM output format lists the name of the transition in the fourth column, - // but omits the fourth column if it is an internal action. In either case we can skip to the end of the line. - buf = forwardToLineEnd(buf, lineEndings); - - buf = trimWhitespaces(buf); - } - - if (isRewardFile) { - // If not all rows were filled for the last state, we need to insert them. - result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource] ) - (lastchoice + 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 < rewardMatrixInformation.nondeterministicChoiceIndices->size() - 1; ++i) { - result.choices += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[i]); - } - } - - return result; - } - - NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation) { + NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parse(std::string const &filename, bool isRewardFile, Result const & modelInformation) { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); @@ -151,14 +44,14 @@ namespace storm { } // Find out about the used line endings. - SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + SupportedLineEndings lineEndings = findUsedLineEndings(filename, true); // Open file. MappedFile file(filename.c_str()); char* buf = file.data; // Perform first pass, i.e. obtain number of columns, rows and non-zero elements. - NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.data, lineEndings, isRewardFile, rewardMatrixInformation); + NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.data, lineEndings, isRewardFile, modelInformation); // If first pass returned zero, the file format was wrong. if (firstPass.numberOfNonzeroEntries == 0) { @@ -176,14 +69,14 @@ namespace storm { if (isRewardFile) { // The reward matrix should match the size of the transition matrix. - if (firstPass.choices > rewardMatrixInformation.rowCount || (uint_fast64_t)(firstPass.highestStateIndex + 1) > rewardMatrixInformation.columnCount) { + if (firstPass.choices > modelInformation.transitionMatrix.getRowCount() || (uint_fast64_t)(firstPass.highestStateIndex + 1) > modelInformation.transitionMatrix.getColumnCount()) { LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size."); throw storm::exceptions::WrongFormatException() << "Reward matrix size exceeds transition matrix size."; - } else if (firstPass.choices != rewardMatrixInformation.rowCount) { + } else if (firstPass.choices != modelInformation.transitionMatrix.getRowCount()) { LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count."); throw storm::exceptions::WrongFormatException() << "Reward matrix row count does not match transition matrix row count."; } else { - firstPass.highestStateIndex = rewardMatrixInformation.columnCount - 1; + firstPass.highestStateIndex = modelInformation.transitionMatrix.getColumnCount() - 1; } } @@ -214,13 +107,13 @@ namespace storm { // If we have switched the source state, we possibly need to insert the rows of the last // source state. if (source != lastsource) { - curRow += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[lastsource]) -(lastchoice + 1); + curRow += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[lastsource]) -(lastchoice + 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 += ((*rewardMatrixInformation.nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation.nondeterministicChoiceIndices)[i]); + curRow += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); } // If we advanced to the next state, but skipped some choices, we have to reserve rows @@ -279,5 +172,113 @@ namespace storm { return NondeterministicSparseTransitionParser::Result(matrixBuilder.build(), rowMapping); } + NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings, bool isRewardFile, Result const & modelInformation) { + + // Check file header and extract number of transitions. + + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] < '0' || buf[0] > '9') { + buf = storm::parser::forwardToNextLine(buf, lineEndings); + } + + // Read all transitions. + uint_fast64_t source = 0, target = 0, choice = 0, lastchoice = 0, lastsource = 0; + double val = 0.0; + NondeterministicSparseTransitionParser::FirstPassResult result; + + // Since the first line is already a new choice but is not covered below, that has to be covered here. + result.choices = 1; + + while (buf[0] != '\0') { + + // Read source state and choice. + source = checked_strtol(buf, &buf); + + // Read the name of the nondeterministic choice. + choice = checked_strtol(buf, &buf); + + // Check if we encountered a state index that is bigger than all previously seen. + if (source > result.highestStateIndex) { + result.highestStateIndex = source; + } + + if (isRewardFile) { + // If we have switched the source state, we possibly need to insert rows for skipped choices of the last + // source state. + if (source != lastsource) { + // number of choices skipped = number of choices of last state - number of choices read + result.choices += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[lastsource]) - (lastchoice + 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) { + result.choices += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); + } + + // If we advanced to the next state, but skipped some choices, we have to reserve rows + // for them. + if (source != lastsource) { + result.choices += choice + 1; + } else if (choice != lastchoice) { + result.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) { + result.numberOfNonzeroEntries += source - lastsource - 1; + result.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. + ++result.choices; + } + } + + // Read target and check if we encountered a state index that is bigger than all previously + // seen. + target = checked_strtol(buf, &buf); + if (target > result.highestStateIndex) { + result.highestStateIndex = target; + } + + // Read value and check whether it's positive. + 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) << "\"."); + NondeterministicSparseTransitionParser::FirstPassResult nullResult; + return nullResult; + } + + lastchoice = choice; + lastsource = source; + + // Increase number of non-zero values. + result.numberOfNonzeroEntries++; + + // The PRISM output format lists the name of the transition in the fourth column, + // but omits the fourth column if it is an internal action. In either case we can skip to the end of the line. + buf = forwardToLineEnd(buf, lineEndings); + + buf = trimWhitespaces(buf); + } + + if (isRewardFile) { + // If not all rows were filled for the last state, we need to insert them. + result.choices += ((modelInformation.rowMapping)[lastsource + 1] - (modelInformation.rowMapping)[lastsource] ) - (lastchoice + 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 < modelInformation.rowMapping.size() - 1; ++i) { + result.choices += ((modelInformation.rowMapping)[i + 1] - (modelInformation.rowMapping)[i]); + } + } + + return result; + } + } // namespace parser } // namespace storm diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index 34fc3f397..3df4834ae 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -39,6 +39,12 @@ namespace storm { */ struct Result { + // Constructs an empty Result. + Result() : transitionMatrix(), rowMapping() { + // Intentionally left empty. + } + + // Constructs a Result, initializing its members with the given values. Result(storm::storage::SparseMatrix transitionMatrix, std::vector rowMapping) : transitionMatrix(transitionMatrix), rowMapping(rowMapping) { // Intentionally left empty. } @@ -52,16 +58,22 @@ namespace storm { }; /*! - * @brief Load a nondeterministic transition system from file and create a - * sparse adjacency matrix whose entries represent the weights of the edges + * @brief Load a nondeterministic 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. */ - static Result parseNondeterministicTransitions(std::string const &filename); + static Result parseNondeterministicTransitions(std::string const & filename); /*! * @brief Load a nondeterministic 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 modelInformation The information about the transition structure of nondeterministic model in which the transition rewards shall be used. + * @return A struct containing the parsed file contents, i.e. the transition reward matrix and the mapping between its rows and the states of the model. */ - static Result parseNondeterministicTransitionRewards(std::string const &filename, RewardMatrixInformationStruct const& rewardMatrixInformation); + static Result parseNondeterministicTransitionRewards(std::string const & filename, Result const & modelInformation); private: @@ -79,7 +91,7 @@ namespace storm { * @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 structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer, SupportedLineEndingsEnum lineEndings, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation); + static FirstPassResult firstPass(char* buffer, SupportedLineEndings lineEndings, bool isRewardFile, Result const & modelInformation); /*! * The main parsing routine. @@ -88,10 +100,10 @@ namespace storm { * @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. + * @param modelInformation 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 Result parse(std::string const& filename, bool isRewardFile, RewardMatrixInformationStruct const& rewardMatrixInformation); + static Result parse(std::string const& filename, bool isRewardFile, Result const & modelInformation); }; diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index b1b0c6e79..9e4113445 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -11,6 +11,7 @@ #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" #include "src/utility/OsDetection.h" +#include "src/parser/MappedFile.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -91,7 +92,7 @@ char* trimWhitespaces(char* buf) { /*! * @briefs Analyzes the given file and tries to find out the used file endings. */ -SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) { +SupportedLineEndings findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) { MappedFile fileMap(fileName.c_str()); char* buf = nullptr; char* const bufferEnd = fileMap.dataend; @@ -100,11 +101,11 @@ SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool t if (*buf == '\r') { // check for following \n if (((buf + sizeof(char)) < bufferEnd) && (*(buf + sizeof(char)) == '\n')) { - return SupportedLineEndingsEnum::SlashRN; + return SupportedLineEndings::SlashRN; } - return SupportedLineEndingsEnum::SlashR; + return SupportedLineEndings::SlashR; } else if (*buf == '\n') { - return SupportedLineEndingsEnum::SlashN; + return SupportedLineEndings::SlashN; } } @@ -114,25 +115,25 @@ SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool t } LOG4CPLUS_WARN(logger, "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n"); - return SupportedLineEndingsEnum::Unsupported; + return SupportedLineEndings::Unsupported; } /*! * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character). */ -char* forwardToLineEnd(char* buffer, SupportedLineEndingsEnum lineEndings) { +char* forwardToLineEnd(char* buffer, SupportedLineEndings lineEndings) { switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: + case SupportedLineEndings::SlashN: return buffer + strcspn(buffer, "\n\0"); break; - case SupportedLineEndingsEnum::SlashR: + case SupportedLineEndings::SlashR: return buffer + strcspn(buffer, "\r\0"); break; - case SupportedLineEndingsEnum::SlashRN: + case SupportedLineEndings::SlashRN: return buffer + strcspn(buffer, "\r\0"); break; default: - case SupportedLineEndingsEnum::Unsupported: + case SupportedLineEndings::Unsupported: // This Line will never be reached as the Parser would have thrown already. throw; break; @@ -143,19 +144,19 @@ char* forwardToLineEnd(char* buffer, SupportedLineEndingsEnum lineEndings) { /*! * @brief Encapsulates the usage of function @strchr to forward to the next line */ -char* forwardToNextLine(char* buffer, SupportedLineEndingsEnum lineEndings) { +char* forwardToNextLine(char* buffer, SupportedLineEndings lineEndings) { switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: + case SupportedLineEndings::SlashN: return strchr(buffer, '\n') + 1; break; - case SupportedLineEndingsEnum::SlashR: + case SupportedLineEndings::SlashR: return strchr(buffer, '\r') + 1; break; - case SupportedLineEndingsEnum::SlashRN: + case SupportedLineEndings::SlashRN: return strchr(buffer, '\r') + 2; break; default: - case SupportedLineEndingsEnum::Unsupported: + case SupportedLineEndings::Unsupported: // This Line will never be reached as the Parser would have thrown already. throw; break; @@ -168,26 +169,26 @@ char* forwardToNextLine(char* buffer, SupportedLineEndingsEnum lineEndings) { * @param targetBuffer The Target for the hint, must be at least 64 bytes long * @param buffer The Source Buffer from which the Model Hint will be read */ -void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, SupportedLineEndingsEnum lineEndings) { +void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, SupportedLineEndings lineEndings) { if (targetBufferSize <= 4) { throw; } switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: + case SupportedLineEndings::SlashN: #ifdef WINDOWS sscanf_s(buffer, "%60s\n", targetBuffer, targetBufferSize); #else sscanf(buffer, "%60s\n", targetBuffer); #endif break; - case SupportedLineEndingsEnum::SlashR: + case SupportedLineEndings::SlashR: #ifdef WINDOWS sscanf_s(buffer, "%60s\r", targetBuffer, sizeof(targetBufferSize)); #else sscanf(buffer, "%60s\r", targetBuffer); #endif break; - case SupportedLineEndingsEnum::SlashRN: + case SupportedLineEndings::SlashRN: #ifdef WINDOWS sscanf_s(buffer, "%60s\r\n", targetBuffer, sizeof(targetBufferSize)); #else @@ -195,7 +196,7 @@ void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char c #endif break; default: - case SupportedLineEndingsEnum::Unsupported: + case SupportedLineEndings::Unsupported: // This Line will never be reached as the Parser would have thrown already. throw; break; @@ -205,13 +206,13 @@ void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char c /*! * @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0 */ -void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, SupportedLineEndingsEnum lineEndings) { +void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, SupportedLineEndings lineEndings) { if (targetBufferSize < 5) { LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed Target Buffer is too small."); throw; } switch (lineEndings) { - case SupportedLineEndingsEnum::SlashN: { + case SupportedLineEndings::SlashN: { char source[] = " \n\t"; #ifdef WINDOWS strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); @@ -220,7 +221,7 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi #endif break; } - case SupportedLineEndingsEnum::SlashR: { + case SupportedLineEndings::SlashR: { char source[] = " \r\t"; #ifdef WINDOWS strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); @@ -229,7 +230,7 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi #endif break; } - case SupportedLineEndingsEnum::SlashRN: { + case SupportedLineEndings::SlashRN: { char source[] = " \r\n\t"; #ifdef WINDOWS strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); @@ -239,7 +240,7 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi break; } default: - case SupportedLineEndingsEnum::Unsupported: + case SupportedLineEndings::Unsupported: // This Line will never be reached as the Parser would have thrown already. LOG4CPLUS_ERROR(logger, "getMatchingSeparatorString: The passed lineEndings were Unsupported. Check your input file."); throw; @@ -247,87 +248,6 @@ void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSi } } -/*! - * Will stat the given file, open it and map it to memory. - * If anything of this fails, an appropriate exception is raised - * and a log entry is written. - * @param filename file to be opened - */ -MappedFile::MappedFile(const char* filename) { -#if defined LINUX || defined MACOSX - /* - * Do file mapping for reasonable systems. - * stat64(), open(), mmap() - */ -#ifdef MACOSX - if (stat(filename, &(this->st)) != 0) { -#else - if (stat64(filename, &(this->st)) != 0) { -#endif - LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << "): Probably, this file does not exist."); - throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist."; - } - this->file = open(filename, O_RDONLY); - - if (this->file < 0) { - LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file."); - throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file."; - } - - this->data = reinterpret_cast(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0)); - if (this->data == reinterpret_cast(-1)) { - close(this->file); - LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno)); - throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno); - } - this->dataend = this->data + this->st.st_size; -#elif defined WINDOWS - /* - * Do file mapping for windows. - * _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile() - */ - if (_stat64(filename, &(this->st)) != 0) { - LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << "): Probably, this file does not exist."); - throw exceptions::FileIoException("MappedFile Error in stat(): Probably, this file does not exist."); - } - - this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL); - if (this->file == INVALID_HANDLE_VALUE) { - LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << "): Probably, we may not read this file."); - throw exceptions::FileIoException("MappedFile Error in CreateFileA(): Probably, we may not read this file."); - } - - this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL); - if (this->mapping == NULL) { - CloseHandle(this->file); - LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ")."); - throw exceptions::FileIoException("MappedFile Error in CreateFileMappingA()."); - } - - this->data = static_cast(MapViewOfFile(this->mapping, FILE_MAP_READ, 0, 0, this->st.st_size)); - if (this->data == NULL) { - CloseHandle(this->mapping); - CloseHandle(this->file); - LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ")."); - throw exceptions::FileIoException("MappedFile Error in MapViewOfFile()."); - } - this->dataend = this->data + this->st.st_size; -#endif -} - -/*! - * Will unmap the data and close the file. - */ -MappedFile::~MappedFile() { -#if defined LINUX || defined MACOSX - munmap(this->data, this->st.st_size); - close(this->file); -#elif defined WINDOWS - CloseHandle(this->mapping); - CloseHandle(this->file); -#endif -} - } // namespace parser } // namespace storm diff --git a/src/parser/Parser.h b/src/parser/Parser.h index b2cfb0677..962f699eb 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -16,161 +16,78 @@ namespace storm { -/*! - * @brief Contains all file parser and helper classes. - * - * This namespace contains everything needed to load data files (like - * atomic propositions, transition systems, formulas, ...) including - * methods for efficient file access (see MappedFile). - */ -namespace parser { - -struct RewardMatrixInformationStruct { - RewardMatrixInformationStruct() : rowCount(0), columnCount(0), nondeterministicChoiceIndices(nullptr) { - // Intentionally left empty. - } - - RewardMatrixInformationStruct(uint_fast64_t rowCount, uint_fast64_t columnCount, std::vector const * const nondeterministicChoiceIndices) - : rowCount(rowCount), columnCount(columnCount), nondeterministicChoiceIndices(nondeterministicChoiceIndices) { - // Intentionally left empty. - } - - uint_fast64_t rowCount; - uint_fast64_t columnCount; - std::vector const * const nondeterministicChoiceIndices; -}; - -/*! - * @brief Opens a file and maps it to memory providing a char* - * containing the file content. - * - * This class is a very simple interface to read files efficiently. - * The given file is opened and mapped to memory using mmap(). - * The public member data is a pointer to the actual file content. - * Using this method, the kernel will take care of all buffering. This is - * most probably much more efficient than doing this manually. - */ - -#if !defined LINUX && !defined MACOSX && !defined WINDOWS -#error Platform not supported -#endif - -class MappedFile { - private: -#if defined LINUX || defined MACOSX - /*! - * @brief file descriptor obtained by open(). - */ - int file; -#elif defined WINDOWS - HANDLE file; - HANDLE mapping; -#endif - -#if defined LINUX - /*! - * @brief stat information about the file. - */ - struct stat64 st; -#elif defined MACOSX - /*! - * @brief stat information about the file. - */ - struct stat st; -#elif defined WINDOWS - /*! - * @brief stat information about the file. - */ - struct __stat64 st; -#endif - - public: - /*! - * @brief pointer to actual file content. - */ - char* data; - - /*! - * @brief pointer to end of file content. - */ - char* dataend; - /*! - * @brief Constructor of MappedFile. + * @brief Contains all file parsers and helper classes. + * + * This namespace contains everything needed to load data files (like + * atomic propositions, transition systems, formulas, etc.) including + * methods for efficient file access (see MappedFile). */ - MappedFile(const char* filename); - + namespace parser { + /*! - * @brief Destructor of MappedFile. + * @brief Parses integer and checks, if something has been parsed. */ - ~MappedFile(); -}; - -/*! - * @brief Parses integer and checks, if something has been parsed. - */ -uint_fast64_t checked_strtol(const char* str, char** end); - -/*! - * @brief Parses floating point and checks, if something has been parsed. - */ -double checked_strtod(const char* str, char** end); - -/*! - * @brief Skips all non whitespace characters until the next whitespace. - */ -char* skipWord(char* buf); + uint_fast64_t checked_strtol(const char* str, char** end); -/*! - * @brief Skips common whitespaces in a string. - */ -char* trimWhitespaces(char* buf); + /*! + * @brief Parses floating point and checks, if something has been parsed. + */ + double checked_strtod(const char* str, char** end); -/*! - * @brief Tests whether the given file exists and is readable. - */ -bool fileExistsAndIsReadable(const char* fileName); + /*! + * @brief Skips all non whitespace characters until the next whitespace. + */ + char* skipWord(char* buf); -/*! - * @brief Enum Class Type containing all supported file endings. - */ -enum class SupportedLineEndingsEnum : unsigned short { - Unsupported = 0, - SlashR, - SlashN, - SlashRN -}; - -/*! - * @briefs Analyzes the given file and tries to find out the used line endings. - */ -storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported = false); + /*! + * @brief Skips common whitespaces in a string. + */ + char* trimWhitespaces(char* buf); -/*! - * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character). - */ -char* forwardToLineEnd(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); + /*! + * @brief Tests whether the given file exists and is readable. + */ + bool fileExistsAndIsReadable(const char* fileName); -/*! - * @brief Encapsulates the usage of function @strchr to forward to the next line - */ -char* forwardToNextLine(char* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); + /*! + * @brief Enum Class Type containing all supported file endings. + */ + enum class SupportedLineEndings : unsigned short { + Unsupported = 0, + SlashR, + SlashN, + SlashRN + }; -/*! - * @brief Encapsulates the usage of function @sscanf to scan for the model type hint - * @param targetBuffer The Target for the hint, should be at least 64 bytes long - * @param buffer The Source Buffer from which the Model Hint will be read + /*! + * @briefs Analyzes the given file and tries to find out the used line endings. + */ + storm::parser::SupportedLineEndings findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported = false); - */ -void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, storm::parser::SupportedLineEndingsEnum lineEndings); + /*! + * @brief Encapsulates the usage of function @strcspn to forward to the end of the line (next char is the newline character). + */ + char* forwardToLineEnd(char* buffer, storm::parser::SupportedLineEndings lineEndings); -/*! - * @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0 - */ -void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, storm::parser::SupportedLineEndingsEnum lineEndings); + /*! + * @brief Encapsulates the usage of function @strchr to forward to the next line + */ + char* forwardToNextLine(char* buffer, storm::parser::SupportedLineEndings lineEndings); -} // namespace parser + /*! + * @brief Encapsulates the usage of function @sscanf to scan for the model type hint + * @param targetBuffer The Target for the hint, should be at least 64 bytes long + * @param buffer The Source Buffer from which the Model Hint will be read + */ + void scanForModelHint(char* targetBuffer, uint_fast64_t targetBufferSize, char const* buffer, storm::parser::SupportedLineEndings lineEndings); + + /*! + * @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0 + */ + void getMatchingSeparatorString(char* targetBuffer, uint_fast64_t targetBufferSize, storm::parser::SupportedLineEndings lineEndings); + } // namespace parser } // namespace storm #endif /* STORM_PARSER_PARSER_H_ */ diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index 9a4e34be6..a0bd62ce3 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -12,6 +12,7 @@ #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" #include "src/parser/Parser.h" +#include "src/parser/MappedFile.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger;