Updated CMakeLists.txt

- Added more sub-folders in the source-structure
 - Added an option for MSVC to use /bigobj with the Compiler as PrismParser.cpp bloats the object instance count
 - Edited CUDD Link Targets for MSVC
Edited SymbolicModelAdapter.h, added an alternative implementation for log2 (NOT part of C90, not of Cxx!)
Edited Program.cpp, promoted vars from int to uint to conquer warnings related to loss of precision
Likewise in DeterministicSparseTransitionParser.cpp, IntegerConstantExpression.h

Edited storm.cpp, reimplemented Usage-Query for non-Unix platforms.
Edited CuddUtility.h, added an include for int Type definitions as they do not fall from the sky
Edited ErrorHandling.h. reimplemented ErrorHandling for non-Unix platforms. Backtraces can not yet be provided.

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

src/adapters/SymbolicModelAdapter.h

@@ -16,6 +16,7 @@
 #include "cuddObj.hh"
 #include <iostream>
 #include <unordered_map>
+#include <cmath>
 
 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<uint_fast64_t>(std::ceil(std::log2(integerRange)));
+				uint_fast64_t numberOfDecisionDiagramVariables = static_cast<uint_fast64_t>(std::ceil(log2(integerRange)));
 
 				std::vector<ADD*> allRowDecisionDiagramVariablesForVariable;
 				std::vector<ADD*> allColumnDecisionDiagramVariablesForVariable;

src/ir/Program.cpp

@@ -119,24 +119,24 @@ std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> P
 }
 
 std::string Program::getVariableString() const {
-	std::map<unsigned int, std::string> bools;
-	std::map<unsigned int, std::string> ints;
-	unsigned maxInt = 0, maxBool = 0;
+	std::map<uint_fast64_t, std::string> bools;
+	std::map<uint_fast64_t, std::string> 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();
 }
 

src/ir/expressions/IntegerConstantExpression.h

@@ -62,7 +62,7 @@ public:
 		return defined;
 	}
 
-	int getValue() {
+	int_fast64_t getValue() {
 		return value;
 	}
 

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;

src/storm.cpp

@@ -45,17 +45,47 @@
 
 #include "src/exceptions/InvalidSettingsException.h"
 
-#include <sys/time.h>
-#include <sys/resource.h>
 #include <iostream>
 #include <iomanip>
 
 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
 }
 
 

src/utility/CuddUtility.h

@@ -10,6 +10,8 @@
 
 #include "cuddObj.hh"
 
+#include "boost/integer/integer_mask.hpp"
+
 namespace storm {
 
 namespace utility {

src/utility/ErrorHandling.h

@@ -8,9 +8,9 @@
 #ifndef ERRORHANDLING_H
 #define	ERRORHANDLING_H
 
+#include "src/utility/OsDetection.h"
 #include <signal.h>
-#include <execinfo.h>
-#include <cxxabi.h>
+
 
 /*
  * 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);
 }

src/utility/OsDetection.h

@@ -4,17 +4,32 @@
 #if defined __linux__ || defined __linux
 #	define LINUX
 #	include <sys/mman.h>
+#include <execinfo.h> // Required by ErrorHandling.h
+#include <cxxabi.h> // Required by ErrorHandling.h
+#include <sys/time.h> // Required by storm.cpp, Memory Usage
+#include <sys/resource.h> // Required by storm.cpp, Memory Usage
 #elif defined TARGET_OS_MAC || defined __apple__ || defined __APPLE__
 #	define MACOSX
 #	define _DARWIN_USE_64_BIT_INODE
 #	include <sys/mman.h>
 #	include <unistd.h>
+#	include <execinfo.h> // Required by ErrorHandling.h
+#	include <cxxabi.h> // Required by ErrorHandling.h
+#	include <sys/time.h> // Required by storm.cpp, Memory Usage
+#	include <sys/resource.h> // Required by storm.cpp, Memory Usage
 #elif defined _WIN32 || defined _WIN64
 #	define WINDOWS
 #	define NOMINMAX
 #	include <Windows.h>
 #	include <winnt.h>
+#	include <DbgHelp.h>
+#	include <Psapi.h>
 #	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