Fixed some problems related to the memory-mapped file.

Former-commit-id: 68225d8006

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);

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;

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;
 		}

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.

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<double>());
+                                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<double>());
-									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.

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.

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<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
-			if (this->data == reinterpret_cast<char*>(-1)) {
+            
+			this->data = static_cast<char*>(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

src/parser/MappedFile.h

@@ -8,6 +8,7 @@
 #ifndef STORM_PARSER_MAPPEDFILE_H_
 #define STORM_PARSER_MAPPEDFILE_H_
 
+#include <cstddef>
 #include <sys/stat.h>
 
 #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.

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));
 		}

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

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<double> const & modelInformation) {
+		NondeterministicSparseTransitionParser::FirstPassResult NondeterministicSparseTransitionParser::firstPass(char const* buf, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation) {
 
 			// Check file header and extract number of transitions.
 

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<double> const & modelInformation);
+			static FirstPassResult firstPass(char const* buffer, bool isRewardFile, storm::storage::SparseMatrix<double> const & modelInformation);
 
 			/*!
 			 * The main parsing routine.

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<double> stateRewards(stateCount);

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<char**>(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<char**>(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;
 }

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