diff --git a/CMakeLists.txt b/CMakeLists.txt index 84173c8dc..8caf0b081 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -194,9 +194,9 @@ configure_file ( "${PROJECT_BINARY_DIR}/storm-config.h" ) -add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab +add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab DEPENDS storm) -add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests +add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-tests -v --fix-deadlocks DEPENDS storm-tests) set (CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams) diff --git a/FindPantheios.cmake b/FindPantheios.cmake deleted file mode 100644 index bfc5f39ad..000000000 --- a/FindPantheios.cmake +++ /dev/null @@ -1,466 +0,0 @@ -# Locate the Pantheois Logging Framework. -# -# Defines the following variables: -# -# PANTHEIOS_FOUND - Found the Pantheios Logging Framework -# PANTHEIOS_INCLUDE_DIRS - Include directories -# -# Accepts the following variables as input: -# -# PANTHEIOS_ROOT - (as a CMake or environment variable) -# The root directory of the pantheios install prefix -# -# PANTHEIOS_USE_DYNAMIC_RUNTIME -# -# If you want to use splitting, specify LRSplit and than preface the components with L and R, so e.g. LRSplit LFile RSyslog -# To use more than one BackEnd, specify NBackEnd followed by a list of components. NBackEnd requires the NFrontEnd. -# -# Possible Components for BackEnd: -# ACELogger -# COMErrorObject -# File -# FileCallback -# FPrintf -# FPrintfCallback -# Null -# Speech -# Syslog -# WindowsConsole -# WindowsConsoleCallback -# WindowsDebugger -# WindowsDebuggerCallback -# WindowsEventLog -# WindowsMessageBox -# WindowsSyslog -# WindowsSyslogCallback -# -# Possible components for FrontEnd: -# NoFrontEnd -# SimpleFrontEnd -# NFrontEnd -# -# - -#============================================================================= -# Copyright 2012 Philipp Berger -# -# Distributed under the OSI-approved BSD License (the "License"); -# see accompanying file Copyright.txt for details. -# -# This software is distributed WITHOUT ANY WARRANTY; without even the -# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. -# See the License for more information. -#============================================================================= -# (To distribute this file outside of CMake, substitute the full -# License text for the above reference.) -# -# Credits: -# -# HUGE thanks to Michael Wild -# Additional thanks to: -# Mateusz Loskot -# Rolf Eike Beer - - - -# default for WideString option -set(PANTHEIOS_WIDESTRING 0) -# default for Front- and BackEnd -set(PANTHEIOS_FRONTEND "simple") -set(PANTHEIOS_BACKEND "file") -set(PANTHEIOS_BACKEND_L OFF) -set(PANTHEIOS_BACKEND_R OFF) -set(PANTHEIOS_BACKEND_LIST) - -# Use FIND_PACKAGE( Pantheios COMPONENTS ... ) to enable modules -if( Pantheios_FIND_COMPONENTS ) - list(FIND Pantheios_FIND_COMPONENTS "LRSplit" PANTHEIOS_use_lrsplit) - list(FIND Pantheios_FIND_COMPONENTS "NFrontEnd" PANTHEIOS_use_nfe) - list(FIND Pantheios_FIND_COMPONENTS "NBackEnd" PANTHEIOS_use_nbe) - list(FIND Pantheios_FIND_COMPONENTS "WideString" PANTHEIOS_use_ws) - - list(REMOVE_ITEM Pantheios_FIND_COMPONENTS "LRSplit" "NFrontEnd" "NBackEnd" "WideString") - - if (NOT PANTHEIOS_use_ws EQUAL -1) - # Use WideString - set(PANTHEIOS_WIDESTRING 1) - endif() - - if (NOT PANTHEIOS_use_lrsplit EQUAL -1) - # Found LRSplit - set(PANTHEIOS_BACKEND "lrsplit") - if (NOT PANTHEIOS_use_nbe EQUAL -1) - # Also found NBe - message(FATAL_ERROR "Pantheios: Use either LRSplit or NBackEnd, not both.") - endif() - if (NOT PANTHEIOS_use_nfe EQUAL -1) - # Also found NFe - message(FATAL_ERROR "Pantheios: Use either LRSplit or NFrontEnd, not both.") - endif() - - foreach( component ${Pantheios_FIND_COMPONENTS} ) - # LRSplit L BackEnds - string(SUBSTRING ${component} 0 1 _sub_comp_head) - string(LENGTH ${component} _length_comp) - math(EXPR _length_comp_tail "${_length_comp} - 1") - string(SUBSTRING ${component} 1 ${_length_comp_tail} _sub_comp_tail) - - if ((_sub_comp_tail STREQUAL "ACELogger") OR (_sub_comp_tail STREQUAL "COMErrorObject") OR (_sub_comp_tail STREQUAL "File") OR (_sub_comp_tail STREQUAL "FileCallback") OR (_sub_comp_tail STREQUAL "FPrintf") OR (_sub_comp_tail STREQUAL "FPrintfCallback") OR (_sub_comp_tail STREQUAL "Null") OR (_sub_comp_tail STREQUAL "Speech") OR (_sub_comp_tail STREQUAL "Syslog") OR (_sub_comp_tail STREQUAL "WindowsConsole") OR (_sub_comp_tail STREQUAL "WindowsConsoleCallback") OR (_sub_comp_tail STREQUAL "WindowsDebugger") OR (_sub_comp_tail STREQUAL "WindowsDebuggerCallback") OR (_sub_comp_tail STREQUAL "WindowsEventLog") OR (_sub_comp_tail STREQUAL "WindowsMessageBox") OR (_sub_comp_tail STREQUAL "WindowsSyslog") OR (_sub_comp_tail STREQUAL "WindowsSyslogCallback")) - if ((_sub_comp_head STREQUAL L) OR (_sub_comp_head STREQUAL R)) - message(STATUS "Pantheios: Setting LRSplit BackEnd ${_sub_comp_head} to ${_sub_comp_tail}") - string(TOLOWER ${_sub_comp_tail} _sub_comp_tail_low) - set(PANTHEIOS_BACKEND_${_sub_comp_head} "${_sub_comp_tail_low}") - else () - message(FATAL_ERROR "Pantheios: Internal Parsing Error") - endif() - - # FrontEnds - elseif (component STREQUAL "NoFrontEnd") - message(STATUS "Pantheios: Setting FrontEnd to NoFrontEnd") - set(PANTHEIOS_FRONTEND "null") - elseif (component STREQUAL "SimpleFrontEnd") - message(STATUS "Pantheios: Setting FrontEnd to SimpleFrontEnd") - set(PANTHEIOS_FRONTEND "simple") - - else () - message(FATAL_ERROR "Unknown Component: ${component}") - endif () - endforeach(component) - elseif (NOT PANTHEIOS_use_nbe EQUAL -1) - # Found NBackEnd - if (PANTHEIOS_use_nfe EQUAL -1) - message(FATAL_ERROR "Pantheios: Usage of NBackEnd requires the NFrontEnd.") - endif() - set(PANTHEIOS_BACKEND "N") - set(PANTHEIOS_FRONTEND "N") - - foreach( component ${Pantheios_FIND_COMPONENTS} ) - # Std BackEnds - if ((component STREQUAL "ACELogger") OR (component STREQUAL "COMErrorObject") OR (component STREQUAL "File") OR (component STREQUAL "FileCallback") OR (component STREQUAL "FPrintf") OR (component STREQUAL "FPrintfCallback") OR (component STREQUAL "Null") OR (component STREQUAL "Speech") OR (component STREQUAL "Syslog") OR (component STREQUAL "WindowsConsole") OR (component STREQUAL "WindowsConsoleCallback") OR (component STREQUAL "WindowsDebugger") OR (component STREQUAL "WindowsDebuggerCallback") OR (component STREQUAL "WindowsEventLog") OR (component STREQUAL "WindowsMessageBox") OR (component STREQUAL "WindowsSyslog") OR (component STREQUAL "WindowsSyslogCallback")) - message(STATUS "Pantheios: Adding BackEnd ${component}") - string(TOLOWER ${component} _low_comp) - list(APPEND PANTHEIOS_BACKEND_LIST ${_low_comp}) - else () - message(FATAL_ERROR "Unknown Component: ${component}") - endif () - endforeach(component) - else () - # Simple, one FE, one BE - foreach( component ${Pantheios_FIND_COMPONENTS} ) - if ((component STREQUAL "ACELogger") OR (component STREQUAL "COMErrorObject") OR (component STREQUAL "File") OR (component STREQUAL "FileCallback") OR (component STREQUAL "FPrintf") OR (component STREQUAL "FPrintfCallback") OR (component STREQUAL "Null") OR (component STREQUAL "Speech") OR (component STREQUAL "Syslog") OR (component STREQUAL "WindowsConsole") OR (component STREQUAL "WindowsConsoleCallback") OR (component STREQUAL "WindowsDebugger") OR (component STREQUAL "WindowsDebuggerCallback") OR (component STREQUAL "WindowsEventLog") OR (component STREQUAL "WindowsMessageBox") OR (component STREQUAL "WindowsSyslog") OR (component STREQUAL "WindowsSyslogCallback")) - message(STATUS "Pantheios: Setting BackEnd to ${component}") - string(TOLOWER ${component} _low_comp) - set(PANTHEIOS_BACKEND ${_low_comp}) - - # FrontEnds - elseif (component STREQUAL "NoFrontEnd") - message(STATUS "Pantheios: Setting FrontEnd to NoFrontEnd") - set(PANTHEIOS_FRONTEND "null") - elseif (component STREQUAL "SimpleFrontEnd") - message(STATUS "Pantheios: Setting FrontEnd to SimpleFrontEnd") - set(PANTHEIOS_FRONTEND "simple") - else () - message(FATAL_ERROR "Unknown Component: ${component}") - endif () - endforeach(component) - endif () -endif(Pantheios_FIND_COMPONENTS) - -if (PANTHEIOS_USE_DYNAMIC_RUNTIME) - set(PANTHEIOS_LIB_LINKTYPE "dll") -else () - set(PANTHEIOS_LIB_LINKTYPE "mt") -endif () - -if(PANTHEIOS_INCLUDE_DIR) - if (NOT PANTHEIOS_ROOT) - get_filename_component(PANTHEIOS_ROOT "${PANTHEIOS_INCLUDE_DIR}" PATH) - endif() - - get_filename_component(PANTHEIOS_ROOT_HINT "${PANTHEIOS_INCLUDE_DIR}" PATH) -endif() - -find_path(PANTHEIOS_INCLUDE_DIR pantheios/pantheios.h - PATH_SUFFIXES include - HINTS ${PANTHEIOS_ROOT} ${PANTHEIOS_ROOT_HINT} - ENV PANTHEIOS_ROOT -) - -# No idea what the stuff for ICC et. al. is, so I don't handle it here... -set(_P_COMP_TAG) -set(_P_OS_TAG) -set(_P_ARCH_TAG) -if(MSVC) - if(MSVC60) - set(_P_COMP_TAG vc6) - elseif(MSVC70) - set(_P_COMP_TAG vc7) - elseif(MSVC71) - set(_P_COMP_TAG vc71) - elseif(MSVC80) - set(_P_COMP_TAG vc8) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - set(_P_ARCH_TAG .x64) - endif() - elseif(MSVC90) - set(_P_COMP_TAG vc9) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - set(_P_ARCH_TAG .x64) - endif() - elseif(MSVC10) - set(_P_COMP_TAG vc10) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - set(_P_ARCH_TAG .x64) - endif() - elseif(MSVC11) - set(_P_COMP_TAG vc11) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - set(_P_ARCH_TAG .x64) - endif() - endif() -elseif(CMAKE_COMPILER_IS_GNUCC) - execute_process(COMMAND ${CMAKE_C_COMPILER} -dumpversion OUTPUT_VARIABLE GCC_VERSION) - string(REGEX MATCHALL "[0-9]+" GCC_VERSION_COMPONENTS ${GCC_VERSION}) - list(GET GCC_VERSION_COMPONENTS 0 GCC_MAJOR) - list(GET GCC_VERSION_COMPONENTS 1 GCC_MINOR) - set(_P_COMP_TAG gcc${GCC_MAJOR}${GCC_MINOR}) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - set(_P_ARCH_TAG .file64bit) - endif() -else() - message(FATAL_ERROR "Pantheios: Your compiler/environment is currently unsupported.") -endif() - -set(_P_LIB_TAG ${_P_COMP_TAG}${_P_OS_TAG}${_P_ARCH_TAG}) - -# Is this the right way? -set(PANTHEIOS_INCLUDE_DIRS ${PANTHEIOS_INCLUDE_DIR}) - -set(_P_REQUIRED_LIBVARS) -set(PANTHEIOS_LIBRARIES) -set(PANTHEIOS_LIBRARIES_DEBUG) -set(PANTHEIOS_LIBRARIES_RELEASE) - - -#core and util libraries -foreach(l core util) - find_library(PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY - pantheios.1.${l}.${_P_LIB_TAG}.${PANTHEIOS_LIB_LINKTYPE}.debug - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - find_library(PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY - pantheios.1.${l}.${_P_LIB_TAG}.${PANTHEIOS_LIB_LINKTYPE} - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY - PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY - ) - list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY} - ) -endforeach() - -# set PANTHEIOS_LIBRARY_DIRS -get_filename_component(PANTHEIOS_LIBRARY_DIRS ${PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY} PATH) - - - -# backend libraries (split, sole, local, remote and common) -set(_P_LT ${PANTHEIOS_LIB_LINKTYPE}) -set(_P_BE ${PANTHEIOS_BACKEND}) - -find_library(PANTHEIOS_be_${_P_BE}_${_P_LT}_DEBUG_LIBRARY - pantheios.1.be.${_P_BE}.${_P_LIB_TAG}.${_P_LT}.debug - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT -) - -find_library(PANTHEIOS_be_${_P_BE}_${_P_LT}_LIBRARY - pantheios.1.be.${_P_BE}.${_P_LIB_TAG}.${_P_LT} - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT -) - -list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_be_${_P_BE}_${_P_LT}_DEBUG_LIBRARY - PANTHEIOS_be_${_P_BE}_${_P_LT}_LIBRARY -) -list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_be_${_P_BE}_${_P_LT}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_be_${_P_BE}_${_P_LT}_LIBRARY} -) - -if (_P_BE STREQUAL N) - # N Backend, go through list - message(STATUS "Pantheios: Dbg: Lib-n") - - foreach (blib PANTHEIOS_BACKEND_LIST) - find_library(PANTHEIOS_bec_${blib}_${_P_LT}_DEBUG_LIBRARY - pantheios.1.bec.${blib}.${_P_LIB_TAG}.${_P_LT}.debug - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - find_library(PANTHEIOS_bec_${blib}_${_P_LT}_LIBRARY - pantheios.1.bec.${blib}.${_P_LIB_TAG}.${_P_LT} - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_bec_${blib}_${_P_LT}_DEBUG_LIBRARY - PANTHEIOS_bec_${blib}_${_P_LT}_LIBRARY - ) - list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_bec_${blib}_${_P_LT}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_bec_${blib}_${_P_LT}_LIBRARY} - ) - endforeach() -elseif (_P_BE STREQUAL lrsplit) - # LRSplit - message(STATUS "Pantheios: Dbg: Lib-lrsplit") - - # Left side - foreach (t bec bel) - find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_DEBUG_LIBRARY - pantheios.1.${t}.${PANTHEIOS_BACKEND_L}.${_P_LIB_TAG}.${_P_LT}.debug - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_LIBRARY - pantheios.1.${t}.${PANTHEIOS_BACKEND_L}.${_P_LIB_TAG}.${_P_LT} - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_DEBUG_LIBRARY - PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_LIBRARY - ) - list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_LIBRARY} - ) - endforeach() - # Right side - foreach (t bec ber) - find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_DEBUG_LIBRARY - pantheios.1.${t}.${PANTHEIOS_BACKEND_R}.${_P_LIB_TAG}.${_P_LT}.debug - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_LIBRARY - pantheios.1.${t}.${PANTHEIOS_BACKEND_R}.${_P_LIB_TAG}.${_P_LT} - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_DEBUG_LIBRARY - PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_LIBRARY - ) - list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_LIBRARY} - ) - endforeach() -else () - # normal - message(STATUS "Pantheios: Dbg: Lib-normal") - foreach (t bec) - find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_DEBUG_LIBRARY - pantheios.1.${t}.${PANTHEIOS_BACKEND}.${_P_LIB_TAG}.${_P_LT}.debug - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_LIBRARY - pantheios.1.${t}.${PANTHEIOS_BACKEND}.${_P_LIB_TAG}.${_P_LT} - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_DEBUG_LIBRARY - PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_LIBRARY - ) - list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_LIBRARY} - ) - endforeach() -endif() - -# frontent libraries -set(PANTHEIOS_fe_DEBUG_LIBRARY) -set(PANTHEIOS_fe_LIBRARY) -if(NOT PANTHEIOS_FRONTENT STREQUAL null) - set(_P_FE ${PANTHEIOS_FRONTEND}) - find_library(PANTHEIOS_${_P_FE}_${_P_LT}_DEBUG_LIBRARY - pantheios.1.fe.${_P_FE}.${_P_LIB_TAG}.${_P_LT}.debug - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - find_library(PANTHEIOS_${_P_FE}_${_P_LT}_LIBRARY - pantheios.1.fe.${_P_FE}.${_P_LIB_TAG}.${_P_LT} - PATH_SUFFIXES lib - HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT} - ENV PANTHEIOS_ROOT - ) - - list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_${_P_FE}_${_P_LT}_DEBUG_LIBRARY - PANTHEIOS_${_P_FE}_${_P_LT}_LIBRARY - ) - list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_${_P_FE}_${_P_LT}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_${_P_FE}_${_P_LT}_LIBRARY} - ) -endif() - -# gcc needs the core library mentioned a second time at the end -# (see Pantheios FAQ Q/A8) -# At this point, the core has to be found already, -# so only the additions to the lists are repeated here... -if(CMAKE_COMPILER_IS_GNUCC) - list(APPEND _P_REQUIRED_LIBVARS - PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY - PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY - ) - list(APPEND PANTHEIOS_LIBRARIES - debug ${PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY} - optimized ${PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY} - ) -endif() - -# copy to NAME_LIBS -set(PANTHEIOS_LIBS ${PANTHEIOS_LIBRARIES}) - -# handle the QUIETLY and REQUIRED arguments and set Pantheios_FOUND to TRUE if -# all listed variables are TRUE -include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(Pantheios - REQUIRED_VARS PANTHEIOS_INCLUDE_DIR ${_P_REQUIRED_LIBVARS} -) - -message(STATUS ${PANTHEIOS_INCLUDE_DIR} ${PANTHEIOS_LIBRARIES}) -mark_as_advanced(PANTHEIOS_INCLUDE_DIR PANTHEIOS_LIBRARIES) - diff --git a/FindSTLSoft.cmake b/FindSTLSoft.cmake deleted file mode 100644 index 5499ff851..000000000 --- a/FindSTLSoft.cmake +++ /dev/null @@ -1,56 +0,0 @@ -# Locate the STLSoft Headers. -# -# Defines the following variables: -# -# STLSOFT_FOUND - Found the Pantheios Logging Framework -# STLSOFT_INCLUDE_DIRS - Include directories -# -# Accepts the following variables as input: -# -# STLSOFT_ROOT - (as a CMake or environment variable) -# The root directory of the STLSoft install prefix -# -# - -#============================================================================= -# Copyright 2012 Philipp Berger -# -# Distributed under the OSI-approved BSD License (the "License"); -# see accompanying file Copyright.txt for details. -# -# This software is distributed WITHOUT ANY WARRANTY; without even the -# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. -# See the License for more information. -#============================================================================= -# (To distribute this file outside of CMake, substitute the full -# License text for the above reference.) -# - - - - -if(STLSOFT_INCLUDE_DIR) - if (NOT STLSOFT_ROOT) - get_filename_component(STLSOFT_ROOT "${STLSOFT_INCLUDE_DIR}" PATH) - endif() - - get_filename_component(STLSOFT_ROOT_HINT "${STLSOFT_INCLUDE_DIR}" PATH) -endif() - -find_path(STLSOFT_INCLUDE_DIR stlsoft/stlsoft.h - PATH_SUFFIXES include - HINTS ${STLSOFT_ROOT} ${STLSOFT_ROOT_HINT} - ENV STLSOFT_ROOT -) -set(STLSOFT_INCLUDE_DIRS ${STLSOFT_INCLUDE_DIR}) - -# handle the QUIETLY and REQUIRED arguments and set STLSOFT_FOUND to TRUE if -# all listed variables are TRUE -include(FindPackageHandleStandardArgs) -FIND_PACKAGE_HANDLE_STANDARD_ARGS(STLSoft - REQUIRED_VARS STLSOFT_INCLUDE_DIR -) - - -mark_as_advanced(STLSOFT_INCLUDE_DIR) - diff --git a/LICENSE-MRMC.txt b/LICENSE-STORM.txt similarity index 100% rename from LICENSE-MRMC.txt rename to LICENSE-STORM.txt diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index 3fd990a46..482b8a16a 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -31,15 +31,16 @@ public: LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format."); // Prepare the resulting matrix. - gmm::csr_matrix* result = new gmm::csr_matrix(matrix.rowCount, matrix.rowCount); + gmm::csr_matrix* result = new gmm::csr_matrix(matrix.rowCount, matrix.colCount); // Copy Row Indications - std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), std::back_inserter(result->jc)); + std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), result->jc.begin()); // Copy Columns Indications result->ir.resize(realNonZeros); - std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), std::back_inserter(result->ir)); + std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), result->ir.begin()); // And do the same thing with the actual values. - std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), std::back_inserter(result->pr)); + result->pr.resize(realNonZeros); + std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), result->pr.begin()); LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format."); diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 6204605af..c673bbfaf 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -19,6 +19,7 @@ #include "src/models/Dtmc.h" #include "src/storage/BitVector.h" #include "src/exceptions/InvalidPropertyException.h" +#include "src/utility/Vector.h" #include #include "log4cplus/logger.h" diff --git a/src/models/AbstractModel.cpp b/src/models/AbstractModel.cpp index 70acd4e3a..43959a714 100644 --- a/src/models/AbstractModel.cpp +++ b/src/models/AbstractModel.cpp @@ -13,13 +13,13 @@ * @return Output stream os. */ std::ostream& storm::models::operator<<(std::ostream& os, storm::models::ModelType const type) { - switch (type) { - case storm::models::Unknown: os << "Unknown"; break; - case storm::models::DTMC: os << "DTMC"; break; - case storm::models::CTMC: os << "CTMC"; break; - case storm::models::MDP: os << "MDP"; break; - case storm::models::CTMDP: os << "CTMDP"; break; - default: os << "Invalid ModelType"; break; - } - return os; + switch (type) { + case storm::models::Unknown: os << "Unknown"; break; + case storm::models::DTMC: os << "DTMC"; break; + case storm::models::CTMC: os << "CTMC"; break; + case storm::models::MDP: os << "MDP"; break; + case storm::models::CTMDP: os << "CTMDP"; break; + default: os << "Invalid ModelType"; break; + } + return os; } diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index bb223b718..c35ecd3cc 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -24,7 +24,7 @@ std::ostream& operator<<(std::ostream& os, ModelType const type); * This is base class defines a common interface for all models to identify * their type and obtain the special model. */ -class AbstractModel { +class AbstractModel: public std::enable_shared_from_this { public: /*! @@ -44,7 +44,7 @@ class AbstractModel { */ template std::shared_ptr as() { - return std::dynamic_pointer_cast(std::shared_ptr(this)); + return std::dynamic_pointer_cast(shared_from_this()); } /*! diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 303a77739..c19208543 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -18,7 +18,7 @@ #include "src/storage/SparseMatrix.h" #include "src/exceptions/InvalidArgumentException.h" #include "src/utility/CommandLine.h" - +#include "src/utility/Settings.h" #include "src/models/AbstractModel.h" namespace storm { @@ -49,8 +49,15 @@ public: : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), backwardTransitions(nullptr) { - if (!this->checkValidityProbabilityMatrix()) { - std::cerr << "Probability matrix is invalid" << std::endl; + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + if (this->transitionRewardMatrix != nullptr) { + if (!this->transitionRewardMatrix->isSubmatrixOf(*(this->probabilityMatrix))) { + LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); + throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions."; + } } } @@ -65,9 +72,7 @@ public: if (dtmc.backwardTransitions != nullptr) { this->backwardTransitions = new storm::models::GraphTransitions(*dtmc.backwardTransitions); } - if (!this->checkValidityProbabilityMatrix()) { - std::cerr << "Probability matrix is invalid" << std::endl; - } + // no checks here, as they have already been performed for dtmc. } //! Destructor @@ -206,11 +211,27 @@ private: * * Checks probability matrix if all rows sum up to one. */ - bool checkValidityProbabilityMatrix() { + bool checkValidityOfProbabilityMatrix() { + // Get the settings object to customize linear solving. + storm::settings::Settings* s = storm::settings::instance(); + double precision = s->get("precision"); + + if (this->probabilityMatrix->getRowCount() != this->probabilityMatrix->getColumnCount()) { + // not square + LOG4CPLUS_ERROR(logger, "Probability matrix is not square."); + return false; + } + for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) { T sum = this->probabilityMatrix->getRowSum(row); - if (sum == 0) continue; - if (std::abs(sum - 1) > 1e-10) return false; + if (sum == 0) { + LOG4CPLUS_ERROR(logger, "Row " << row << " has sum 0"); + return false; + } + if (std::abs(sum - 1) > precision) { + LOG4CPLUS_ERROR(logger, "Row " << row << " has sum " << sum); + return false; + } } return true; } diff --git a/src/models/Mdp.h b/src/models/Mdp.h new file mode 100644 index 000000000..dc58782a2 --- /dev/null +++ b/src/models/Mdp.h @@ -0,0 +1,246 @@ +/* + * Mdp.h + * + * Created on: 14.01.2013 + * Author: Philipp Berger + */ + +#ifndef STORM_MODELS_MDP_H_ +#define STORM_MODELS_MDP_H_ + +#include +#include +#include +#include + +#include "AtomicPropositionsLabeling.h" +#include "GraphTransitions.h" +#include "src/storage/SparseMatrix.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/utility/CommandLine.h" +#include "src/utility/Settings.h" +#include "src/models/AbstractModel.h" + +namespace storm { + +namespace models { + +/*! + * This class represents a Markov Decision Process (MDP) whose states are + * labeled with atomic propositions. + */ +template +class Mdp : public storm::models::AbstractModel { + +public: + //! Constructor + /*! + * Constructs a MDP object from the given transition probability matrix and + * the given labeling of the states. + * @param probabilityMatrix The transition probability relation of the + * MDP given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic + * propositions to each state. + */ + Mdp(std::shared_ptr> probabilityMatrix, + std::shared_ptr stateLabeling, + std::shared_ptr> stateRewards = nullptr, + std::shared_ptr> transitionRewardMatrix = nullptr) + : probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), + stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), + backwardTransitions(nullptr) { + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + //! Copy Constructor + /*! + * Copy Constructor. Performs a deep copy of the given MDP. + * @param mdp A reference to the MDP that is to be copied. + */ + Mdp(const Mdp &mdp) : probabilityMatrix(mdp.probabilityMatrix), + stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards), + transitionRewardMatrix(mdp.transitionRewardMatrix) { + if (mdp.backwardTransitions != nullptr) { + this->backwardTransitions = new storm::models::GraphTransitions(*mdp.backwardTransitions); + } + if (!this->checkValidityOfProbabilityMatrix()) { + LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); + throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; + } + } + + //! Destructor + /*! + * Destructor. Frees the matrix and labeling associated with this MDP. + */ + ~Mdp() { + if (this->backwardTransitions != nullptr) { + delete this->backwardTransitions; + } + } + + /*! + * Returns the state space size of the MDP. + * @return The size of the state space of the MDP. + */ + uint_fast64_t getNumberOfStates() const { + return this->probabilityMatrix->getColumnCount(); + } + + /*! + * Returns the number of (non-zero) transitions of the MDP. + * @return The number of (non-zero) transitions of the MDP. + */ + uint_fast64_t getNumberOfTransitions() const { + return this->probabilityMatrix->getNonZeroEntryCount(); + } + + /*! + * Returns a bit vector in which exactly those bits are set to true that + * correspond to a state labeled with the given atomic proposition. + * @param ap The atomic proposition for which to get the bit vector. + * @return A bit vector in which exactly those bits are set to true that + * correspond to a state labeled with the given atomic proposition. + */ + storm::storage::BitVector* getLabeledStates(std::string ap) const { + return this->stateLabeling->getAtomicProposition(ap); + } + + /*! + * Returns a pointer to the matrix representing the transition probability + * function. + * @return A pointer to the matrix representing the transition probability + * function. + */ + std::shared_ptr> getTransitionProbabilityMatrix() const { + return this->probabilityMatrix; + } + + /*! + * Returns a pointer to the matrix representing the transition rewards. + * @return A pointer to the matrix representing the transition rewards. + */ + std::shared_ptr> getTransitionRewardMatrix() const { + return this->transitionRewardMatrix; + } + + /*! + * Returns a pointer to the vector representing the state rewards. + * @return A pointer to the vector representing the state rewards. + */ + std::shared_ptr> getStateRewards() const { + return this->stateRewards; + } + + /*! + * + */ + std::set const getPropositionsForState(uint_fast64_t const &state) const { + return stateLabeling->getPropositionsForState(state); + } + + /*! + * Retrieves a reference to the backwards transition relation. + * @return A reference to the backwards transition relation. + */ + storm::models::GraphTransitions& getBackwardTransitions() { + if (this->backwardTransitions == nullptr) { + this->backwardTransitions = new storm::models::GraphTransitions(this->probabilityMatrix, false); + } + return *this->backwardTransitions; + } + + /*! + * Retrieves whether this MDP has a state reward model. + * @return True if this MDP has a state reward model. + */ + bool hasStateRewards() { + return this->stateRewards != nullptr; + } + + /*! + * Retrieves whether this MDP has a transition reward model. + * @return True if this MDP has a transition reward model. + */ + bool hasTransitionRewards() { + return this->transitionRewardMatrix != nullptr; + } + + /*! + * Retrieves whether the given atomic proposition is a valid atomic proposition in this model. + * @param atomicProposition The atomic proposition to be checked for validity. + * @return True if the given atomic proposition is valid in this model. + */ + bool hasAtomicProposition(std::string const& atomicProposition) { + return this->stateLabeling->containsAtomicProposition(atomicProposition); + } + + /*! + * Prints information about the model to the specified stream. + * @param out The stream the information is to be printed to. + */ + void printModelInformationToStream(std::ostream& out) const { + storm::utility::printSeparationLine(out); + out << std::endl; + out << "Model type: \t\tMDP" << std::endl; + out << "States: \t\t" << this->getNumberOfStates() << std::endl; + out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; + this->stateLabeling->printAtomicPropositionsInformationToStream(out); + out << "Size in memory: \t" + << (this->probabilityMatrix->getSizeInMemory() + + this->stateLabeling->getSizeInMemory() + + sizeof(*this))/1024 << " kbytes" << std::endl; + out << std::endl; + storm::utility::printSeparationLine(out); + } + + storm::models::ModelType getType() { + return MDP; + } + +private: + + /*! + * @brief Perform some sanity checks. + * + * Checks probability matrix if all rows sum up to one. + */ + bool checkValidityOfProbabilityMatrix() { + // Get the settings object to customize linear solving. + storm::settings::Settings* s = storm::settings::instance(); + double precision = s->get("precision"); + for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) { + T sum = this->probabilityMatrix->getRowSum(row); + if (sum == 0) continue; + if (std::abs(sum - 1) > precision) return false; + } + return true; + } + + /*! A matrix representing the transition probability function of the MDP. */ + std::shared_ptr> probabilityMatrix; + + /*! The labeling of the states of the MDP. */ + std::shared_ptr stateLabeling; + + /*! The state-based rewards of the MDP. */ + std::shared_ptr> stateRewards; + + /*! The transition-based rewards of the MDP. */ + std::shared_ptr> transitionRewardMatrix; + + /*! + * A data structure that stores the predecessors for all states. This is + * needed for backwards directed searches. + */ + storm::models::GraphTransitions* backwardTransitions; +}; + +} // namespace models + +} // namespace storm + +#endif /* STORM_MODELS_MDP_H_ */ diff --git a/src/parser/AtomicPropositionLabelingParser.h b/src/parser/AtomicPropositionLabelingParser.h index e2a24b6e9..8ca0413f8 100644 --- a/src/parser/AtomicPropositionLabelingParser.h +++ b/src/parser/AtomicPropositionLabelingParser.h @@ -24,7 +24,7 @@ class AtomicPropositionLabelingParser : Parser { std::shared_ptr getLabeling() { return this->labeling; } - + private: std::shared_ptr labeling; }; diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index f52b2cf8e..110831ff6 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -5,7 +5,8 @@ #include "src/exceptions/WrongFileFormatException.h" #include "src/models/AbstractModel.h" -#include "src/parser/DtmcParser.h" +#include "src/parser/DeterministicModelParser.h" +#include "src/parser/MdpParser.h" namespace storm { namespace parser { @@ -26,20 +27,29 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con // Do actual parsing switch (type) { case storm::models::DTMC: { - DtmcParser* parser = new DtmcParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - this->model = parser->getDtmc(); - break; - } - case storm::models::CTMC: + DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getDtmc(); break; - case storm::models::MDP: + } + case storm::models::CTMC: { + DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getCtmc(); break; + } + case storm::models::MDP: { + MdpParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getMdp(); + break; + } case storm::models::CTMDP: break; default: ; // Unknown } - if (!this->model) std::cout << "model is still null" << std::endl; + + if (!this->model) { + LOG4CPLUS_WARN(logger, "Model is still null."); + } } storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) { diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h index d609f10dc..1424cb9b7 100644 --- a/src/parser/AutoParser.h +++ b/src/parser/AutoParser.h @@ -14,7 +14,7 @@ namespace parser { /*! * @brief Checks the given files and parses the model within these files. * - * This parser analyzes the format hitn in the first line of the transition + * This parser analyzes the format hint in the first line of the transition * file. If this is a valid format, it will use the parser for this format, * otherwise it will throw an exception. * diff --git a/src/parser/DtmcParser.cpp b/src/parser/DeterministicModelParser.cpp similarity index 70% rename from src/parser/DtmcParser.cpp rename to src/parser/DeterministicModelParser.cpp index b47b982e8..2372cde3e 100644 --- a/src/parser/DtmcParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -1,11 +1,11 @@ /* - * DtmcParser.cpp + * DeterministicModelParser.cpp * * Created on: 19.12.2012 * Author: thomas */ -#include "src/parser/DtmcParser.h" +#include "src/parser/DeterministicModelParser.h" #include #include @@ -27,25 +27,29 @@ namespace parser { * @param stateRewardFile String containing the location of the state reward file (...srew) * @param transitionRewardFile String containing the location of the transition reward file (...trew) */ -DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, +DeterministicModelParser::DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { storm::parser::DeterministicSparseTransitionParser tp(transitionSystemFile); - uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); - - std::shared_ptr> stateRewards = nullptr; - std::shared_ptr> transitionRewards = nullptr; + this->transitionSystem = tp.getMatrix(); + + uint_fast64_t stateCount = this->transitionSystem->getRowCount(); storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); + this->labeling = lp.getLabeling(); + + this->stateRewards = nullptr; + this->transitionRewards = nullptr; + if (stateRewardFile != "") { storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); - stateRewards = srp.getStateRewards(); + this->stateRewards = srp.getStateRewards(); } if (transitionRewardFile != "") { storm::parser::DeterministicSparseTransitionParser trp(transitionRewardFile); - transitionRewards = trp.getMatrix(); + this->transitionRewards = trp.getMatrix(); } - - dtmc = std::shared_ptr>(new storm::models::Dtmc(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); + this->dtmc = nullptr; + this->ctmc = nullptr; } } /* namespace parser */ diff --git a/src/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h new file mode 100644 index 000000000..3065b0eb4 --- /dev/null +++ b/src/parser/DeterministicModelParser.h @@ -0,0 +1,62 @@ +/* + * DtmcParser.h + * + * Created on: 19.12.2012 + * Author: thomas + */ + +#ifndef STORM_PARSER_DETERMINISTICMODELPARSER_H_ +#define STORM_PARSER_DETERMINISTICMODELPARSER_H_ + +#include "src/parser/Parser.h" +#include "src/models/Dtmc.h" +#include "src/models/Ctmc.h" + +namespace storm { +namespace parser { + +/*! + * @brief Load label and transition file and return initialized dtmc or ctmc object. + * + * @Note This class creates a new Dtmc or Ctmc object that can + * be accessed via getDtmc() or getCtmc(). However, it will not delete this object! + * + * @Note The labeling representation in the file may use at most as much nodes as are specified in the transition system. + */ +class DeterministicModelParser: public storm::parser::Parser { + public: + DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + /*! + * @brief Get the parsed dtmc model. + */ + std::shared_ptr> getDtmc() { + if (this->dtmc == nullptr) { + this->dtmc = std::shared_ptr>(new storm::models::Dtmc(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); + } + return this->dtmc; + } + /*! + * @brief Get the parsed ctmc model. + */ + std::shared_ptr> getCtmc() { + if (this->ctmc == nullptr) { + this->ctmc = std::shared_ptr>(new storm::models::Ctmc(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); + } + return this->ctmc; + } + + private: + std::shared_ptr> transitionSystem; + std::shared_ptr labeling; + std::shared_ptr> stateRewards; + std::shared_ptr> transitionRewards; + + std::shared_ptr> dtmc; + std::shared_ptr> ctmc; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */ diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 32d2a7e9b..59eb336d7 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -44,7 +44,7 @@ namespace parser { * @param buf Data to scan. Is expected to be some char array. * @param maxnode Is set to highest id of all nodes. */ -uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& maxnode) { +uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) { uint_fast64_t non_zero = 0; /* @@ -68,7 +68,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas /* * Check all transitions for non-zero diagonal entrys. */ - uint_fast64_t row, lastrow = 0, col; + int_fast64_t row, lastrow = -1, col; double val; maxnode = 0; while (buf[0] != '\0') { @@ -89,7 +89,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, uint_fas * anyway) or add a self-loop (in this case, we'll need the * additional transition). */ - if (lastrow < row-1) non_zero += row - lastrow - 1; + if (lastrow < row - 1) non_zero += row - lastrow - 1; lastrow = row; /* * Read probability of this transition. @@ -132,7 +132,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st /* * Perform first pass, i.e. count entries that are not zero. */ - uint_fast64_t maxnode; + int_fast64_t maxnode; uint_fast64_t non_zero = this->firstPass(file.data, maxnode); /* * If first pass returned zero, the file format was wrong. @@ -170,7 +170,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } this->matrix->initialize(non_zero); - uint_fast64_t row, lastrow = 0, col; + int_fast64_t row, lastrow = -1, col; double val; bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); bool hadDeadlocks = false; @@ -192,7 +192,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st * Check if we skipped a node, i.e. if a node does not have any * outgoing transitions. */ - for (uint_fast64_t node = lastrow + 1; node < row; node++) { + for (int_fast64_t node = lastrow + 1; node < row; node++) { hadDeadlocks = true; if (fixDeadlocks) { this->matrix->addNextValue(node, node, 1); diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 1d699d0c8..099d0fa4a 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -26,7 +26,7 @@ class DeterministicSparseTransitionParser : public Parser { private: std::shared_ptr> matrix; - uint_fast64_t firstPass(char* buf, uint_fast64_t &maxnode); + uint_fast64_t firstPass(char* buf, int_fast64_t &maxnode); }; diff --git a/src/parser/DtmcParser.h b/src/parser/DtmcParser.h deleted file mode 100644 index 7cf45a335..000000000 --- a/src/parser/DtmcParser.h +++ /dev/null @@ -1,40 +0,0 @@ -/* - * DtmcParser.h - * - * Created on: 19.12.2012 - * Author: thomas - */ - -#ifndef DTMCPARSER_H_ -#define DTMCPARSER_H_ - -#include "src/parser/Parser.h" -#include "src/models/Dtmc.h" - -namespace storm { -namespace parser { - -/*! - * @brief Load label and transition file and return initialized dtmc object - * - * @Note This class creates a new Dtmc object that can - * be accessed via getDtmc(). However, it will not delete this object! - * - * @Note The labeling representation in the file may use at most as much nodes as are specified in the dtmc. - */ -class DtmcParser: public storm::parser::Parser { -public: - DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, - std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); - - std::shared_ptr> getDtmc() { - return this->dtmc; - } - -private: - std::shared_ptr> dtmc; -}; - -} /* namespace parser */ -} /* namespace storm */ -#endif /* DTMCPARSER_H_ */ diff --git a/src/parser/MdpParser.cpp b/src/parser/MdpParser.cpp new file mode 100644 index 000000000..f73c0b515 --- /dev/null +++ b/src/parser/MdpParser.cpp @@ -0,0 +1,53 @@ +/* + * MdpParser.cpp + * + * Created on: 14.01.2013 + * Author: Philipp Berger + */ + +#include "src/parser/MdpParser.h" + +#include +#include + +#include "src/parser/NonDeterministicSparseTransitionParser.h" +#include "src/parser/AtomicPropositionLabelingParser.h" +#include "src/parser/SparseStateRewardParser.h" + +namespace storm { +namespace parser { + +/*! + * Parses a transition file and a labeling file and produces a MDP out of them; a pointer to the mdp + * is saved in the field "mdp" + * Note that the labeling file may have at most as many nodes as the transition file! + * + * @param transitionSystemFile String containing the location of the transition file (....tra) + * @param labelingFile String containing the location of the labeling file (....lab) + * @param stateRewardFile String containing the location of the state reward file (...srew) + * @param transitionRewardFile String containing the location of the transition reward file (...trew) + */ +MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile, std::string const & transitionRewardFile) { + storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile); + uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); + + std::shared_ptr> stateRewards = nullptr; + std::shared_ptr> transitionRewards = nullptr; + + storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); + if (stateRewardFile != "") { + storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); + stateRewards = srp.getStateRewards(); + } + if (transitionRewardFile != "") { + storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile); + transitionRewards = trp.getMatrix(); + } + + mdp = std::shared_ptr>(new storm::models::Mdp(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); +} + +} /* namespace parser */ + +} /* namespace storm */ diff --git a/src/parser/MdpParser.h b/src/parser/MdpParser.h new file mode 100644 index 000000000..e64356dc9 --- /dev/null +++ b/src/parser/MdpParser.h @@ -0,0 +1,40 @@ +/* + * MdpParser.h + * + * Created on: 14.01.2013 + * Author: thomas + */ + +#ifndef STORM_PARSER_MDPPARSER_H_ +#define STORM_PARSER_MDPPARSER_H_ + +#include "src/parser/Parser.h" +#include "src/models/Mdp.h" + +namespace storm { +namespace parser { + +/*! + * @brief Load label and transition file and return initialized mdp object + * + * @Note This class creates a new Mdp object that can + * be accessed via getMdp(). However, it will not delete this object! + * + * @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. + */ +class MdpParser: public storm::parser::Parser { +public: + MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, + std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); + + std::shared_ptr> getMdp() { + return this->mdp; + } + +private: + std::shared_ptr> mdp; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_MDPPARSER_H_ */ diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NonDeterministicSparseTransitionParser.cpp index 394006f99..1eb270739 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.cpp +++ b/src/parser/NonDeterministicSparseTransitionParser.cpp @@ -49,7 +49,7 @@ namespace parser { * @param maxnode Is set to highest id of all nodes. * @return The number of non-zero elements. */ -uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode) { +uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) { /* * Check file header and extract number of transitions. */ @@ -77,8 +77,8 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_ /* * Read all transitions. */ - uint_fast64_t source, target; - uint_fast64_t lastsource = 0; + int_fast64_t source, target; + int_fast64_t lastsource = -1; uint_fast64_t nonzero = 0; double val; choices = 0; @@ -97,6 +97,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_ choices++; if (source > lastsource + 1) { nonzero += source - lastsource - 1; + choices += source - lastsource - 1; parsed_nonzero += source - lastsource - 1; } lastsource = source; @@ -169,7 +170,8 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s /* * Perform first pass, i.e. obtain number of columns, rows and non-zero elements. */ - uint_fast64_t maxnode, choices; + int_fast64_t maxnode; + uint_fast64_t choices; uint_fast64_t nonzero = this->firstPass(file.data, choices, maxnode); /* @@ -217,7 +219,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s /* * Parse file content. */ - uint_fast64_t source, target, lastsource = 0; + int_fast64_t source, target, lastsource = -1; uint_fast64_t curRow = 0; std::string choice; double val; @@ -240,7 +242,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s * outgoing transitions. If so, insert a self-loop. * Also add self-loops to rowMapping. */ - for (uint_fast64_t node = lastsource + 1; node < source; node++) { + for (int_fast64_t node = lastsource + 1; node < source; node++) { hadDeadlocks = true; if (fixDeadlocks) { this->rowMapping->insert(RowMapping::value_type(curRow, std::pair(node, ""))); diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NonDeterministicSparseTransitionParser.h index 5b487d5a2..592e2814f 100644 --- a/src/parser/NonDeterministicSparseTransitionParser.h +++ b/src/parser/NonDeterministicSparseTransitionParser.h @@ -35,7 +35,7 @@ class NonDeterministicSparseTransitionParser : public Parser { std::shared_ptr> matrix; std::shared_ptr rowMapping; - uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode); + uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode); }; diff --git a/src/parser/SparseStateRewardParser.h b/src/parser/SparseStateRewardParser.h index 3ed71e1c2..a6b3e1203 100644 --- a/src/parser/SparseStateRewardParser.h +++ b/src/parser/SparseStateRewardParser.h @@ -20,7 +20,7 @@ class SparseStateRewardParser : Parser { std::shared_ptr> getStateRewards() { return this->stateRewards; } - + private: std::shared_ptr> stateRewards; }; diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 091092824..66baf546e 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -69,13 +69,17 @@ public: * Returns the index of the current bit that is set to true. * @return The index of the current bit that is set to true. */ - uint_fast64_t operator*() const { return currentIndex; } + uint_fast64_t operator*() const { + return currentIndex; + } /*! * Compares the iterator with another iterator to determine whether * the iteration process has reached the end. */ - bool operator!=(const constIndexIterator& rhs) const { return currentIndex != rhs.currentIndex; } + bool operator!=(const constIndexIterator& rhs) const { + return currentIndex != rhs.currentIndex; + } private: /*! The bit vector to search for set bits. */ diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index cdb1392a4..308917481 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -25,10 +25,13 @@ extern log4cplus::Logger logger; // Forward declaration for adapter classes. -namespace storm { namespace adapters{ class GmmxxAdapter; } } - namespace storm { +namespace adapters{ +class GmmxxAdapter; +} +} +namespace storm { namespace storage { /*! @@ -49,7 +52,7 @@ public: * a row, we can simply iterate over the array (part) itself. */ typedef const uint_fast64_t * const constIndexIterator; - + /*! * Iterator type if we want to iterate over elements. */ @@ -91,7 +94,8 @@ public: * Constructs a square sparse matrix object with the given number rows * @param size The number of rows and cols in the matrix */ - SparseMatrix(uint_fast64_t size) : rowCount(size), colCount(size), nonZeroEntryCount(0), + SparseMatrix(uint_fast64_t size) + : rowCount(size), colCount(size), nonZeroEntryCount(0), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { } //! Copy Constructor @@ -114,12 +118,12 @@ public: LOG4CPLUS_ERROR(logger, "Unable to allocate internal storage."); throw std::bad_alloc(); } else { - std::copy(ssm.valueStorage.begin(), ssm.valueStorage.end(), std::back_inserter(valueStorage)); + std::copy(ssm.valueStorage.begin(), ssm.valueStorage.end(), valueStorage.begin()); // The elements that are not of the value type but rather the // index type may be copied directly. - std::copy(ssm.columnIndications.begin(), ssm.columnIndications.end(), std::back_inserter(columnIndications)); - std::copy(ssm.rowIndications.begin(), ssm.rowIndications.end(), std::back_inserter(rowIndications)); + std::copy(ssm.columnIndications.begin(), ssm.columnIndications.end(), columnIndications.begin()); + std::copy(ssm.rowIndications.begin(), ssm.rowIndications.end(), rowIndications.begin()); } } } @@ -208,7 +212,7 @@ public: // Try to prepare the internal storage and throw an error in case of // failure. - + // Get necessary pointers to the contents of the Eigen matrix. const T* valuePtr = eigenSparseMatrix.valuePtr(); const _Index* indexPtr = eigenSparseMatrix.innerIndexPtr(); @@ -319,7 +323,6 @@ public: throw storm::exceptions::OutOfRangeException("Trying to add a value at illegal position."); } - // If we switched to another row, we have to adjust the missing // entries in the row_indications array. if (row != lastRow) { @@ -416,8 +419,8 @@ public: /*! * Gets the matrix element at the given row and column to the given value. * NOTE: This function does not check the internal status for errors for performance reasons. - * WARNING: It is possible to modify through this function. Usage only valid - * for elements EXISTING in the sparse matrix! If the requested value does not exist, + * WARNING: It is possible to modify through this function. Usage only valid + * for elements EXISTING in the sparse matrix! If the requested value does not exist, * an exception will be thrown. * @param row The row in which the element is to be read. * @param col The column in which the element is to be read. @@ -663,8 +666,9 @@ public: uint_fast64_t rowEnd = rowIndications[row + 1]; if (rowStart >= rowEnd) { - LOG4CPLUS_ERROR(logger, "The row " << row << " can not be made absorbing, no state in row, would have to recreate matrix!"); - throw storm::exceptions::InvalidStateException("A row can not be made absorbing, no state in row, would have to recreate matrix!"); + this->print(); + LOG4CPLUS_ERROR(logger, "Cannot make row absorbing, because there is no entry in this row."); + throw storm::exceptions::InvalidStateException("Cannot make row absorbing, because there is no entry in this row."); } uint_fast64_t pseudoDiagonal = row % colCount; @@ -796,13 +800,15 @@ public: * value. */ void invertDiagonal() { + if (this->getRowCount() != this->getColumnCount()) { + throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!"; + } T one(1); for (uint_fast64_t row = 0; row < rowCount; ++row) { uint_fast64_t rowStart = rowIndications[row]; uint_fast64_t rowEnd = rowIndications[row + 1]; - uint_fast64_t pseudoDiagonal = row % colCount; while (rowStart < rowEnd) { - if (columnIndications[rowStart] == pseudoDiagonal) { + if (columnIndications[rowStart] == row) { valueStorage[rowStart] = one - valueStorage[rowStart]; break; } @@ -815,12 +821,14 @@ public: * Negates all non-zero elements that are not on the diagonal. */ void negateAllNonDiagonalElements() { + if (this->getRowCount() != this->getColumnCount()) { + throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!"; + } for (uint_fast64_t row = 0; row < rowCount; ++row) { uint_fast64_t rowStart = rowIndications[row]; uint_fast64_t rowEnd = rowIndications[row + 1]; - uint_fast64_t pseudoDiagonal = row % colCount; while (rowStart < rowEnd) { - if (columnIndications[rowStart] != pseudoDiagonal) { + if (columnIndications[rowStart] != row) { valueStorage[rowStart] = - valueStorage[rowStart]; } ++rowStart; @@ -880,6 +888,18 @@ public: return result; } + T getRowVectorProduct(uint_fast64_t row, std::vector& vector) { + T result = storm::utility::constGetZero();; + auto valueIterator = valueStorage.begin() + rowIndications[row]; + const auto valueIteratorEnd = valueStorage.begin() + rowIndications[row + 1]; + auto columnIterator = columnIndications.begin() + rowIndications[row]; + const auto columnIteratorEnd = columnIndications.begin() + rowIndications[row + 1]; + for (; valueIterator != valueIteratorEnd; ++valueIterator, ++columnIterator) { + result += *valueIterator * vector[*columnIterator]; + } + return result; + } + /*! * Returns the size of the matrix in memory measured in bytes. * @return The size of the matrix in memory measured in bytes. @@ -914,7 +934,7 @@ public: constIndexIterator endConstColumnIterator(uint_fast64_t row) const { return &(this->columnIndications[0]) + this->rowIndications[row + 1]; } - + /*! * Returns an iterator over the elements of the given row. The iterator * will include no zero entries. @@ -934,7 +954,7 @@ public: constIterator endConstIterator(uint_fast64_t row) const { return &(this->valueStorage[0]) + this->rowIndications[row + 1]; } - + /*! * @brief Calculate sum of all entries in given row. * @@ -951,13 +971,32 @@ public: return sum; } - void print() const { - std::cout << "entries: ----------------------------" << std::endl; - for (uint_fast64_t i = 0; i < rowCount; ++i) { - for (uint_fast64_t j = rowIndications[i]; j < rowIndications[i + 1]; ++j) { - std::cout << "(" << i << "," << columnIndications[j] << ") = " << valueStorage[j] << std::endl; + /*! + * @brief Checks if it is a submatrix of the given matrix. + * + * A matrix A is a submatrix of B if a value in A is only nonzero, if + * the value in B at the same position is also nonzero. Furthermore, A + * and B have to have the same size. + * @param matrix Matrix to check against. + * @return True iff this is a submatrix of matrix. + */ + bool isSubmatrixOf(SparseMatrix const & matrix) const { + if (this->getRowCount() != matrix.getRowCount()) return false; + if (this->getColumnCount() != matrix.getColumnCount()) return false; + + for (uint_fast64_t row = 0; row < this->getRowCount(); ++row) { + for (uint_fast64_t elem = rowIndications[row], elem2 = matrix.rowIndications[row]; elem < rowIndications[row + 1] && elem < matrix.rowIndications[row + 1]; ++elem, ++elem2) { + if (columnIndications[elem] < matrix.columnIndications[elem2]) return false; } } + return true; + } + + void print() const { + std::cout << "entries in (" << rowCount << "x" << colCount << " matrix):" << std::endl; + std::cout << rowIndications << std::endl; + std::cout << columnIndications << std::endl; + std::cout << valueStorage << std::endl; } private: @@ -1018,7 +1057,7 @@ private: setState(MatrixStatus::Error); } - /*! + /*! * Sets the internal status to the given state if the current state is not * the error state. * @param new_state The new state to be switched to. diff --git a/src/storm.cpp b/src/storm.cpp index 65c2b835a..250163f70 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -99,18 +99,15 @@ bool parseOptions(const int argc, const char* argv[]) { } catch (storm::exceptions::InvalidSettingsException& e) { std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; std::cout << std::endl << storm::settings::help; - delete s; return false; } if (s->isSet("help")) { std::cout << storm::settings::help; - delete s; return false; } if (s->isSet("test-prctl")) { storm::parser::PrctlParser parser(s->getString("test-prctl").c_str()); - delete s; return false; } @@ -133,9 +130,7 @@ bool parseOptions(const int argc, const char* argv[]) { * Function to perform some cleanup. */ void cleanUp() { - if (storm::settings::instance() != nullptr) { - delete storm::settings::instance(); - } + // nothing here } void testCheckingDie(storm::models::Dtmc& dtmc) { diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 3c9b3e4d3..26f733071 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -33,6 +33,8 @@ storm::settings::Settings* storm::settings::Settings::inst = nullptr; std::map< std::pair, std::shared_ptr > storm::settings::Settings::modules; +storm::settings::Destroyer storm::settings::Settings::destroyer; + /*! * The constructor fills the option descriptions, parses the * command line and the config file and puts the option values to @@ -46,7 +48,7 @@ std::map< std::pair, std::shared_ptrsecondRun(argc, argv, filename); // Finalize parsed options, check for specified requirements. - bpo::notify(this->vm); + if (!sloppy) { + bpo::notify(this->vm); + } LOG4CPLUS_DEBUG(logger, "Finished loading config."); } catch (bpo::reading_file e) { diff --git a/src/utility/Settings.h b/src/utility/Settings.h index b85ff9256..b35e893c4 100644 --- a/src/utility/Settings.h +++ b/src/utility/Settings.h @@ -27,6 +27,8 @@ namespace settings { namespace bpo = boost::program_options; + class Destroyer; + /*! * @brief Wrapper around boost::program_options to handle configuration options. * @@ -43,8 +45,7 @@ namespace settings { * option modules. An option module can be anything that implements the * interface specified by registerModule(). */ - class Settings - { + class Settings { public: /*! @@ -57,19 +58,19 @@ namespace settings { } /*! - * @brief Get value of string option + * @brief Get value of string option. */ inline const std::string& getString(std::string const & name) const { return this->get(name); } /*! - * @brief Check if an option is set + * @brief Check if an option is set. */ inline const bool isSet(std::string const & name) const { return this->vm.count(name) > 0; } - + /*! * @brief Register a new module. * @@ -118,17 +119,30 @@ namespace settings { // Store module. Settings::modules[ trigger ] = desc; } - + friend std::ostream& help(std::ostream& os); friend std::ostream& helpConfigfile(std::ostream& os); friend Settings* instance(); - friend Settings* newInstance(int const argc, char const * const argv[], char const * const filename); + friend Settings* newInstance(int const argc, char const * const argv[], char const * const filename, bool const sloppy = false); + friend Destroyer; private: /*! - * @brief Constructor. + * @brief Private constructor. + * + * This constructor is private, as noone should be able to create + * an instance manually, one should always use the + * newInstance() method. + */ + Settings(int const argc, char const * const argv[], char const * const filename, bool const sloppy); + + /*! + * @brief Private destructor. + * + * This destructor should be private, as noone should be able to destroy a singleton. + * The object is automatically destroyed when the program terminates by the destroyer. */ - Settings(int const argc, char const * const argv[], char const * const filename); + ~Settings() {} /*! * @brief Initialize options_description object. @@ -174,8 +188,35 @@ namespace settings { * @brief actual instance of this class. */ static Settings* inst; + + /*! + * @brief Destroyer object. + */ + static Destroyer destroyer; }; + /*! + * @brief Destroyer class for singleton object of Settings. + * + * The sole purpose of this class is to clean up the singleton object + * instance of Settings. The Settings class has a static member of this + * Destroyer type that gets cleaned up when the program terminates. In + * it's destructor, this object will remove the Settings instance. + */ + class Destroyer { + public: + /*! + * @brief Destructor. + * + * Free Settings::inst. + */ + ~Destroyer() { + if (Settings::inst != nullptr) { + delete Settings::inst; + } + } + }; + /*! * @brief Print usage help. */ @@ -200,9 +241,9 @@ namespace settings { * @param filename either NULL or name of config file * @return The new instance of Settings. */ - inline Settings* newInstance(int const argc, char const * const argv[], char const * const filename) { + inline Settings* newInstance(int const argc, char const * const argv[], char const * const filename, bool const sloppy) { if (Settings::inst != nullptr) delete Settings::inst; - Settings::inst = new Settings(argc, argv, filename); + Settings::inst = new Settings(argc, argv, filename, sloppy); return Settings::inst; } diff --git a/src/vector/dense_vector.h b/src/vector/dense_vector.h new file mode 100644 index 000000000..b118d8e5d --- /dev/null +++ b/src/vector/dense_vector.h @@ -0,0 +1,183 @@ +#ifndef MRMC_VECTOR_BITVECTOR_H_ +#define MRMC_VECTOR_BITVECTOR_H_ + +#include +#include +#include +#include "boost/integer/integer_mask.hpp" + +#include +#include + +#include "src/exceptions/invalid_state.h" +#include "src/exceptions/invalid_argument.h" +#include "src/exceptions/out_of_range.h" + +namespace mrmc { + +namespace vector { + +//! A Vector +/*! + A bit vector for boolean fields or quick selection schemas on Matrix entries. + Does NOT perform index bound checks! + */ +template +class DenseVector { + public: + //! Constructor + /*! + \param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize() + */ + BitVector(uint_fast64_t initial_length) { + bucket_count = initial_length / 64; + if (initial_length % 64 != 0) { + ++bucket_count; + } + bucket_array = new uint_fast64_t[bucket_count](); + + // init all 0 + for (uint_fast64_t i = 0; i < bucket_count; ++i) { + bucket_array[i] = 0; + } + } + + //! Copy Constructor + /*! + Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other. + @param bv A reference to the bit vector that should be copied from + */ + BitVector(const BitVector &bv) : bucket_count(bv.bucket_count) + { + pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor."); + bucket_array = new uint_fast64_t[bucket_count](); + memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count); + } + + ~BitVector() { + if (bucket_array != NULL) { + delete[] bucket_array; + } + } + + void resize(uint_fast64_t new_length) { + uint_fast64_t* tempArray = new uint_fast64_t[new_length](); + + // 64 bit/entries per uint_fast64_t + uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count); + memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize); + + bucket_count = new_length / 64; + if (new_length % 64 != 0) { + ++bucket_count; + } + + delete[] bucket_array; + bucket_array = tempArray; + } + + void set(const uint_fast64_t index, const bool value) { + uint_fast64_t bucket = index / 64; + // Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. + // MSVC: C4334, use 1i64 or cast to __int64. + // result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) + uint_fast64_t mask = 1; + mask = mask << (index % 64); + if (value) { + bucket_array[bucket] |= mask; + } else { + bucket_array[bucket] &= ~mask; + } + } + + bool get(const uint_fast64_t index) { + uint_fast64_t bucket = index / 64; + // Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. + // MSVC: C4334, use 1i64 or cast to __int64. + // result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) + uint_fast64_t mask = 1; + mask = mask << (index % 64); + return ((bucket_array[bucket] & mask) == mask); + } + + // Operators + BitVector operator &(BitVector const &bv) { + uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; + BitVector result(minSize * 64); + for (uint_fast64_t i = 0; i < minSize; ++i) { + result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i]; + } + + return result; + } + BitVector operator |(BitVector const &bv) { + uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; + BitVector result(minSize * 64); + for (uint_fast64_t i = 0; i < minSize; ++i) { + result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i]; + } + + return result; + } + + BitVector operator ^(BitVector const &bv) { + uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; + BitVector result(minSize * 64); + for (uint_fast64_t i = 0; i < minSize; ++i) { + result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i]; + } + + return result; + } + + BitVector operator ~() { + BitVector result(this->bucket_count * 64); + for (uint_fast64_t i = 0; i < this->bucket_count; ++i) { + result.bucket_array[i] = ~this->bucket_array[i]; + } + + return result; + } + + /*! + * Returns the number of bits that are set (to one) in this bit vector. + * @return The number of bits that are set (to one) in this bit vector. + */ + uint_fast64_t getNumberOfSetBits() { + uint_fast64_t set_bits = 0; + for (uint_fast64_t i = 0; i < bucket_count; i++) { +#ifdef __GNUG__ // check if we are using g++ and use built-in function if available + set_bits += __builtin_popcount (this->bucket_array[i]); +#else + uint_fast32_t cnt; + uint_fast64_t bitset = this->bucket_array[i]; + for (cnt = 0; bitset; cnt++) { + bitset &= bitset - 1; + } + set_bits += cnt; +#endif + } + return set_bits; + } + + /*! + * Returns the size of the bit vector in memory measured in bytes. + * @return The size of the bit vector in memory measured in bytes. + */ + uint_fast64_t getSizeInMemory() { + return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count; + } + + private: + uint_fast64_t bucket_count; + + /*! Array containing the boolean bits for each node, 64bits/64nodes per element */ + uint_fast64_t* bucket_array; + +}; + +} // namespace vector + +} // namespace mrmc + +#endif // MRMC_SPARSE_STATIC_SPARSE_MATRIX_H_ diff --git a/test/parser/ParseDtmcTest.cpp b/test/parser/ParseDtmcTest.cpp index be1dd1595..f5bd8f163 100644 --- a/test/parser/ParseDtmcTest.cpp +++ b/test/parser/ParseDtmcTest.cpp @@ -8,12 +8,12 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "src/parser/DtmcParser.h" +#include "src/parser/DeterministicModelParser.h" #include "src/utility/IoUtility.h" TEST(ParseDtmcTest, parseAndOutput) { - storm::parser::DtmcParser* dtmcParser; - ASSERT_NO_THROW(dtmcParser = new storm::parser::DtmcParser( + storm::parser::DeterministicModelParser* dtmcParser; + ASSERT_NO_THROW(dtmcParser = new storm::parser::DeterministicModelParser( STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra", STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp new file mode 100644 index 000000000..4147c0122 --- /dev/null +++ b/test/parser/ParseMdpTest.cpp @@ -0,0 +1,32 @@ +/* + * ParseMdpTest.cpp + * + * Created on: 14.01.2013 + * Author: Thomas Heinemann + */ + + +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/MdpParser.h" +#include "src/utility/IoUtility.h" + +TEST(ParseMdpTest, parseAndOutput) { + storm::parser::MdpParser* mdpParser; + ASSERT_NO_THROW(mdpParser = new storm::parser::MdpParser( + STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", + STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); + + std::shared_ptr> mdp = mdpParser->getMdp(); + std::shared_ptr> matrix = mdp->getTransitionProbabilityMatrix(); + + ASSERT_EQ(mdp->getNumberOfStates(), 3); + ASSERT_EQ(mdp->getNumberOfTransitions(), 11); + ASSERT_EQ(matrix->getRowCount(), 2 * 3); + ASSERT_EQ(matrix->getColumnCount(), 3); + + + delete mdpParser; +} + + diff --git a/test/mrmc-tests.cpp b/test/storm-tests.cpp similarity index 52% rename from test/mrmc-tests.cpp rename to test/storm-tests.cpp index 8f92bcd07..9165b68a8 100644 --- a/test/mrmc-tests.cpp +++ b/test/storm-tests.cpp @@ -6,6 +6,9 @@ #include "log4cplus/consoleappender.h" #include "log4cplus/fileappender.h" +#include "src/utility/Settings.h" +#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h" + log4cplus::Logger logger; /*! @@ -25,8 +28,36 @@ void setUpLogging() { // logger.addAppender(consoleLogAppender); } -int main(int argc, char** argv) { +/*! + * Function that parses the command line options. + * @param argc The argc argument of main(). + * @param argv The argv argument of main(). + * @return True iff the program should continue to run after parsing the options. + */ +bool parseOptions(int const argc, char const * const argv[]) { + storm::settings::Settings* s = nullptr; + try { + storm::settings::Settings::registerModule>(); + s = storm::settings::newInstance(argc, argv, nullptr, true); + } catch (storm::exceptions::InvalidSettingsException& e) { + std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl; + std::cout << std::endl << storm::settings::help; + return false; + } + + if (s->isSet("help")) { + std::cout << storm::settings::help; + return false; + } + + return true; +} + +int main(int argc, char* argv[]) { setUpLogging(); + if (!parseOptions(argc, argv)) { + return 0; + } std::cout << "STORM Testing Suite" << std::endl; testing::InitGoogleTest(&argc, argv);