diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 427d64ba9..c0a058381 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -6,193 +6,164 @@ */ #include "src/parser/AtomicPropositionLabelingParser.h" +#include "src/parser/Parser.h" -#include -#include -#include -#include -#include - -#include -#include #include #include -#include #include #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" -#include "src/utility/OsDetection.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; namespace storm { -namespace parser { + namespace parser { + storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t node_count, std::string const & filename) { -/*! - * Reads a label file and puts the result in a labeling structure. - * - * Labelings created with this method have to be freed with the delete operator. - * @param node_count the number of states. - * @param filename input .lab file's name. - * @return The pointer to the created labeling object. - */ -storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const & filename) { - /* - * Open file. - */ - if (!storm::parser::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 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[5];// = " \r\n\t"; - storm::parser::getMatchingSeparatorString(separator, sizeof(separator), lineEndings); - - bool foundDecl = false, foundEnd = false; - uint_fast32_t proposition_count = 0; - { - size_t cnt = 0; - /* - * Iterate over tokens until we hit #END or end of file. - */ - while(buf[0] != '\0') { - buf += cnt; - cnt = strcspn(buf, separator); // position of next separator - if (cnt > 0) { - /* - * next token is #DECLARATION: just skip it - * next token is #END: stop search - * otherwise increase proposition_count - */ - if (strncmp(buf, "#DECLARATION", cnt) == 0) { - foundDecl = true; - continue; - } else if (strncmp(buf, "#END", cnt) == 0) { - foundEnd = true; - break; + // Open the given file. + if (!storm::parser::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 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 pass: Count the number of propositions. + // Convert the line endings into a string containing all whitespace characters, that separate words in the file. + char separator[5]; + storm::parser::getMatchingSeparatorString(separator, sizeof(separator), lineEndings); + + bool foundDecl = false, foundEnd = false; + uint_fast32_t proposition_count = 0; + size_t cnt = 0; + + // Iterate over tokens until we hit #END or the end of the file. + while(buf[0] != '\0') { + + // Move the buffer pointer to the separator. + buf += cnt; + + // Get the number of characters until the next separator. + cnt = strcspn(buf, separator); + if (cnt > 0) { + + // If the next token is #DECLARATION: Just skip it. + // If the next token is #END: Stop the search. + // Otherwise increase proposition_count. + if (strncmp(buf, "#DECLARATION", cnt) == 0) { + foundDecl = true; + continue; + } else if (strncmp(buf, "#END", cnt) == 0) { + foundEnd = true; + break; + } + proposition_count++; + } else { + + // If the next character is a separator, skip it. + buf++; } - proposition_count++; - } else { - buf++; // next char is separator, one step forward } - } - /* - * If #DECLARATION or #END were not found, the file format is wrong - */ - if (!(foundDecl && foundEnd)) { - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted."); - if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token."); - if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token."); - throw storm::exceptions::WrongFormatException(); - } - } - - /* - * create labeling object with given node and proposition count - */ - storm::models::AtomicPropositionsLabeling labeling(node_count, proposition_count); - - /* - * second run: add propositions and node labels to labeling - * - * first thing to do: reset file pointer - */ - buf = file.data; - { - /* - * load propositions - * As we already checked the file format, we can be a bit sloppy here... - */ - char proposition[128]; // buffer for proposition names - size_t cnt = 0; - do { - buf += cnt; - cnt = strcspn(buf, separator); // position of next separator - if (cnt >= sizeof(proposition)) { - /* - * if token is longer than our buffer, the following strncpy code might get risky... - */ - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found."); + // If #DECLARATION or #END have not been found, the file format is wrong. + if (!(foundDecl && foundEnd)) { + LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). File header is corrupted."); + if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token."); + if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token."); throw storm::exceptions::WrongFormatException(); - } else if (cnt > 0) { - /* - * next token is: #DECLARATION: just skip it - * next token is: #END: stop search - * otherwise: copy token to buffer, append trailing null byte and hand it to labeling - */ - if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; - if (strncmp(buf, "#END", cnt) == 0) break; - strncpy(proposition, buf, cnt); - proposition[cnt] = '\0'; - labeling.addAtomicProposition(proposition); - } else { - cnt = 1; // next char is separator, one step forward } - } while (cnt > 0); - /* - * Right here, the buf pointer is still pointing to our last token, - * i.e. to #END. We want to skip this one... - */ - buf += 4; - } - - { - /* - * now parse node label assignments - */ - uint_fast64_t node; - char proposition[128]; - size_t cnt; - /* - * iterate over nodes - */ - while (buf[0] != '\0') { - /* - * parse node number, then iterate over propositions - */ - node = checked_strtol(buf, &buf); - while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { + + + // Create labeling object with given node and proposition count. + storm::models::AtomicPropositionsLabeling labeling(node_count, proposition_count); + + // Second pass: Add propositions and node labels to labeling. + // First thing to do: Reset the file pointer. + buf = file.data; + + // Prepare a buffer for proposition names. + char proposition[128]; + cnt = 0; + + // Parse proposition names. + // As we already checked the file header, we know that #DECLARATION and #END are tokens in the character stream. + while(buf[0] != '\0') { + + // Move the buffer pointer to the separator. + buf += cnt; + + // The number of characters until the next separator. cnt = strcspn(buf, separator); - if (cnt == 0) { - /* - * next char is a separator - * if it's a newline, we continue with next node - * otherwise we skip it and try again - */ - if (buf[0] == '\n' || buf[0] == '\r') break; - buf++; - } else { - /* - * copy proposition to buffer and add it to labeling - */ + + if (cnt >= sizeof(proposition)) { + + // if token is longer than our buffer, the following strncpy code might get risky... + LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found."); + throw storm::exceptions::WrongFormatException(); + + } else if (cnt > 0) { + + // If the next token is #DECLARATION: Just skip it. + if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; + + // If the next token is #END: Stop the search. + if (strncmp(buf, "#END", cnt) == 0) break; + + // Otherwise copy the token to the buffer, append a trailing null byte and hand it to labeling. strncpy(proposition, buf, cnt); proposition[cnt] = '\0'; - labeling.addAtomicPropositionToState(proposition, node); - buf += cnt; + labeling.addAtomicProposition(proposition); + } else { + + // The next character is a separator, thus move one step forward. + buf++; } } - buf = storm::parser::trimWhitespaces(buf); + + // At this point, the pointer buf is still pointing to our last token, i.e. to #END. + // We want to skip it. + buf += 4; + + uint_fast64_t node; + cnt = 0; + + // Now parse the assignments of labels to nodes. + while (buf[0] != '\0') { + + // Parse the node number and iterate over its labels (atomic propositions). + // Stop at the end of the line. + node = checked_strtol(buf, &buf); + while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { + cnt = strcspn(buf, separator); + if (cnt == 0) { + + // The next character is a separator. + // If it is a line separator, we continue with next node. + // Otherwise, we skip it and try again. + if (buf[0] == '\n' || buf[0] == '\r') break; + buf++; + } else { + + // Copy the label to the buffer, null terminate it and add it to labeling. + strncpy(proposition, buf, cnt); + proposition[cnt] = '\0'; + labeling.addAtomicPropositionToState(proposition, node); + buf += cnt; + } + } + buf = trimWhitespaces(buf); + } + + return labeling; } - } - - return labeling; -} -} // namespace parser + } // namespace parser } // namespace storm diff --git a/src/parser/AtomicPropositionLabelingParser.h b/src/parser/AtomicPropositionLabelingParser.h index 578b1d9ae..976dd9f35 100644 --- a/src/parser/AtomicPropositionLabelingParser.h +++ b/src/parser/AtomicPropositionLabelingParser.h @@ -1,23 +1,28 @@ -#ifndef STORM_PARSER_LABPARSER_H_ -#define STORM_PARSER_LABPARSER_H_ +#ifndef STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_ +#define STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_ #include "src/models/AtomicPropositionsLabeling.h" #include -#include "src/parser/Parser.h" +namespace storm { + namespace parser { -#include + class AtomicPropositionLabelingParser { -namespace storm { -namespace parser { + public: + + /* + * Reads a label file and puts the result in an AtomicPropositionsLabeling object. + * + * @param node_count The number of states of the model to be labeled. + * @param filename The path and name of the labeling (.lab) file. + * @return The parsed labeling as an AtomicPropositionsLabeling object. + */ + static storm::models::AtomicPropositionsLabeling parseAtomicPropositionLabeling(uint_fast64_t node_count, std::string const &filename); -/*! - * @brief Load label file and return initialized AtomicPropositionsLabeling object. - * - */ -storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename); + }; -} // namespace parser + } // namespace parser } // namespace storm -#endif /* STORM_PARSER_LABPARSER_H_ */ +#endif /* STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_ */ diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 3f25b9c0c..ca841396a 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -33,7 +33,7 @@ DeterministicModelParser::Result DeterministicModelParser::parseDeterministicMod uint_fast64_t stateCount = resultTransitionSystem.getColumnCount(); uint_fast64_t rowCount = resultTransitionSystem.getRowCount(); - storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); + storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile))); DeterministicModelParser::Result result(std::move(resultTransitionSystem), std::move(labeling)); diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index b9bb1621e..004210aa1 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -1,5 +1,5 @@ -#ifndef STORM_PARSER_TRAPARSER_H_ -#define STORM_PARSER_TRAPARSER_H_ +#ifndef STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ +#define STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ #include "src/storage/SparseMatrix.h" #include "src/parser/Parser.h" @@ -82,4 +82,4 @@ private: } // namespace storm -#endif /* STORM_PARSER_TRAPARSER_H_ */ +#endif /* STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ */ diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp index cf98ded11..172d71ecd 100644 --- a/src/parser/MarkovAutomatonParser.cpp +++ b/src/parser/MarkovAutomatonParser.cpp @@ -16,7 +16,7 @@ storm::models::MarkovAutomaton MarkovAutomatonParser::parseMarkovAutomat storm::storage::SparseMatrix transitionMatrix(transitionResult.transitionMatrixBuilder.build(0,0)); // Parse the state labeling. - storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser(transitionMatrix.getColumnCount(), labelingFilename)); + storm::models::AtomicPropositionsLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename)); // If given, parse the state rewards file. boost::optional> stateRewards; diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index fd2e85912..528f62f51 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -35,7 +35,7 @@ namespace storm { uint_fast64_t stateCount = transitions.getColumnCount(); uint_fast64_t rowCount = transitions.getRowCount(); - storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser(stateCount, labelingFile))); + storm::models::AtomicPropositionsLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFile))); Result result(std::move(transitions), std::move(transitionParserResult.rowMapping), std::move(labeling)); diff --git a/test/functional/parser/ReadLabFileTest.cpp b/test/functional/parser/ReadLabFileTest.cpp index 2e35ee1ae..8c0a31b89 100644 --- a/test/functional/parser/ReadLabFileTest.cpp +++ b/test/functional/parser/ReadLabFileTest.cpp @@ -16,14 +16,14 @@ TEST(ReadLabFileTest, NonExistingFileTest) { // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(0,STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(0,STORM_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), storm::exceptions::FileIoException); } TEST(ReadLabFileTest, ParseTest) { // This test is based on a test case from the original MRMC. // Parsing the file - storm::models::AtomicPropositionsLabeling labeling = storm::parser::AtomicPropositionLabelingParser(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"); + storm::models::AtomicPropositionsLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(12, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/pctl_general_input_01.lab"); // Checking whether all propositions are in the labelling @@ -79,14 +79,14 @@ TEST(ReadLabFileTest, ParseTest) { } TEST(ReadLabFileTest, WrongHeaderTest1) { - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header1.lab"), storm::exceptions::WrongFormatException); } TEST(ReadLabFileTest, WrongHeaderTest2) { - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_header2.lab"), storm::exceptions::WrongFormatException); } TEST(ReadLabFileTest, WrongPropositionTest) { - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/wrong_format_proposition.lab"), storm::exceptions::WrongFormatException); }