diff --git a/CMakeLists.txt b/CMakeLists.txt index 8caf0b081..d17922f26 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -75,7 +75,7 @@ elseif(MSVC) add_definitions(/D_SCL_SECURE_NO_DEPRECATE) else(CLANG) # Set standard flags for clang - set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") + set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG -funroll-loops -O4") set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable") # Turn on popcnt instruction if desired (yes by default) diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h index c1b6ee054..6c670f88b 100644 --- a/src/exceptions/BaseException.h +++ b/src/exceptions/BaseException.h @@ -28,7 +28,11 @@ class BaseException : public std::exception { } virtual const char* what() const throw() { - return this->stream.str().c_str(); + std::string errorString = this->stream.str(); + char* result = new char[errorString.size() + 1]; + result[errorString.size()] = '\0'; + std::copy(errorString.begin(), errorString.end(), result); + return result; } private: diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index c5668846d..e9e430988 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -133,7 +133,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast * @return a pointer to the created sparse matrix. */ -DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename) +DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing) : matrix(nullptr) { /* * Enforce locale where decimal point is '.'. @@ -188,12 +188,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st this->matrix->initialize(non_zero); int_fast64_t row, lastrow = -1, col; - int_fast64_t lastDiagonal = -1; double val; bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); - bool fixSelfloops = storm::settings::instance()->isSet("fix-selfloops"); bool hadDeadlocks = false; - bool hadNoSelfLoops = false; + bool rowHadDiagonalEntry = false; /* * Read all transitions from file. Note that we assume that the @@ -208,45 +206,39 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st col = checked_strtol(buf, &buf); val = checked_strtod(buf, &buf); + if (row != lastrow) { + rowHadDiagonalEntry = false; + } + /* - * Check if a self-loop was skipped. + * Check if we skipped a state entirely, i.e. a state does not have any + * outgoing transitions. */ - if (lastDiagonal < (row - 1)) { - /* - * Check if we skipped a node entirely, i.e. a node does not have any - * outgoing transitions. - */ - if ((lastrow + 1) < row) { - for (int_fast64_t node = lastrow + 1; node < row; node++) { - hadDeadlocks = true; - if (fixDeadlocks || fixSelfloops) { - this->matrix->addNextValue(node, node, storm::utility::constGetOne()); - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); - } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); - } - } - } else { - // there were other transitions but no self-loop - for (int_fast64_t node = lastDiagonal + 1; node < row; node++) { - hadNoSelfLoops = true; - if (fixSelfloops) { - this->matrix->addNextValue(node, node, storm::utility::constGetZero()); - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no self transition. A self-loop was inserted."); - } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no self transition."); - } + if ((lastrow + 1) < row) { + for (int_fast64_t state = lastrow + 1; state < row; ++state) { + hadDeadlocks = true; + if (fixDeadlocks) { + this->matrix->addNextValue(state, state, storm::utility::constGetOne()); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << state << " has no outgoing transitions. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << state << " has no outgoing transitions."); } } - lastDiagonal = row - 1; - } - - + } + + // Insert the missing diagonal value if requested. + if (col > row && !rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { + this->matrix->addNextValue(row, row, storm::utility::constGetZero()); + } + rowHadDiagonalEntry = true; + } + /* - * Check if this is a self-loop and remember that + * Check if the transition is a self-loop */ if (row == col) { - lastDiagonal = row; + rowHadDiagonalEntry = true; } lastrow = row; @@ -255,7 +247,6 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st buf = trimWhitespaces(buf); } if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; - if (!fixSelfloops && hadNoSelfLoops) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had no self loops. You can use --fix-selfloops to insert self-loops on the fly."; /* * Finalize Matrix. diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 099d0fa4a..2407f3398 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -17,7 +17,7 @@ namespace parser { */ class DeterministicSparseTransitionParser : public Parser { public: - DeterministicSparseTransitionParser(std::string const &filename); + DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true); std::shared_ptr> getMatrix() { return this->matrix; diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index f983f22fc..26f733071 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -139,7 +139,6 @@ void Settings::initDescriptions() { ("transrew", bpo::value()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") - ("fix-selfloops", "insert self-loops for states without such transitions") ; }