diff --git a/CMakeLists.txt b/CMakeLists.txt index a78fb8925..bec5a07dc 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -90,6 +90,8 @@ elseif(MSVC) message(STATUS "Using MSVC") # required for GMM to compile, ugly error directive in their code add_definitions(/D_SCL_SECURE_NO_DEPRECATE) + # required as the PRCTL Parser bloats object files (COFF) beyond their maximum size (see http://msdn.microsoft.com/en-us/library/8578y171(v=vs.110).aspx) + add_definitions(/bigobj) else(CLANG) message(STATUS "Using CLANG") # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. @@ -120,13 +122,19 @@ file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) set(STORM_SOURCES "${STORM_SOURCES_WITHOUT_MAIN};${STORM_MAIN_FILE}") file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) -file(GLOB_RECURSE STORM_FORMULA_FILES ${PROJECT_SOURCE_DIR}/src/formula/*.h ${PROJECT_SOURCE_DIR}/src/formula/*.cpp) +file(GLOB STORM_FORMULA_FILES ${PROJECT_SOURCE_DIR}/src/formula/*.h ${PROJECT_SOURCE_DIR}/src/formula/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_ABSTRACT_FILES ${PROJECT_SOURCE_DIR}/src/formula/abstract/*.h ${PROJECT_SOURCE_DIR}/src/formula/abstract/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_CSL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Csl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Csl/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_LTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Ltl/*.cpp) +file(GLOB_RECURSE STORM_FORMULA_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.h ${PROJECT_SOURCE_DIR}/src/formula/Prctl/*.cpp) file(GLOB_RECURSE STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp) file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp) -file(GLOB_RECURSE STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) +file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp) +file(GLOB_RECURSE STORM_PARSER_PRISMPARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.h ${PROJECT_SOURCE_DIR}/src/parser/prismparser/*.cpp) file(GLOB_RECURSE STORM_STORAGE_FILES ${PROJECT_SOURCE_DIR}/src/storage/*.h ${PROJECT_SOURCE_DIR}/src/storage/*.cpp) file(GLOB_RECURSE STORM_UTILITY_FILES ${PROJECT_SOURCE_DIR}/src/utility/*.h ${PROJECT_SOURCE_DIR}/src/utility/*.cpp) -file(GLOB_RECURSE STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) +file(GLOB STORM_IR_FILES ${PROJECT_SOURCE_DIR}/src/ir/*.h ${PROJECT_SOURCE_DIR}/src/ir/*.cpp) +file(GLOB_RECURSE STORM_IR_EXPRESSIONS_FILES ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.h ${PROJECT_SOURCE_DIR}/src/ir/expressions/*.cpp) # Test Sources # Note that the tests also need the source files, except for the main file @@ -138,12 +146,18 @@ source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(formula FILES ${STORM_FORMULA_FILES}) +source_group(formula\\abstract FILES ${STORM_FORMULA_ABSTRACT_FILES}) +source_group(formula\\csl FILES ${STORM_FORMULA_CSL_FILES}) +source_group(formula\\ltl FILES ${STORM_FORMULA_LTL_FILES}) +source_group(formula\\prctl FILES ${STORM_FORMULA_PRCTL_FILES}) source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES}) source_group(models FILES ${STORM_MODELS_FILES}) source_group(parser FILES ${STORM_PARSER_FILES}) +source_group(parser\\prismparser FILES ${STORM_PARSER_PRISMPARSER_FILES}) source_group(storage FILES ${STORM_STORAGE_FILES}) source_group(utility FILES ${STORM_UTILITY_FILES}) source_group(ir FILES ${STORM_IR_FILES}) +source_group(ir\\expressions FILES ${STORM_IR_EXPRESSIONS_FILES}) source_group(functional-test FILES ${STORM_FUNCTIONAL_TEST_FILES}) source_group(performance-test FILES ${STORM_PERFORMANCE_TEST_FILES}) @@ -236,6 +250,14 @@ target_link_libraries(storm ${Boost_LIBRARIES}) target_link_libraries(storm-functional-tests ${Boost_LIBRARIES}) target_link_libraries(storm-performance-tests ${Boost_LIBRARIES}) +if (MSVC) + # Add the DebugHelper DLL + set(CMAKE_CXX_STANDARD_LIBRARIES "${CMAKE_CXX_STANDARD_LIBRARIES} Dbghelp.lib") + target_link_libraries(storm "Dbghelp.lib") + target_link_libraries(storm-functional-tests "Dbghelp.lib") + target_link_libraries(storm-performance-tests "Dbghelp.lib") +endif(MSVC) + if (USE_INTELTBB) target_link_libraries(storm tbb tbbmalloc) target_link_libraries(storm-functional-tests tbb tbbmalloc) @@ -318,9 +340,16 @@ if (LOG4CPLUS_INCLUDE_DIR) endif(LOG4CPLUS_INCLUDE_DIR) if (CUDD_LIBRARY_DIRS) - target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd") - target_link_libraries(storm-functional-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") - target_link_libraries(storm-performance-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + if (MSVC) + set(cuddMsvcLibs "optimized" "${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/CUDD_Win32/x64/Release/CUDD_Win32.lib" "debug" "${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/CUDD_Win32/x64/Debug/CUDD_Win32.lib") + target_link_libraries(storm ${cuddMsvcLibs}) + target_link_libraries(storm-functional-tests ${cuddMsvcLibs}) + target_link_libraries(storm-performance-tests ${cuddMsvcLibs}) + else () + target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd") + target_link_libraries(storm-functional-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + target_link_libraries(storm-performance-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") + endif () endif(CUDD_LIBRARY_DIRS) if (THREADS_FOUND) diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h index 06b7dd37f..819133a23 100644 --- a/src/adapters/SymbolicModelAdapter.h +++ b/src/adapters/SymbolicModelAdapter.h @@ -16,6 +16,7 @@ #include "cuddObj.hh" #include #include +#include namespace storm { @@ -138,6 +139,16 @@ private: SymbolicExpressionAdapter rowExpressionAdapter; SymbolicExpressionAdapter columnExpressionAdapter; + // As log2 is not part of C90, only of C99 which no Compiler fully supports, this feature is unavailable on MSVC + inline double log2(uint_fast64_t number) { +# include "src/utility/OsDetection.h" +# ifndef WINDOWS + return std::log2(number); +# else + return std::log(number) / std::log(2); +# endif + } + ADD* getInitialStateDecisionDiagram(storm::ir::Program const& program) { ADD* initialStates = cuddUtility->getOne(); for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { @@ -258,7 +269,7 @@ private: throw storm::exceptions::WrongFormatException() << "Range of variable " << integerVariable.getName() << " is empty or negativ."; } - uint_fast64_t numberOfDecisionDiagramVariables = static_cast(std::ceil(std::log2(integerRange))); + uint_fast64_t numberOfDecisionDiagramVariables = static_cast(std::ceil(log2(integerRange))); std::vector allRowDecisionDiagramVariablesForVariable; std::vector allColumnDecisionDiagramVariablesForVariable; diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index 96ad94b2b..c854bc645 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -119,24 +119,24 @@ std::map> P } std::string Program::getVariableString() const { - std::map bools; - std::map ints; - unsigned maxInt = 0, maxBool = 0; + std::map bools; + std::map ints; + uint_fast64_t maxInt = 0, maxBool = 0; for (Module module: this->modules) { - for (unsigned int i = 0; i < module.getNumberOfBooleanVariables(); i++) { + for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); i++) { storm::ir::BooleanVariable var = module.getBooleanVariable(i); bools[var.getIndex()] = var.getName(); if (var.getIndex() >= maxBool) maxBool = var.getIndex()+1; } - for (unsigned int i = 0; i < module.getNumberOfIntegerVariables(); i++) { + for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); i++) { storm::ir::IntegerVariable var = module.getIntegerVariable(i); ints[var.getIndex()] = var.getName(); if (var.getIndex() >= maxInt) maxInt = var.getIndex()+1; } } std::stringstream ss; - for (unsigned int i = 0; i < maxBool; i++) ss << bools[i] << "\t"; - for (unsigned int i = 0; i < maxInt; i++) ss << ints[i] << "\t"; + for (uint_fast64_t i = 0; i < maxBool; i++) ss << bools[i] << "\t"; + for (uint_fast64_t i = 0; i < maxInt; i++) ss << ints[i] << "\t"; return ss.str(); } diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index c4ad56ed7..1cc3450e5 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -62,7 +62,7 @@ public: return defined; } - int getValue() { + int_fast64_t getValue() { return value; } diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 62e6481cc..d28e1c0d3 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -59,7 +59,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas * Check all transitions for non-zero diagonal entries and deadlock states. */ int_fast64_t lastRow = -1; - int_fast64_t row, col; + uint_fast64_t row, col; uint_fast64_t readTransitionCount = 0; bool rowHadDiagonalEntry = false; double val; diff --git a/src/storm.cpp b/src/storm.cpp index 548399d38..3c3d47679 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -45,17 +45,47 @@ #include "src/exceptions/InvalidSettingsException.h" -#include -#include #include #include void printUsage() { +#ifndef WINDOWS struct rusage ru; getrusage(RUSAGE_SELF, &ru); std::cout << "Memory Usage: " << ru.ru_maxrss << "kB" << std::endl; - std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; + std::cout << "CPU Time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; +#else + HANDLE hProcess = GetCurrentProcess (); + FILETIME ftCreation, ftExit, ftUser, ftKernel; + PROCESS_MEMORY_COUNTERS pmc; + if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { + std::cout << "Memory Usage: " << std::endl; + std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; + std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; + std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; + std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; + std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; + std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; + std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; + std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; + std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; + } + + GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); + + ULARGE_INTEGER uLargeInteger; + uLargeInteger.LowPart = ftKernel.dwLowDateTime; + uLargeInteger.HighPart = ftKernel.dwHighDateTime; + double kernelTime = uLargeInteger.QuadPart / 10000.0; // 100 ns Resolution to milliseconds + uLargeInteger.LowPart = ftUser.dwLowDateTime; + uLargeInteger.HighPart = ftUser.dwHighDateTime; + double userTime = uLargeInteger.QuadPart / 10000.0; + + std::cout << "CPU Time: " << std::endl; + std::cout << "\tKernel Time: " << std::setprecision(3) << kernelTime << std::endl; + std::cout << "\tUser Time: " << std::setprecision(3) << userTime << std::endl; +#endif } diff --git a/src/utility/CuddUtility.h b/src/utility/CuddUtility.h index 8102eb012..2832884a2 100644 --- a/src/utility/CuddUtility.h +++ b/src/utility/CuddUtility.h @@ -10,6 +10,8 @@ #include "cuddObj.hh" +#include "boost/integer/integer_mask.hpp" + namespace storm { namespace utility { diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h index ea65ab03a..b832b7c69 100644 --- a/src/utility/ErrorHandling.h +++ b/src/utility/ErrorHandling.h @@ -8,9 +8,9 @@ #ifndef ERRORHANDLING_H #define ERRORHANDLING_H +#include "src/utility/OsDetection.h" #include -#include -#include + /* * Demangles the given string. This is needed for the correct display of backtraces. @@ -22,16 +22,42 @@ std::string demangle(char const* symbol) { // Attention: sscanf format strings rely on the size being 128. char temp[128]; - char* demangled; - // Check for C++ symbol. + // Check for C++ symbol, on Non-MSVC Only if (sscanf(symbol, "%*[^(]%*[^_]%127[^)+]", temp) == 1) { +#ifndef WINDOWS + char* demangled; if (NULL != (demangled = abi::__cxa_demangle(temp, NULL, NULL, &status))) { std::string result(demangled); free(demangled); return result; } +#else + DWORD error; + HANDLE hProcess; + + SymSetOptions(SYMOPT_UNDNAME | SYMOPT_DEFERRED_LOADS); + + hProcess = GetCurrentProcess(); + + if (!SymInitialize(hProcess, NULL, TRUE)) { + // SymInitialize failed + error = GetLastError(); + LOG4CPLUS_ERROR(logger, "SymInitialize returned error : " << error); + return FALSE; + } else { + char demangled[1024]; + if (UnDecorateSymbolName(temp, demangled, sizeof(demangled), UNDNAME_COMPLETE)) { + return std::string(demangled); + } else { + // UnDecorateSymbolName failed + DWORD error = GetLastError(); + LOG4CPLUS_ERROR(logger, "UnDecorateSymbolName returned error: " << error); + } + } +#endif } + // Check for C symbol. if (sscanf(symbol, "%127s", temp) == 1) { return temp; @@ -50,6 +76,7 @@ void signalHandler(int sig) { #define SIZE 128 LOG4CPLUS_FATAL(logger, "The program received signal " << sig << ". The following backtrace shows the status upon reception of the signal."); +#ifndef WINDOWS void *buffer[SIZE]; char **strings; int nptrs; @@ -68,6 +95,9 @@ void signalHandler(int sig) { LOG4CPLUS_FATAL(logger, nptrs-j << ": " << demangle(strings[j])); } free(strings); +#else + LOG4CPLUS_WARN(logger, "No Backtrace Support available on Platform Windows!"); +#endif LOG4CPLUS_FATAL(logger, "Exiting."); exit(2); } diff --git a/src/utility/OsDetection.h b/src/utility/OsDetection.h index bc459d40c..8fb6c7c6e 100644 --- a/src/utility/OsDetection.h +++ b/src/utility/OsDetection.h @@ -4,17 +4,32 @@ #if defined __linux__ || defined __linux # define LINUX # 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 #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__ # define MACOSX # define _DARWIN_USE_64_BIT_INODE # 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 #elif defined _WIN32 || defined _WIN64 # define WINDOWS # define NOMINMAX # include # include +# include +# include # define strncpy strncpy_s +# define sscanf sscanf_s + +// This disables Warning C4250 - Diamond Inheritance Dominance +#pragma warning(disable:4250) + #else # error Could not detect Operating System #endif