diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 211a3aecf..a5150c05a 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -668,7 +668,7 @@ namespace storm { // Finalize the resulting matrices. modelComponents.transitionMatrix = transitionMatrixBuilder.build(); - modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount()); + modelComponents.transitionRewardMatrix = transitionRewardMatrixBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()); // Now build the state labeling. modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index dffdd030a..58ee0abbd 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -34,7 +34,7 @@ namespace storm { } MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // First pass: Count the number of propositions. bool foundDecl = false, foundEnd = false; diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 808d36f0b..b4e72c4cf 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -12,6 +12,7 @@ #include "src/parser/DeterministicModelParser.h" #include "src/parser/NondeterministicModelParser.h" #include "src/parser/MarkovAutomatonParser.h" +#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/WrongFormatException.h" #include "src/utility/cstring.h" @@ -74,25 +75,30 @@ namespace storm { // Open the file. MappedFile file(filename.c_str()); - char* buf = file.getData(); + + LOG_THROW(file.getDataSize() >= hintLength, storm::exceptions::WrongFormatException, "File too short to be readable."); + char const* fileData = file.getData(); + + char filehintBuffer[hintLength + 1]; + memcpy(filehintBuffer, fileData, hintLength); + filehintBuffer[hintLength] = 0; // Find and read in the hint. - char hint[65]; - // %60s => The input hint can be AT MOST 60 chars long. + std::string formatString = "%" + std::to_string(hintLength) + "s"; + char hint[5]; #ifdef WINDOWS - sscanf_s(buf, "%60s", hint, sizeof(hint)); + sscanf_s(filehintBuffer, formatString.c_str(), hint, hintLength + 1); #else - sscanf(buf, "%60s", hint); + int ret = sscanf(filehintBuffer, formatString.c_str(), hint); #endif - for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); - + // Check if the hint value is known and store the appropriate enum value. - if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC; - else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC; - else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP; - else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP; - else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA; + if (strcmp(hint, "DTMC") == 0) hintType = storm::models::DTMC; + else if (strcmp(hint, "CTMC") == 0) hintType = storm::models::CTMC; + else if (strcmp(hint, "MDP") == 0) hintType = storm::models::MDP; + else if (strcmp(hint, "CTMDP") == 0) hintType = storm::models::CTMDP; + else if (strcmp(hint, "MA") == 0) hintType = storm::models::MA; return hintType; } diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index 993cbe6bb..c3bab16e6 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -47,6 +47,8 @@ namespace storm { std::string const & transitionRewardFilename = ""); private: + // Define the maximal length of a hint in the file. + static constexpr uint_fast64_t hintLength = 10; /*! * Opens the given file and parses the file format hint. diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 67e31484f..8f81685b6 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -53,7 +53,7 @@ namespace storm { // Open file. MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // Perform first pass, i.e. count entries that are not zero. bool insertDiagonalEntriesIfMissing = !isRewardFile; @@ -115,6 +115,23 @@ namespace storm { buf = trimWhitespaces(buf); } } else { + // Read first row and add self-loops if necessary. + char const* tmp; + row = checked_strtol(buf, &tmp); + + if (row > 0) { + for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { + hadDeadlocks = true; + if (fixDeadlocks) { + resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::constantOne()); + 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. + } + } + } + while (buf[0] != '\0') { // Read next transition. @@ -139,7 +156,6 @@ namespace storm { 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."); @@ -193,7 +209,7 @@ namespace storm { return result; } - DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char* buf, bool insertDiagonalEntriesIfMissing) { + DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf, bool insertDiagonalEntriesIfMissing) { DeterministicSparseTransitionParser::FirstPassResult result; @@ -207,6 +223,16 @@ namespace storm { // Check all transitions for non-zero diagonal entries and deadlock states. uint_fast64_t row, col, lastRow = 0, lastCol = -1; bool rowHadDiagonalEntry = false; + + // Read first row and reserve space for self-loops if necessary. + char const* tmp; + row = checked_strtol(buf, &tmp); + if (row > 0) { + for (uint_fast64_t skippedRow = 0; skippedRow < row; ++skippedRow) { + ++result.numberOfNonzeroEntries; + } + } + while (buf[0] != '\0') { // Read the transition. diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index e31ef2291..ede2e37ba 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -67,7 +67,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, bool insertDiagonalEntriesIfMissing = true); + static FirstPassResult firstPass(char const* buffer, bool insertDiagonalEntriesIfMissing = true); /* * The main parsing routine. diff --git a/src/parser/MappedFile.cpp b/src/parser/MappedFile.cpp index 2b7e13a05..7abf526cf 100644 --- a/src/parser/MappedFile.cpp +++ b/src/parser/MappedFile.cpp @@ -42,15 +42,15 @@ namespace storm { 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)) { + + this->data = static_cast(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0)); + if (this->data == MAP_FAILED) { 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 + #elif defined WINDOWS // Do file mapping for windows. // _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile() @@ -100,13 +100,17 @@ namespace storm { return fin.good(); } - char* MappedFile::getData() { + char const* MappedFile::getData() const { return data; } - char* MappedFile::getDataEnd() { + char const* MappedFile::getDataEnd() const { return dataEnd; } + + std::size_t MappedFile::getDataSize() const { + return this->getDataEnd() - this->getData(); + } } // namespace parser } // namespace storm diff --git a/src/parser/MappedFile.h b/src/parser/MappedFile.h index 6de9877d4..4273d1c55 100644 --- a/src/parser/MappedFile.h +++ b/src/parser/MappedFile.h @@ -8,6 +8,7 @@ #ifndef STORM_PARSER_MAPPEDFILE_H_ #define STORM_PARSER_MAPPEDFILE_H_ +#include #include #include "src/utility/OsDetection.h" @@ -61,15 +62,20 @@ namespace storm { * * @return A pointer to the first character of the mapped file data. */ - char* getData(); + char const* getData() const; /*! * Returns a pointer to the end of the mapped file data. * * @return A pointer to the first position after the last character of the mapped file data. */ - char* getDataEnd(); + char const* getDataEnd() const; + /*! + * Returns the size of the mapped file data. + */ + std::size_t getDataSize() const; + private: //! A pointer to the mapped file content. diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index 6e02df99d..fbfa9a1b2 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -12,7 +12,7 @@ namespace storm { using namespace storm::utility::cstring; - MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char* buf) { + MarkovAutomatonSparseTransitionParser::FirstPassResult MarkovAutomatonSparseTransitionParser::firstPass(char const* buf) { MarkovAutomatonSparseTransitionParser::FirstPassResult result; bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -154,7 +154,7 @@ namespace storm { return result; } - MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char* buf, FirstPassResult const& firstPassResult) { + MarkovAutomatonSparseTransitionParser::Result MarkovAutomatonSparseTransitionParser::secondPass(char const* buf, FirstPassResult const& firstPassResult) { Result result(firstPassResult); bool fixDeadlocks = storm::settings::Settings::getInstance()->isSet("fixDeadlocks"); @@ -271,7 +271,7 @@ namespace storm { // Open file and prepare pointer to buffer. MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); return secondPass(buf, firstPass(buf)); } diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.h b/src/parser/MarkovAutomatonSparseTransitionParser.h index 798a9e0e3..1e1ebd1f0 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.h +++ b/src/parser/MarkovAutomatonSparseTransitionParser.h @@ -85,7 +85,7 @@ namespace storm { * @param buffer The buffer that cointains the input. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char* buffer); + static FirstPassResult firstPass(char const* buffer); /*! * Performs the second pass on the input pointed to by the given buffer with the information of the first pass. @@ -94,7 +94,7 @@ namespace storm { * @param firstPassResult The result of the first pass performed on the same input. * @return A structure representing the result of the second pass. */ - static Result secondPass(char* buffer, FirstPassResult const& firstPassResult); + static Result secondPass(char const* buffer, FirstPassResult const& firstPassResult); }; } // namespace parser diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp index 5923f7778..116364856 100644 --- a/src/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/parser/NondeterministicSparseTransitionParser.cpp @@ -50,7 +50,7 @@ namespace storm { // Open file. MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // Perform first pass, i.e. obtain number of columns, rows and non-zero elements. NondeterministicSparseTransitionParser::FirstPassResult firstPass = NondeterministicSparseTransitionParser::firstPass(file.getData(), isRewardFile, modelInformation); @@ -200,7 +200,7 @@ namespace storm { return resultMatrix; } - NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char* buf, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation) { + NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char const* buf, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation) { // Check file header and extract number of transitions. diff --git a/src/parser/NondeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h index f75babbb7..85a5aac4f 100644 --- a/src/parser/NondeterministicSparseTransitionParser.h +++ b/src/parser/NondeterministicSparseTransitionParser.h @@ -74,7 +74,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, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation); + static FirstPassResult firstPass(char const* buffer, bool isRewardFile, storm::storage::SparseMatrix const & modelInformation); /*! * The main parsing routine. diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index e707dbe3b..364c364b0 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -29,7 +29,7 @@ namespace storm { } MappedFile file(filename.c_str()); - char* buf = file.getData(); + char const* buf = file.getData(); // Create state reward vector with given state count. std::vector stateRewards(stateCount); diff --git a/src/utility/cstring.cpp b/src/utility/cstring.cpp index 2267fdf62..71bcbe69a 100644 --- a/src/utility/cstring.cpp +++ b/src/utility/cstring.cpp @@ -22,8 +22,8 @@ namespace cstring { * @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); +uint_fast64_t checked_strtol(char const* str, char const** end) { + uint_fast64_t res = strtol(str, const_cast(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) << "\""); @@ -40,8 +40,8 @@ uint_fast64_t checked_strtol(const char* str, char** end) { * @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); +double checked_strtod(char const* str, char const** end) { + double res = strtod(str, const_cast(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) << "\""); @@ -56,7 +56,7 @@ double checked_strtod(const char* str, char** end) { * @param buf The string buffer to operate on. * @return A pointer to the first whitespace character. */ -char* skipWord(char* buf){ +char const* skipWord(char const* buf){ while(!isspace(*buf) && *buf != '\0') buf++; return buf; } @@ -67,7 +67,7 @@ char* skipWord(char* buf){ * @param buf The string buffer to operate on. * @return A pointer to the first non-whitespace character. */ -char* trimWhitespaces(char* buf) { +char const* trimWhitespaces(char const* buf) { while (isspace(*buf)) buf++; return buf; } @@ -75,15 +75,15 @@ 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) { +char const* forwardToLineEnd(char const* 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); +char const* forwardToNextLine(char const* buffer) { + char const* lineEnd = forwardToLineEnd(buffer); while((*lineEnd == '\n') || (*lineEnd == '\r')) lineEnd++; return lineEnd; } diff --git a/src/utility/cstring.h b/src/utility/cstring.h index ebe153f3b..65168e525 100644 --- a/src/utility/cstring.h +++ b/src/utility/cstring.h @@ -17,34 +17,34 @@ namespace storm { /*! * @brief Parses integer and checks, if something has been parsed. */ - uint_fast64_t checked_strtol(const char* str, char** end); + uint_fast64_t checked_strtol(const char* str, char const** end); /*! * @brief Parses floating point and checks, if something has been parsed. */ - double checked_strtod(const char* str, char** end); + double checked_strtod(const char* str, char const** end); /*! * @brief Skips all non whitespace characters until the next whitespace. */ - char* skipWord(char* buf); + char const* skipWord(char const* buf); /*! * @brief Skips common whitespaces in a string. */ - char* trimWhitespaces(char* buf); + char const* trimWhitespaces(char const* 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); + char const* forwardToLineEnd(char const* 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); + char const* forwardToNextLine(char const* buffer); } // namespace cstring } // namespace utility