From 2fc666892d8338f10fbb583ba5e4afed102af4f9 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 12 Jun 2013 21:04:32 +0200 Subject: [PATCH] Added multi plattform new-line handling for parsers Former-commit-id: f7df0996a78423afdb6a1ff630ca21d9bf6cff63 --- .../AtomicPropositionLabelingParser.cpp | 35 ++++++++++- .../DeterministicSparseTransitionParser.cpp | 38 ++++++++++-- .../DeterministicSparseTransitionParser.h | 2 +- ...NondeterministicSparseTransitionParser.cpp | 59 +++++++++++++++++-- src/parser/Parser.cpp | 11 +++- src/parser/Parser.h | 2 +- 6 files changed, 128 insertions(+), 19 deletions(-) diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index bed9e6d96..c1aab6ced 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -49,13 +49,42 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f throw storm::exceptions::FileIoException() << "The supplied Labeling input file \"" << filename << "\" does not exist or is not readable by this process."; } + /* + * Find out about the used line endings. + */ + SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + MappedFile file(filename.c_str()); char* buf = file.data; /* * First run: obtain number of propositions. */ - char separator[] = " \r\n\t"; + char separator[5];// = " \r\n\t"; + switch (lineEndings) { + case SupportedLineEndingsEnum::SlashN: + separator[0] = ' '; + separator[1] = '\n'; + separator[2] = '\t'; + separator[3] = '\0'; + separator[4] = '\0'; + break; + case SupportedLineEndingsEnum::SlashR: + separator[0] = ' '; + separator[1] = '\r'; + separator[2] = '\t'; + separator[3] = '\0'; + separator[4] = '\0'; + break; + case SupportedLineEndingsEnum::SlashRN: + separator[0] = ' '; + separator[1] = '\r'; + separator[2] = '\n'; + separator[3] = '\t'; + separator[4] = '\0'; + break; + } + bool foundDecl = false, foundEnd = false; uint_fast32_t proposition_count = 0; { @@ -160,7 +189,7 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f * parse node number, then iterate over propositions */ node = checked_strtol(buf, &buf); - while ((buf[0] != '\n') && (buf[0] != '\0')) { + while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { cnt = strcspn(buf, separator); if (cnt == 0) { /* @@ -168,7 +197,7 @@ storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_f * if it's a newline, we continue with next node * otherwise we skip it and try again */ - if (buf[0] == '\n') break; + if (buf[0] == '\n' || buf[0] == '\r') break; buf++; } else { /* diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 0a2107ff8..9b2ee51cd 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -44,15 +44,27 @@ namespace parser { * @param buf Data to scan. Is expected to be some char array. * @param maxnode Is set to highest id of all nodes. */ -uint_fast64_t firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { +uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { bool isRewardMatrix = rewardMatrixInformation != nullptr; uint_fast64_t nonZeroEntryCount = 0; + /* * Check file header and extract number of transitions. */ if (!isRewardMatrix) { - buf = strchr(buf, '\n') + 1; // skip format hint + // skip format hint + switch (lineEndings) { + case SupportedLineEndingsEnum::SlashN: + buf = strchr(buf, '\n') + 1; + break; + case SupportedLineEndingsEnum::SlashR: + buf = strchr(buf, '\r') + 1; + break; + case SupportedLineEndingsEnum::SlashRN: + buf = strchr(buf, '\r') + 2; + break; + } } /* @@ -129,7 +141,7 @@ uint_fast64_t firstPass(char* buf, uint_fast64_t& maxnode, RewardMatrixInformati * @return a pointer to the created sparse matrix. */ -storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) { +storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const& filename, bool insertDiagonalEntriesIfMissing, RewardMatrixInformationStruct* rewardMatrixInformation) { /* * Enforce locale where decimal point is '.'. */ @@ -142,6 +154,11 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process."; } + /* + * Find out about the used line endings. + */ + SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + /* * Open file. */ @@ -152,7 +169,7 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st * Perform first pass, i.e. count entries that are not zero. */ uint_fast64_t maxStateId; - uint_fast64_t nonZeroEntryCount = firstPass(file.data, maxStateId, rewardMatrixInformation); + uint_fast64_t nonZeroEntryCount = firstPass(file.data, lineEndings, maxStateId, rewardMatrixInformation); LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << nonZeroEntryCount << " NonZeros."); @@ -174,7 +191,18 @@ storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::st * Read file header, extract number of states. */ if (!isRewardMatrix) { - buf = strchr(buf, '\n') + 1; // skip format hint + // skip format hint + switch (lineEndings) { + case SupportedLineEndingsEnum::SlashN: + buf = strchr(buf, '\n') + 1; + break; + case SupportedLineEndingsEnum::SlashR: + buf = strchr(buf, '\r') + 1; + break; + case SupportedLineEndingsEnum::SlashRN: + buf = strchr(buf, '\r') + 2; + break; + } } // If the matrix that is being parsed is a reward matrix, it should match the size of the diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 7ea82b410..cca8bf9e0 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -15,7 +15,7 @@ namespace parser { * @brief Load a deterministic transition system from file and create a * sparse adjacency matrix whose entries represent the weights of the edges */ -storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); +storm::storage::SparseMatrix DeterministicSparseTransitionParser(std::string const& filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); } // namespace parser } // namespace storm diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 5d40e0cca..2ff9eade5 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -49,14 +49,25 @@ namespace parser { * @param maxnode Is set to highest id of all nodes. * @return The number of non-zero elements. */ -uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { +uint_fast64_t firstPass(char* buf, SupportedLineEndingsEnum lineEndings, uint_fast64_t& choices, int_fast64_t& maxnode, RewardMatrixInformationStruct* rewardMatrixInformation) { bool isRewardFile = rewardMatrixInformation != nullptr; /* * Check file header and extract number of transitions. */ if (!isRewardFile) { - buf = strchr(buf, '\n') + 1; // skip format hint + // skip format hint + switch (lineEndings) { + case SupportedLineEndingsEnum::SlashN: + buf = strchr(buf, '\n') + 1; + break; + case SupportedLineEndingsEnum::SlashR: + buf = strchr(buf, '\r') + 1; + break; + case SupportedLineEndingsEnum::SlashRN: + buf = strchr(buf, '\r') + 2; + break; + } } /* @@ -149,7 +160,17 @@ uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode /* * Proceed to beginning of next line. */ - buf += strcspn(buf, " \t\n\r"); + switch (lineEndings) { + case SupportedLineEndingsEnum::SlashN: + buf += strcspn(buf, " \t\n"); + break; + case SupportedLineEndingsEnum::SlashR: + buf += strcspn(buf, " \t\r"); + break; + case SupportedLineEndingsEnum::SlashRN: + buf += strcspn(buf, " \t\r\n"); + break; + } buf = trimWhitespaces(buf); } @@ -190,6 +211,11 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP bool isRewardFile = rewardMatrixInformation != nullptr; + /* + * Find out about the used line endings. + */ + SupportedLineEndingsEnum lineEndings = findUsedLineEndings(filename, true); + /* * Open file. */ @@ -201,7 +227,7 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP */ int_fast64_t maxnode; uint_fast64_t choices; - uint_fast64_t nonzero = firstPass(file.data, choices, maxnode, rewardMatrixInformation); + uint_fast64_t nonzero = firstPass(file.data, lineEndings, choices, maxnode, rewardMatrixInformation); /* * If first pass returned zero, the file format was wrong. @@ -221,7 +247,18 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP * Skip file header. */ if (!isRewardFile) { - buf = strchr(buf, '\n') + 1; // skip format hint + // skip format hint + switch (lineEndings) { + case SupportedLineEndingsEnum::SlashN: + buf = strchr(buf, '\n') + 1; + break; + case SupportedLineEndingsEnum::SlashR: + buf = strchr(buf, '\r') + 1; + break; + case SupportedLineEndingsEnum::SlashRN: + buf = strchr(buf, '\r') + 2; + break; + } } if (isRewardFile) { @@ -338,7 +375,17 @@ NondeterministicSparseTransitionParserResult_t NondeterministicSparseTransitionP if (buf[0] == ' ') { ++buf; } - buf += strcspn(buf, " \t\n\r"); + switch (lineEndings) { + case SupportedLineEndingsEnum::SlashN: + buf += strcspn(buf, " \t\n"); + break; + case SupportedLineEndingsEnum::SlashR: + buf += strcspn(buf, " \t\r"); + break; + case SupportedLineEndingsEnum::SlashRN: + buf += strcspn(buf, " \t\r\n"); + break; + } buf = trimWhitespaces(buf); } diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp index 7f40d508c..dbc2849c5 100644 --- a/src/parser/Parser.cpp +++ b/src/parser/Parser.cpp @@ -72,9 +72,7 @@ char* storm::parser::trimWhitespaces(char* buf) { /*! * @briefs Analyzes the given file and tries to find out the used file endings. */ -storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::string const& fileName) { - storm::parser::SupportedLineEndingsEnum result = storm::parser::SupportedLineEndingsEnum::Unsupported; - +storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) { MappedFile fileMap(fileName.c_str()); char* buf = nullptr; char* const bufferEnd = fileMap.dataend; @@ -91,6 +89,13 @@ storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std:: return storm::parser::SupportedLineEndingsEnum::SlashN; } } + + if (throwOnUnsupported) { + LOG4CPLUS_ERROR(logger, "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n"); + throw storm::exceptions::WrongFormatException() << "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n"; + } + LOG4CPLUS_WARN(logger, "Error while parsing \"" << fileName << "\": Unsupported or unknown line-endings. Please use either of \\r, \\n or \\r\\n"); + return storm::parser::SupportedLineEndingsEnum::Unsupported; } diff --git a/src/parser/Parser.h b/src/parser/Parser.h index b86f7c56e..62dc75d1f 100644 --- a/src/parser/Parser.h +++ b/src/parser/Parser.h @@ -148,7 +148,7 @@ namespace parser { /*! * @briefs Analyzes the given file and tries to find out the used line endings. */ - storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName); + storm::parser::SupportedLineEndingsEnum findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported = false); } // namespace parser } // namespace storm