diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index aaca0d7a3..ad5543476 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -11,7 +11,7 @@ #include #include -#include "src/parser/Parser.h" +#include "src/utility/cstring.h" #include "src/parser/MappedFile.h" #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" @@ -23,25 +23,20 @@ extern log4cplus::Logger logger; namespace storm { namespace parser { + using namespace storm::utility::cstring; + storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t node_count, std::string const & filename) { // Open the given file. - if (!storm::parser::fileExistsAndIsReadable(filename.c_str())) { + if (!MappedFile::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. - SupportedLineEndings 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; @@ -49,11 +44,12 @@ namespace storm { // Iterate over tokens until we hit #END or the end of the file. while(buf[0] != '\0') { - // Move the buffer pointer to the separator. + //Move the buffer to the beginning of the next word. buf += cnt; + buf = trimWhitespaces(buf); // Get the number of characters until the next separator. - cnt = strcspn(buf, separator); + cnt = skipWord(buf) - buf; if (cnt > 0) { // If the next token is #DECLARATION: Just skip it. @@ -67,10 +63,6 @@ namespace storm { break; } proposition_count++; - } else { - - // If the next character is a separator, skip it. - buf++; } } @@ -98,11 +90,12 @@ namespace storm { // 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. + //Move the buffer to the beginning of the next word. buf += cnt; + buf = trimWhitespaces(buf); - // The number of characters until the next separator. - cnt = strcspn(buf, separator); + // Get the number of characters until the next separator. + cnt = skipWord(buf) - buf; if (cnt >= sizeof(proposition)) { @@ -122,10 +115,6 @@ namespace storm { strncpy(proposition, buf, cnt); proposition[cnt] = '\0'; labeling.addAtomicProposition(proposition); - } else { - - // The next character is a separator, thus move one step forward. - buf++; } } @@ -143,7 +132,7 @@ namespace storm { // 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); + cnt = skipWord(buf) - buf; if (cnt == 0) { // The next character is a separator. diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 91e28c9d2..d9d6bcfa5 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -7,7 +7,6 @@ #include "src/parser/AutoParser.h" -#include "src/parser/Parser.h" #include "src/parser/MappedFile.h" #include "src/parser/DeterministicModelParser.h" @@ -15,9 +14,14 @@ #include "src/parser/MarkovAutomatonParser.h" #include "src/exceptions/WrongFormatException.h" +#include "src/utility/cstring.h" +#include "src/utility/OsDetection.h" + namespace storm { namespace parser { + using namespace storm::utility::cstring; + std::shared_ptr> AutoParser::parseModel(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, @@ -68,17 +72,18 @@ namespace storm { storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) { storm::models::ModelType hintType = storm::models::Unknown; - // Find out the line endings used within the file. - storm::parser::SupportedLineEndings lineEndings = storm::parser::findUsedLineEndings(filename); - // Open the file. MappedFile file(filename.c_str()); char* buf = file.data; // Find and read in the hint. - char hint[128]; - // %20s => The input hint can be AT MOST 120 chars long. - storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings); + char hint[65]; + // %60s => The input hint can be AT MOST 60 chars long. + #ifdef WINDOWS + sscanf_s(buf, "%60s", hint, sizeof(hint)); + #else + sscanf(buf, "%60s", hint); + #endif for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 2e52fad59..88df0d076 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -6,6 +6,14 @@ #include namespace storm { + + /*! + * @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). + */ namespace parser { class AutoParser { diff --git a/src/parser/CslParser.h b/src/parser/CslParser.h index 8dd4315d3..2ef4c64e3 100644 --- a/src/parser/CslParser.h +++ b/src/parser/CslParser.h @@ -8,8 +8,6 @@ #ifndef STORM_PARSER_CSLPARSER_H_ #define STORM_PARSER_CSLPARSER_H_ -#include "Parser.h" - #include "src/formula/Csl.h" #include diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h index 3fc840c5e..2143ea820 100644 --- a/src/parser/DeterministicModelParser.h +++ b/src/parser/DeterministicModelParser.h @@ -8,7 +8,6 @@ #ifndef STORM_PARSER_DETERMINISTICMODELPARSER_H_ #define STORM_PARSER_DETERMINISTICMODELPARSER_H_ -#include "src/parser/Parser.h" #include "src/models/Dtmc.h" #include "src/models/Ctmc.h" diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 666a45039..a127ebde0 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -15,6 +15,7 @@ #include #include "src/utility/constants.h" +#include "src/utility/cstring.h" #include "src/parser/MappedFile.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" @@ -27,6 +28,8 @@ extern log4cplus::Logger logger; namespace storm { namespace parser { + using namespace storm::utility::cstring; + storm::storage::SparseMatrix DeterministicSparseTransitionParser::parseDeterministicTransitions(std::string const& filename) { storm::storage::SparseMatrix emptyMatrix; @@ -43,21 +46,18 @@ namespace storm { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); - if (!fileExistsAndIsReadable(filename.c_str())) { + if (!MappedFile::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."; } - // Find out about the used line endings. - SupportedLineEndings lineEndings = findUsedLineEndings(filename, true); - // Open file. MappedFile file(filename.c_str()); char* buf = file.data; // Perform first pass, i.e. count entries that are not zero. bool insertDiagonalEntriesIfMissing = !isRewardFile; - DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, lineEndings, insertDiagonalEntriesIfMissing); + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.data, insertDiagonalEntriesIfMissing); LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros."); @@ -72,7 +72,8 @@ namespace storm { // Skip the format hint if it is there. buf = trimWhitespaces(buf); if(buf[0] < '0' || buf[0] > '9') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); } if(isRewardFile) { @@ -191,14 +192,15 @@ namespace storm { return resultMatrix.build(); } - DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings, bool insertDiagonalEntriesIfMissing) { + DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, bool insertDiagonalEntriesIfMissing) { DeterministicSparseTransitionParser::FirstPassResult result; // Skip the format hint if it is there. buf = trimWhitespaces(buf); if(buf[0] < '0' || buf[0] > '9') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); } // Check all transitions for non-zero diagonal entries and deadlock states. diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index a9147f763..d89490bee 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -2,7 +2,6 @@ #define STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ #include "src/storage/SparseMatrix.h" -#include "src/parser/Parser.h" namespace storm { @@ -59,11 +58,10 @@ private: * transitions and the maximum node id. * * @param buffer The buffer that cointains the input. - * @param lineEndings The line endings that are to be used while parsing. * @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, SupportedLineEndings lineEndings, bool insertDiagonalEntriesIfMissing = true); + static FirstPassResult firstPass(char* buffer, bool insertDiagonalEntriesIfMissing = true); /* * The main parsing routine. diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h index 20e82896b..cefcd8f2c 100644 --- a/src/parser/LtlParser.h +++ b/src/parser/LtlParser.h @@ -8,7 +8,6 @@ #ifndef STORM_PARSER_LTLPARSER_H_ #define STORM_PARSER_LTLPARSER_H_ -#include "Parser.h" #include "src/formula/Ltl.h" namespace storm { diff --git a/src/parser/MappedFile.cpp b/src/parser/MappedFile.cpp index 69d9fd4a9..c1c654aa7 100644 --- a/src/parser/MappedFile.cpp +++ b/src/parser/MappedFile.cpp @@ -11,9 +11,6 @@ #include #include -#include -#include - #include #include "src/exceptions/FileIoException.h" @@ -96,6 +93,11 @@ namespace storm { CloseHandle(this->file); #endif } + + bool MappedFile::fileExistsAndIsReadable(const char* fileName) { + std::ifstream fin(fileName); + return fin.good(); + } } // namespace parser } // namespace storm diff --git a/src/parser/MappedFile.h b/src/parser/MappedFile.h index 8b66b0fde..da2df3c3d 100644 --- a/src/parser/MappedFile.h +++ b/src/parser/MappedFile.h @@ -48,6 +48,12 @@ namespace storm { */ ~MappedFile(); + /*! + * @brief Tests whether the given file exists and is readable. + * @return True iff the file exists and is readable. + */ + static bool fileExistsAndIsReadable(const char* fileName); + /*! * @brief pointer to actual file content. */ diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index de950aab8..a899632a4 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -2,13 +2,17 @@ #include "src/settings/Settings.h" #include "src/exceptions/WrongFormatException.h" -#include "MappedFile.h" +#include "src/parser/MappedFile.h" +#include "src/utility/cstring.h" + namespace storm { namespace parser { -MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings) { +using namespace storm::utility::cstring; + +MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -16,7 +20,8 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran // Skip the format hint if it is there. buf = trimWhitespaces(buf); if(buf[0] < '0' || buf[0] > '9') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); } // Now read the transitions. @@ -84,7 +89,8 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran stateHasProbabilisticChoice = true; } - buf = forwardToNextLine(buf, lineEndings); + // Go to the next line where the transitions start. + buf = forwardToNextLine(buf); // Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates. bool hasSuccessorState = false; @@ -131,7 +137,7 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran // As we found a new successor, we need to increase the number of nonzero entries. ++result.numberOfNonzeroEntries; - buf = forwardToNextLine(buf, lineEndings); + buf = forwardToNextLine(buf); } else { // If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer // to the buffer, because we still need to read the new source state. @@ -143,13 +149,17 @@ MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTran return result; } -MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, SupportedLineEndings lineEndings, FirstPassResult const& firstPassResult) { +MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitionParser::secondPass(char* buf, FirstPassResult const& firstPassResult) { ResultType result(firstPassResult); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); - // Skip the format hint. - buf = storm::parser::forwardToNextLine(buf, lineEndings); + // Skip the format hint if it is there. + buf = trimWhitespaces(buf); + if(buf[0] < '0' || buf[0] > '9') { + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); + } // Now read the transitions. uint_fast64_t source, target = 0; @@ -195,7 +205,8 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio isMarkovianChoice = false; } - buf = forwardToNextLine(buf, lineEndings); + // Go to the next line where the transitions start. + buf = forwardToNextLine(buf); // Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates. bool encounteredNewDistribution = false; @@ -226,7 +237,7 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio result.exitRates[source] += val; } - buf = forwardToNextLine(buf, lineEndings); + buf = forwardToNextLine(buf); } else { // If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer // to the buffer, because we still need to read the new source state. @@ -247,19 +258,16 @@ MarkovAutomatonSparseTransitionParser::ResultType MarkovAutomatonSparseTransitio // Set the locale to correctly recognize floating point numbers. setlocale(LC_NUMERIC, "C"); - if (!fileExistsAndIsReadable(filename.c_str())) { + if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File does not exist or is not readable."; } - // Determine used line endings. - SupportedLineEndings lineEndings = findUsedLineEndings(filename, true); - // Open file and prepare pointer to buffer. MappedFile file(filename.c_str()); char* buf = file.data; - return secondPass(buf, lineEndings, firstPass(buf, lineEndings)); + return secondPass(buf, firstPass(buf)); } } // namespace parser diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 25f9291dc..954f21a63 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -3,7 +3,6 @@ #include "src/storage/SparseMatrix.h" #include "src/storage/BitVector.h" -#include "Parser.h" namespace storm { @@ -77,20 +76,18 @@ private: * Performs the first pass on the input pointed to by the given buffer. * * @param buffer The buffer that cointains the input. - * @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, SupportedLineEndings lineEndings); + static FirstPassResult firstPass(char* buffer); /* * Performs the second pass on the input pointed to by the given buffer with the information of the first pass. * * @param buffer The buffer that cointains the input. - * @param lineEndings The line endings that are to be used while parsing. * @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, SupportedLineEndings lineEndings, FirstPassResult const& firstPassResult); + static ResultType secondPass(char* buffer, FirstPassResult const& firstPassResult); }; } // namespace parser diff --git a/src/parser/NondeterministicModelParser.h b/src/parser/NondeterministicModelParser.h index 6719a4585..50a0525fb 100644 --- a/src/parser/NondeterministicModelParser.h +++ b/src/parser/NondeterministicModelParser.h @@ -8,7 +8,6 @@ #ifndef STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ #define STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ -#include "src/parser/Parser.h" #include "src/models/Mdp.h" #include "src/models/Ctmdp.h" diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 3c7ebbaab..6e7c72246 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -14,6 +14,8 @@ #include "src/exceptions/FileIoException.h" #include "src/exceptions/WrongFormatException.h" +#include "src/utility/cstring.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -21,6 +23,8 @@ extern log4cplus::Logger logger; namespace storm { namespace parser { + using namespace storm::utility::cstring; + NondeterministicSparseTransitionParser::Result NondeterministicSparseTransitionParser::parseNondeterministicTransitions(std::string const& filename) { Result emptyResult; @@ -38,20 +42,17 @@ namespace storm { // Enforce locale where decimal point is '.'. setlocale(LC_NUMERIC, "C"); - if (!fileExistsAndIsReadable(filename.c_str())) { + if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); throw storm::exceptions::WrongFormatException(); } - // Find out about the used line endings. - 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, modelInformation); + NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.data, isRewardFile, modelInformation); // If first pass returned zero, the file format was wrong. if (firstPass.numberOfNonzeroEntries == 0) { @@ -64,7 +65,8 @@ namespace storm { // Skip the format hint if it is there. buf = trimWhitespaces(buf); if(buf[0] < '0' || buf[0] > '9') { - buf = storm::parser::forwardToNextLine(buf, lineEndings); + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); } if (isRewardFile) { @@ -158,7 +160,7 @@ namespace storm { lastchoice = choice; // Proceed to beginning of next line in file and next row in matrix. - buf = forwardToLineEnd(buf, lineEndings); + buf = forwardToLineEnd(buf); buf = trimWhitespaces(buf); } @@ -172,14 +174,15 @@ namespace storm { return NondeterministicSparseTransitionParser::Result(matrixBuilder.build(), rowMapping); } - NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, SupportedLineEndings lineEndings, bool isRewardFile, Result const & modelInformation) { + NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, 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); + buf = forwardToLineEnd(buf); + buf = trimWhitespaces(buf); } // Read all transitions. @@ -261,7 +264,7 @@ namespace storm { // 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 = forwardToLineEnd(buf); buf = trimWhitespaces(buf); } diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index 3df4834ae..d754a39c3 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -1,7 +1,6 @@ #ifndef STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H_ #define STORM_PARSER_NONDETERMINISTICSPARSETRANSITIONPARSER_H_ -#include "src/parser/Parser.h" #include "src/storage/SparseMatrix.h" #include @@ -87,11 +86,10 @@ namespace storm { * number of columns of the matrix. * * @param buffer Buffer containing the data to scan. This is expected to be some char array. - * @param lineEndings The line endings that are to be used while parsing. * @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, SupportedLineEndings lineEndings, bool isRewardFile, Result const & modelInformation); + static FirstPassResult firstPass(char* buffer, bool isRewardFile, Result const & modelInformation); /*! * The main parsing routine. diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp deleted file mode 100644 index 9e4113445..000000000 --- a/src/parser/Parser.cpp +++ /dev/null @@ -1,253 +0,0 @@ -#include "src/parser/Parser.h" - -#include -#include -#include -#include -#include -#include - -#include -#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" -extern log4cplus::Logger logger; - -namespace storm { - -namespace parser { - -/*! - * Calls strtol() internally and checks if the new pointer is different - * from the original one, i.e. if str != *end. If they are the same, a - * storm::exceptions::WrongFormatException will be thrown. - * @param str String to parse - * @param end New pointer will be written there - * @return Result of strtol() - */ -uint_fast64_t checked_strtol(const char* str, char** end) { - uint_fast64_t res = strtol(str, end, 10); - if (str == *end) { - LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number."); - LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\""); - throw storm::exceptions::WrongFormatException("Error while parsing integer. Next input token is not a number."); - } - return res; -} - -/*! - * Calls strtod() internally and checks if the new pointer is different - * from the original one, i.e. if str != *end. If they are the same, a - * storm::exceptions::WrongFormatException will be thrown. - * @param str String to parse - * @param end New pointer will be written there - * @return Result of strtod() - */ -double checked_strtod(const char* str, char** end) { - double res = strtod(str, end); - if (str == *end) { - LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number."); - LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\""); - throw storm::exceptions::WrongFormatException("Error while parsing floating point. Next input token is not a number."); - } - return res; -} - -/*! - * @brief Tests whether the given file exists and is readable. - * @return True iff the file exists and is readable. - */ -bool fileExistsAndIsReadable(const char* fileName) { - std::ifstream fin(fileName); - bool returnValue = !fin.fail(); - return returnValue; -} - -/*! - * Skips all numbers, letters and special characters. - * Returns a pointer to the first char that is a whitespace. - * @param buf The string buffer to operate on. - * @return A pointer to the first whitespace character. - */ -char* skipWord(char* buf){ - while((*buf != ' ') && (*buf != '\t') && (*buf != '\n') && (*buf != '\r')) buf++; - return buf; -} - -/*! - * Skips spaces, tabs, newlines and carriage returns. Returns a pointer - * to first char that is not a whitespace. - * @param buf The string buffer to operate on. - * @return A pointer to the first non-whitespace character. - */ -char* trimWhitespaces(char* buf) { - while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++; - return buf; -} - -/*! - * @briefs Analyzes the given file and tries to find out the used file endings. - */ -SupportedLineEndings findUsedLineEndings(std::string const& fileName, bool throwOnUnsupported) { - MappedFile fileMap(fileName.c_str()); - char* buf = nullptr; - char* const bufferEnd = fileMap.dataend; - - for (buf = fileMap.data; buf != bufferEnd; ++buf) { - if (*buf == '\r') { - // check for following \n - if (((buf + sizeof(char)) < bufferEnd) && (*(buf + sizeof(char)) == '\n')) { - return SupportedLineEndings::SlashRN; - } - return SupportedLineEndings::SlashR; - } else if (*buf == '\n') { - return SupportedLineEndings::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 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, SupportedLineEndings lineEndings) { - switch (lineEndings) { - case SupportedLineEndings::SlashN: - return buffer + strcspn(buffer, "\n\0"); - break; - case SupportedLineEndings::SlashR: - return buffer + strcspn(buffer, "\r\0"); - break; - case SupportedLineEndings::SlashRN: - return buffer + strcspn(buffer, "\r\0"); - break; - default: - case SupportedLineEndings::Unsupported: - // This Line will never be reached as the Parser would have thrown already. - throw; - break; - } - return nullptr; -} - -/*! - * @brief Encapsulates the usage of function @strchr to forward to the next line - */ -char* forwardToNextLine(char* buffer, SupportedLineEndings lineEndings) { - switch (lineEndings) { - case SupportedLineEndings::SlashN: - return strchr(buffer, '\n') + 1; - break; - case SupportedLineEndings::SlashR: - return strchr(buffer, '\r') + 1; - break; - case SupportedLineEndings::SlashRN: - return strchr(buffer, '\r') + 2; - break; - default: - case SupportedLineEndings::Unsupported: - // This Line will never be reached as the Parser would have thrown already. - throw; - break; - } - return nullptr; -} - -/*! - * @brief Encapsulates the usage of function @sscanf to scan for the model type hint - * @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, SupportedLineEndings lineEndings) { - if (targetBufferSize <= 4) { - throw; - } - switch (lineEndings) { - case SupportedLineEndings::SlashN: -#ifdef WINDOWS - sscanf_s(buffer, "%60s\n", targetBuffer, targetBufferSize); -#else - sscanf(buffer, "%60s\n", targetBuffer); -#endif - break; - case SupportedLineEndings::SlashR: -#ifdef WINDOWS - sscanf_s(buffer, "%60s\r", targetBuffer, sizeof(targetBufferSize)); -#else - sscanf(buffer, "%60s\r", targetBuffer); -#endif - break; - case SupportedLineEndings::SlashRN: -#ifdef WINDOWS - sscanf_s(buffer, "%60s\r\n", targetBuffer, sizeof(targetBufferSize)); -#else - sscanf(buffer, "%60s\r\n", targetBuffer); -#endif - break; - default: - case SupportedLineEndings::Unsupported: - // This Line will never be reached as the Parser would have thrown already. - throw; - break; - } -} - -/*! - * @brief Returns the matching Separator-String in the format of "BLANK\t\NEWLINESYMBOL(S)\0 - */ -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 SupportedLineEndings::SlashN: { - char source[] = " \n\t"; -#ifdef WINDOWS - strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); -#else - strncpy(targetBuffer, source, targetBufferSize); -#endif - break; - } - case SupportedLineEndings::SlashR: { - char source[] = " \r\t"; -#ifdef WINDOWS - strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); -#else - strncpy(targetBuffer, source, targetBufferSize); -#endif - break; - } - case SupportedLineEndings::SlashRN: { - char source[] = " \r\n\t"; -#ifdef WINDOWS - strncpy(targetBuffer, targetBufferSize, source, sizeof(source)); -#else - strncpy(targetBuffer, source, targetBufferSize); -#endif - break; - } - default: - 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; - break; - } -} - -} // namespace parser - -} // namespace storm diff --git a/src/parser/Parser.h b/src/parser/Parser.h deleted file mode 100644 index 962f699eb..000000000 --- a/src/parser/Parser.h +++ /dev/null @@ -1,93 +0,0 @@ -/* - * Parser.h - * - * Created on: 21.11.2012 - * Author: Gereon Kremer - */ - -#ifndef STORM_PARSER_PARSER_H_ -#define STORM_PARSER_PARSER_H_ - -#include "src/utility/OsDetection.h" - -#include -#include -#include - -namespace storm { - - /*! - * @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). - */ - namespace parser { - - /*! - * @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); - - /*! - * @brief Skips common whitespaces in a string. - */ - char* trimWhitespaces(char* buf); - - /*! - * @brief Tests whether the given file exists and is readable. - */ - bool fileExistsAndIsReadable(const char* fileName); - - /*! - * @brief Enum Class Type containing all supported file endings. - */ - enum class SupportedLineEndings : unsigned short { - Unsupported = 0, - SlashR, - SlashN, - SlashRN - }; - - /*! - * @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); - - /*! - * @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 Encapsulates the usage of function @strchr to forward to the next line - */ - char* forwardToNextLine(char* buffer, storm::parser::SupportedLineEndings lineEndings); - - /*! - * @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/PrctlParser.h b/src/parser/PrctlParser.h index 848d1de99..3ba8f1998 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -1,8 +1,6 @@ #ifndef STORM_PARSER_PRCTLPARSER_H_ #define STORM_PARSER_PRCTLPARSER_H_ -#include "src/parser/Parser.h" - #include "src/formula/Prctl.h" //#include diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index a0bd62ce3..c79e6f691 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -11,7 +11,7 @@ #include "src/exceptions/WrongFormatException.h" #include "src/exceptions/FileIoException.h" -#include "src/parser/Parser.h" +#include "src/utility/cstring.h" #include "src/parser/MappedFile.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -21,6 +21,8 @@ namespace storm { namespace parser { +using namespace storm::utility::cstring; + /*! * Reads a state reward file and puts the result in a state reward vector. * @@ -30,7 +32,7 @@ namespace parser { */ std::vector SparseStateRewardParser::parseSparseStateReward(uint_fast64_t stateCount, std::string const & filename) { // Open file. - if (!fileExistsAndIsReadable(filename.c_str())) { + if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable."); throw storm::exceptions::WrongFormatException(); } diff --git a/src/utility/cstring.cpp b/src/utility/cstring.cpp new file mode 100644 index 000000000..2267fdf62 --- /dev/null +++ b/src/utility/cstring.cpp @@ -0,0 +1,95 @@ +#include "src/utility/cstring.h" + +#include + +#include "src/exceptions/WrongFormatException.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +namespace storm { + +namespace utility { + +namespace cstring { + +/*! + * Calls strtol() internally and checks if the new pointer is different + * from the original one, i.e. if str != *end. If they are the same, a + * storm::exceptions::WrongFormatException will be thrown. + * @param str String to parse + * @param end New pointer will be written there + * @return Result of strtol() + */ +uint_fast64_t checked_strtol(const char* str, char** end) { + uint_fast64_t res = strtol(str, end, 10); + if (str == *end) { + LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number."); + LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\""); + throw storm::exceptions::WrongFormatException("Error while parsing integer. Next input token is not a number."); + } + return res; +} + +/*! + * Calls strtod() internally and checks if the new pointer is different + * from the original one, i.e. if str != *end. If they are the same, a + * storm::exceptions::WrongFormatException will be thrown. + * @param str String to parse + * @param end New pointer will be written there + * @return Result of strtod() + */ +double checked_strtod(const char* str, char** end) { + double res = strtod(str, end); + if (str == *end) { + LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number."); + LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\""); + throw storm::exceptions::WrongFormatException("Error while parsing floating point. Next input token is not a number."); + } + return res; +} + +/*! + * Skips all numbers, letters and special characters. + * Returns a pointer to the first char that is a whitespace. + * @param buf The string buffer to operate on. + * @return A pointer to the first whitespace character. + */ +char* skipWord(char* buf){ + while(!isspace(*buf) && *buf != '\0') buf++; + return buf; +} + +/*! + * Skips spaces, tabs, newlines and carriage returns. Returns a pointer + * to first char that is not a whitespace. + * @param buf The string buffer to operate on. + * @return A pointer to the first non-whitespace character. + */ +char* trimWhitespaces(char* buf) { + while (isspace(*buf)) buf++; + return 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) { + return buffer + strcspn(buffer, "\n\r\0"); +} + +/*! + * @brief Encapsulates the usage of function @strchr to forward to the next line + */ +char* forwardToNextLine(char* buffer) { + char* lineEnd = forwardToLineEnd(buffer); + while((*lineEnd == '\n') || (*lineEnd == '\r')) lineEnd++; + return lineEnd; +} + +} // namespace cstring + +} // namespace utility + +} // namespace storm diff --git a/src/utility/cstring.h b/src/utility/cstring.h new file mode 100644 index 000000000..ebe153f3b --- /dev/null +++ b/src/utility/cstring.h @@ -0,0 +1,53 @@ +/* + * cstring.h + * + * Created on: 30.01.2014 + * Author: Manuel Sascha Weiand + */ + +#ifndef STORM_UTILITY_CSTRING_H_ +#define STORM_UTILITY_CSTRING_H_ + +#include + +namespace storm { + namespace utility { + namespace cstring { + + /*! + * @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); + + /*! + * @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); + + /*! + * @brief Encapsulates the usage of function @strchr to forward to the next line + * + * Note: All lines after the current, which do not contain any characters are skipped. + */ + char* forwardToNextLine(char* buffer); + + } // namespace cstring + } // namespace utility +} // namespace storm + +#endif /* STORM_UTILITY_CSTRING_H_ */ diff --git a/test/functional/parser/MarkovAutomatonParserTest.cpp b/test/functional/parser/MarkovAutomatonParserTest.cpp index d4ad69b75..77af61ef7 100644 --- a/test/functional/parser/MarkovAutomatonParserTest.cpp +++ b/test/functional/parser/MarkovAutomatonParserTest.cpp @@ -14,7 +14,7 @@ #include "src/parser/MarkovAutomatonSparseTransitionParser.h" #include "src/parser/SparseStateRewardParser.h" -#include "src/parser/Parser.h" +#include "src/utility/cstring.h" #include "src/parser/MarkovAutomatonParser.h" #define STATE_COUNT 6