From a39e9a821fd4f57af55bc85600bf6a0e297f4e1d Mon Sep 17 00:00:00 2001 From: PBerger Date: Sun, 10 Aug 2014 19:54:49 +0200 Subject: [PATCH 1/5] Fixed a type error in TBB implementation. Former-commit-id: 680f43b36af108bfe3333ee168f6c0cd5dff1b83 --- src/storage/SparseMatrix.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 5042bb2e7..c6bfd0214 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -778,8 +778,8 @@ namespace storm { const_iterator ite; std::vector::const_iterator rowIterator = this->rowIndications.begin() + startRow; std::vector::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow; - typename std::vector::iterator resultIterator = result.begin() + startRow; - typename std::vector::iterator resultIteratorEnd = result.begin() + endRow; + std::vector::iterator resultIterator = result.begin() + startRow; + std::vector::iterator resultIteratorEnd = result.begin() + endRow; for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) { *resultIterator = storm::utility::constantZero(); From 94b2d45e059b5841cb203c747cf107f9dbf1a7e6 Mon Sep 17 00:00:00 2001 From: PBerger Date: Tue, 12 Aug 2014 23:14:02 +0200 Subject: [PATCH 2/5] Fixed error reporting in AtomicPropositionLabelingParser.cpp and SparseStateRewardParser.cpp. Former-commit-id: 155d96a54fabbfe3089c11e7e0bd36dec1252ff9 --- .../AtomicPropositionLabelingParser.cpp | 23 ++++++++++--------- src/parser/SparseStateRewardParser.cpp | 17 +++++++------- 2 files changed, 21 insertions(+), 19 deletions(-) diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp index 0dac9a8c9..dffdd030a 100644 --- a/src/parser/AtomicPropositionLabelingParser.cpp +++ b/src/parser/AtomicPropositionLabelingParser.cpp @@ -29,8 +29,8 @@ namespace storm { // Open the given file. 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."; + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."); + throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process."; } MappedFile file(filename.c_str()); @@ -68,10 +68,10 @@ namespace storm { // 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."); + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive)."); if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token."); if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token."); - throw storm::exceptions::WrongFormatException(); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive)."; } @@ -100,8 +100,8 @@ namespace storm { 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(); + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found."; } else if (cnt > 0) { @@ -127,6 +127,7 @@ namespace storm { uint_fast64_t state = 0; uint_fast64_t lastState = (uint_fast64_t)-1; + uint_fast64_t const startIndexComparison = lastState; cnt = 0; // Now parse the assignments of labels to nodes. @@ -137,9 +138,9 @@ namespace storm { state = checked_strtol(buf, &buf); // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). - if(state <= lastState && lastState != (uint_fast64_t)-1) { - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). State " << state << " was found but has already been read or skipped previously."); - throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; + if (state <= lastState && lastState != startIndexComparison) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."; } while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { @@ -159,8 +160,8 @@ namespace storm { // Has the label been declared in the header? if(!labeling.containsAtomicProposition(proposition)) { - LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition" << proposition << " was found but not declared."); - throw storm::exceptions::WrongFormatException(); + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared."; } labeling.addAtomicPropositionToState(proposition, state); buf += cnt; diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp index 679bb5e7e..e707dbe3b 100644 --- a/src/parser/SparseStateRewardParser.cpp +++ b/src/parser/SparseStateRewardParser.cpp @@ -4,7 +4,7 @@ * Created on: 23.12.2012 * Author: Christian Dehnert */ - +#include #include "src/parser/SparseStateRewardParser.h" #include "src/exceptions/WrongFormatException.h" @@ -37,6 +37,7 @@ namespace storm { // Now parse state reward assignments. uint_fast64_t state = 0; uint_fast64_t lastState = (uint_fast64_t)-1; + uint_fast64_t const startIndexComparison = lastState; double reward; // Iterate over states. @@ -47,21 +48,21 @@ namespace storm { // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). // Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index). - if(state <= lastState && lastState != (uint_fast64_t)-1) { - LOG4CPLUS_ERROR(logger, "State " << state << " was found but has already been read or skipped previously."); - throw storm::exceptions::WrongFormatException() << "State " << state << " was found but has already been read or skipped previously."; + if (state <= lastState && lastState != startIndexComparison) { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."; } if(stateCount <= state) { - LOG4CPLUS_ERROR(logger, "Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states."); - throw storm::exceptions::OutOfRangeException() << "Found reward for a state of an invalid index \"" << state << "\""; + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states."); + throw storm::exceptions::OutOfRangeException() << "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\""; } reward = checked_strtod(buf, &buf); if (reward < 0.0) { - LOG4CPLUS_ERROR(logger, "Expected positive reward value but got \"" << reward << "\"."); - throw storm::exceptions::WrongFormatException() << "State reward file specifies illegal reward value."; + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Expected positive reward value but got \"" << reward << "\"."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State reward file specifies illegal reward value."; } stateRewards[state] = reward; From 3bc31e927dca5b0646305fbcf7466bfebc9042e7 Mon Sep 17 00:00:00 2001 From: PBerger Date: Tue, 12 Aug 2014 23:19:31 +0200 Subject: [PATCH 3/5] Added per-formula timing output. This is basically a picky merge from my CUDA branch. Former-commit-id: bb386486bb0c9eb9fae8693b7e24a9b232aef84a --- src/storm.cpp | 22 +++++++++++++++++++--- 1 file changed, 19 insertions(+), 3 deletions(-) diff --git a/src/storm.cpp b/src/storm.cpp index af69da175..1a30c2d7a 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -17,8 +17,10 @@ #include #include #include +#include #include #include +#include #include "storm-config.h" #include "storm-version.h" @@ -112,10 +114,10 @@ void printUsage() { ULARGE_INTEGER uLargeInteger; uLargeInteger.LowPart = ftKernel.dwLowDateTime; uLargeInteger.HighPart = ftKernel.dwHighDateTime; - double kernelTime = uLargeInteger.QuadPart / 10000.0; // 100 ns Resolution to milliseconds + double kernelTime = static_cast(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds uLargeInteger.LowPart = ftUser.dwLowDateTime; uLargeInteger.HighPart = ftUser.dwHighDateTime; - double userTime = uLargeInteger.QuadPart / 10000.0; + double userTime = static_cast(uLargeInteger.QuadPart) / 10000.0; std::cout << "CPU Time: " << std::endl; std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl; @@ -147,6 +149,16 @@ void setUpFileLogging() { logger.addAppender(fileLogAppender); } +/*! +* Gives the current working directory +* +* @return std::string The path of the current working directory +*/ +std::string getCurrentWorkingDirectory() { + char temp[512]; + return (_getcwd(temp, 512 - 1) ? std::string(temp) : std::string("")); +} + /*! * Prints the header. */ @@ -162,7 +174,7 @@ void printHeader(const int argc, const char* argv[]) { if (STORM_CPP_VERSION_DIRTY == 1) { std::cout << " (DIRTY)"; } - std::cout << std::endl; + std::cout << "." << std::endl; #ifdef STORM_HAVE_INTELTBB std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl; @@ -185,6 +197,7 @@ void printHeader(const int argc, const char* argv[]) { commandStream << argv[i] << " "; } std::cout << "Command line: " << commandStream.str() << std::endl << std::endl; + std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; } /*! @@ -290,8 +303,11 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); for (auto formula : formulaList) { + std::chrono::high_resolution_clock::time_point startTime = std::chrono::high_resolution_clock::now(); modelchecker.check(*formula); delete formula; + std::chrono::high_resolution_clock::time_point endTime = std::chrono::high_resolution_clock::now(); + std::cout << "Checking the formula took " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; } } } From a49991484c11348a2a0843374f0c2836a2a9daf3 Mon Sep 17 00:00:00 2001 From: PBerger Date: Tue, 12 Aug 2014 23:47:05 +0200 Subject: [PATCH 4/5] Fixed missing definitions for the current working directory. Former-commit-id: cc991435262f888ece909d3811ce153147049636 --- src/utility/OsDetection.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/utility/OsDetection.h b/src/utility/OsDetection.h index 1969a6de7..37be3f0e7 100644 --- a/src/utility/OsDetection.h +++ b/src/utility/OsDetection.h @@ -4,10 +4,12 @@ #if defined __linux__ || defined __linux # define LINUX # include +# include #include // Required by ErrorHandling.h #include // Required by ErrorHandling.h #include // Required by storm.cpp, Memory Usage #include // Required by storm.cpp, Memory Usage +# define GetCurrentDir getcwd #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__ # define MACOSX # define _DARWIN_USE_64_BIT_INODE @@ -17,6 +19,7 @@ # include // Required by ErrorHandling.h # include // Required by storm.cpp, Memory Usage # include // Required by storm.cpp, Memory Usage +# define GetCurrentDir getcwd #elif defined _WIN32 || defined _WIN64 # define WINDOWS # ifndef NOMINMAX @@ -28,8 +31,10 @@ # include # include # include +# include # define strncpy strncpy_s # define sscanf sscanf_s +# define GetCurrentDir _getcwd // This disables Warning C4250 - Diamond Inheritance Dominance #pragma warning(disable:4250) From 57882db84ef80109c8991025e325888fc74de0ab Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 13 Aug 2014 00:28:50 +0200 Subject: [PATCH 5/5] Fixed warnings about unused variables in PathBasedSubsystemGenerator and SMTMinimalCommandSetGenerator. Also some stuff with type conversions. Fixed the missing include/definition for getcwd Former-commit-id: 08f82f2ed221357443fff7b34c21e6aefed8f908 --- src/counterexamples/PathBasedSubsystemGenerator.h | 7 +++---- src/counterexamples/SMTMinimalCommandSetGenerator.h | 5 +++-- src/storm.cpp | 3 ++- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h index 2325eebe8..48a175494 100644 --- a/src/counterexamples/PathBasedSubsystemGenerator.h +++ b/src/counterexamples/PathBasedSubsystemGenerator.h @@ -588,7 +588,7 @@ public: // estimate the path count using the models state count as well as the probability bound uint_fast8_t const minPrec = 10; uint_fast64_t const stateCount = model.getNumberOfStates(); - uint_fast64_t const stateEstimate = ((T) stateCount) * bound; + uint_fast64_t const stateEstimate = static_cast(stateCount * bound); //since this only has a good effect on big models -> use only if model has at least 10^5 states uint_fast64_t precision = stateEstimate > 100000 ? stateEstimate/1000 : minPrec; @@ -686,9 +686,8 @@ public: //Are we critical? if(subSysProb >= bound){ break; - } - else if (stateEstimate > 100000){ - precision = (stateEstimate/1000) - ((stateEstimate/1000) - minPrec)*(subSysProb/bound); + } else if (stateEstimate > 100000){ + precision = static_cast((stateEstimate / 1000.0) - ((stateEstimate / 1000.0) - minPrec)*(subSysProb/bound)); } } } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 2a33b50eb..94f550141 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1809,15 +1809,16 @@ namespace storm { phiStates = untilFormula.getLeft().check(modelchecker); psiStates = untilFormula.getRight().check(modelchecker); - } catch (std::bad_cast const& e) { + } catch (std::bad_cast const&) { // If the nested formula was not an until formula, it remains to check whether it's an eventually formula. try { storm::property::prctl::Eventually const& eventuallyFormula = dynamic_cast const&>(pathFormula); phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); psiStates = eventuallyFormula.getChild().check(modelchecker); - } catch (std::bad_cast const& e) { + } catch (std::bad_cast const&) { // If the nested formula is neither an until nor a finally formula, we throw an exception. + LOG4CPLUS_ERROR(logger, "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation."; } } diff --git a/src/storm.cpp b/src/storm.cpp index 1a30c2d7a..2287e9b37 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -45,6 +45,7 @@ #include "src/utility/ErrorHandling.h" #include "src/formula/Prctl.h" #include "src/utility/vector.h" +#include "src/utility/OsDetection.h" #include "src/settings/Settings.h" // Registers all standard options @@ -156,7 +157,7 @@ void setUpFileLogging() { */ std::string getCurrentWorkingDirectory() { char temp[512]; - return (_getcwd(temp, 512 - 1) ? std::string(temp) : std::string("")); + return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); } /*!