From d5eb8ccfabadcfe10a873f9bc617399c5fcc6599 Mon Sep 17 00:00:00 2001 From: gereon Date: Sat, 12 Jan 2013 22:26:41 +0100 Subject: [PATCH 01/18] renamed mrmc-tests to storm-tests --- test/{mrmc-tests.cpp => storm-tests.cpp} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename test/{mrmc-tests.cpp => storm-tests.cpp} (100%) diff --git a/test/mrmc-tests.cpp b/test/storm-tests.cpp similarity index 100% rename from test/mrmc-tests.cpp rename to test/storm-tests.cpp From 9ca0acd0d65d8c596bff1ce12741c85e2e6310e7 Mon Sep 17 00:00:00 2001 From: gereon Date: Sat, 12 Jan 2013 22:30:07 +0100 Subject: [PATCH 02/18] removed obsolete cmake files, renamed license file --- FindPantheios.cmake | 466 -------------------------- FindSTLSoft.cmake | 56 ---- LICENSE-MRMC.txt => LICENSE-STORM.txt | 0 3 files changed, 522 deletions(-) delete mode 100644 FindPantheios.cmake delete mode 100644 FindSTLSoft.cmake rename LICENSE-MRMC.txt => LICENSE-STORM.txt (100%) 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 From 7800132684be56ec7e2f43e53f36f45637a5b83c Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 14 Jan 2013 18:24:37 +0100 Subject: [PATCH 03/18] Added Mdp Class, Parser and support in the AutoParser. Added Test for MdpParser --- src/models/Dtmc.h | 27 ++- src/models/Mdp.h | 246 +++++++++++++++++++++++ src/parser/AutoParser.cpp | 14 +- src/parser/DtmcParser.h | 6 +- src/parser/MdpParser.cpp | 53 +++++ src/parser/MdpParser.h | 40 ++++ src/storage/SparseMatrix.h | 12 +- src/vector/dense_vector.h | 183 +++++++++++++++++ test/parser/ParseMdpTest.cpp | 32 +++ test/{mrmc-tests.cpp => storm-tests.cpp} | 0 10 files changed, 593 insertions(+), 20 deletions(-) create mode 100644 src/models/Mdp.h create mode 100644 src/parser/MdpParser.cpp create mode 100644 src/parser/MdpParser.h create mode 100644 src/vector/dense_vector.h create mode 100644 test/parser/ParseMdpTest.cpp rename test/{mrmc-tests.cpp => storm-tests.cpp} (100%) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 303a77739..c766da8cb 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,9 @@ 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."; } } @@ -65,8 +66,9 @@ public: if (dtmc.backwardTransitions != nullptr) { this->backwardTransitions = new storm::models::GraphTransitions(*dtmc.backwardTransitions); } - 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."; } } @@ -206,11 +208,20 @@ 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 + 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) return false; + if (std::abs(sum - 1) > precision) 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/AutoParser.cpp b/src/parser/AutoParser.cpp index f52b2cf8e..f2d161559 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -6,6 +6,7 @@ #include "src/exceptions/WrongFileFormatException.h" #include "src/models/AbstractModel.h" #include "src/parser/DtmcParser.h" +#include "src/parser/MdpParser.h" namespace storm { namespace parser { @@ -26,14 +27,17 @@ 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; - } + DtmcParser* parser = new DtmcParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser->getDtmc(); + break; + } case storm::models::CTMC: break; - case storm::models::MDP: + case storm::models::MDP: { + MdpParser* parser = new MdpParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser->getMdp(); break; + } case storm::models::CTMDP: break; default: ; // Unknown diff --git a/src/parser/DtmcParser.h b/src/parser/DtmcParser.h index 7cf45a335..b1f746bb5 100644 --- a/src/parser/DtmcParser.h +++ b/src/parser/DtmcParser.h @@ -5,8 +5,8 @@ * Author: thomas */ -#ifndef DTMCPARSER_H_ -#define DTMCPARSER_H_ +#ifndef STORM_PARSER_DTMCPARSER_H_ +#define STORM_PARSER_DTMCPARSER_H_ #include "src/parser/Parser.h" #include "src/models/Dtmc.h" @@ -37,4 +37,4 @@ private: } /* namespace parser */ } /* namespace storm */ -#endif /* DTMCPARSER_H_ */ +#endif /* STORM_PARSER_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/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 3a84cf4ad..433501efb 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -795,13 +795,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; } @@ -814,12 +816,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; 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/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 100% rename from test/mrmc-tests.cpp rename to test/storm-tests.cpp From 54499c35ee3558a54892533b358b1e17d40d8433 Mon Sep 17 00:00:00 2001 From: gereon Date: Mon, 14 Jan 2013 23:31:48 +0100 Subject: [PATCH 04/18] adding missing include --- src/modelChecker/DtmcPrctlModelChecker.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index 60a88adce..f443a2ead 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -31,6 +31,7 @@ class DtmcPrctlModelChecker; #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" From 3a1b0f04336b6b6461f80acbe5672e5bc066fb49 Mon Sep 17 00:00:00 2001 From: gereon Date: Mon, 14 Jan 2013 23:33:47 +0100 Subject: [PATCH 05/18] adding sloppy mode for Settings, load settings in tests sloppy mode will not check for requirements of arguments. this is somewhat ugly, as it might not even check for correct type (I'm not sure about that, as we only have strings right now), but it's only the tests-binary anyway... --- src/utility/Settings.cpp | 8 +++++--- src/utility/Settings.h | 8 ++++---- test/storm-tests.cpp | 35 ++++++++++++++++++++++++++++++++++- 3 files changed, 43 insertions(+), 8 deletions(-) diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 3c9b3e4d3..0ba962f20 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -46,12 +46,12 @@ std::map< std::pair, std::shared_ptrinitDescriptions(); - + // Take care of positional arguments. Settings::positional.add("trafile", 1); Settings::positional.add("labfile", 1); @@ -97,7 +97,9 @@ Settings::Settings(int const argc, char const * const argv[], char const * const this->secondRun(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..f0c2a6b23 100644 --- a/src/utility/Settings.h +++ b/src/utility/Settings.h @@ -122,13 +122,13 @@ namespace settings { 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); private: /*! * @brief Constructor. */ - Settings(int const argc, char const * const argv[], char const * const filename); + Settings(int const argc, char const * const argv[], char const * const filename, bool const sloppy); /*! * @brief Initialize options_description object. @@ -200,9 +200,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/test/storm-tests.cpp b/test/storm-tests.cpp index 8f92bcd07..f2556a286 100644 --- a/test/storm-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,38 @@ 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; + delete s; + return false; + } + + if (s->isSet("help")) { + std::cout << storm::settings::help; + delete s; + 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); From 3dc82759af95aca17a62588eaee3e9bed67d0e7d Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 15 Jan 2013 00:34:39 +0100 Subject: [PATCH 06/18] some error output, if Dtmc matrix is invalid --- src/models/Dtmc.h | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index c766da8cb..9a185468e 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -215,13 +215,20 @@ private: 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) return false; - if (std::abs(sum - 1) > precision) 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; } From 0992df5c66ec9bced54b39df3906424e619b896f Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 15 Jan 2013 00:35:40 +0100 Subject: [PATCH 07/18] fixing test for deadlock nodes in parsers --- src/parser/DeterministicSparseTransitionParser.cpp | 12 ++++++------ src/parser/DeterministicSparseTransitionParser.h | 2 +- .../NonDeterministicSparseTransitionParser.cpp | 14 ++++++++------ .../NonDeterministicSparseTransitionParser.h | 2 +- 4 files changed, 16 insertions(+), 14 deletions(-) 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/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); }; From e2f894fe5d8db7318624cb13332c978f896056a0 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Jan 2013 14:59:46 +0100 Subject: [PATCH 08/18] Deleted unnecessary files. --- FindPantheios.cmake | 466 -------------------------------------------- FindSTLSoft.cmake | 56 ------ LICENSE-MRMC.txt | 0 3 files changed, 522 deletions(-) delete mode 100644 FindPantheios.cmake delete mode 100644 FindSTLSoft.cmake delete mode 100644 LICENSE-MRMC.txt 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-MRMC.txt deleted file mode 100644 index e69de29bb..000000000 From b13f1ff37f21823724f7e4c5d52869309fa1fb13 Mon Sep 17 00:00:00 2001 From: gereon Date: Fri, 18 Jan 2013 19:51:48 +0100 Subject: [PATCH 09/18] Adding check "transitionRewards submatrix of transitions" --- src/models/Dtmc.h | 11 +++++++---- src/storage/SparseMatrix.h | 21 +++++++++++++++++++++ 2 files changed, 28 insertions(+), 4 deletions(-) diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 9a185468e..c19208543 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -53,6 +53,12 @@ public: 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."; + } + } } //! Copy Constructor @@ -66,10 +72,7 @@ public: if (dtmc.backwardTransitions != nullptr) { this->backwardTransitions = new storm::models::GraphTransitions(*dtmc.backwardTransitions); } - if (!this->checkValidityOfProbabilityMatrix()) { - LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); - throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; - } + // no checks here, as they have already been performed for dtmc. } //! Destructor diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 433501efb..6a869e185 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -953,6 +953,27 @@ public: } return sum; } + + /*! + * @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: ----------------------------" << std::endl; From 062960b94ccdd87cd701f421ae650518c0272a26 Mon Sep 17 00:00:00 2001 From: gereon Date: Fri, 18 Jan 2013 19:52:49 +0100 Subject: [PATCH 10/18] Some cleanups, removing memleaks --- src/parser/AutoParser.cpp | 13 ++++++++----- src/parser/AutoParser.h | 2 +- src/parser/DtmcParser.cpp | 2 +- src/utility/Settings.cpp | 2 +- 4 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index f2d161559..6aaab5693 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -27,15 +27,15 @@ 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(); + DtmcParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getDtmc(); break; } case storm::models::CTMC: break; case storm::models::MDP: { - MdpParser* parser = new MdpParser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - this->model = parser->getMdp(); + MdpParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + this->model = parser.getMdp(); break; } case storm::models::CTMDP: @@ -43,7 +43,10 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con 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/DtmcParser.cpp index b47b982e8..3aee7b46a 100644 --- a/src/parser/DtmcParser.cpp +++ b/src/parser/DtmcParser.cpp @@ -45,7 +45,7 @@ DtmcParser::DtmcParser(std::string const & transitionSystemFile, std::string con transitionRewards = trp.getMatrix(); } - dtmc = std::shared_ptr>(new storm::models::Dtmc(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); + this->dtmc = std::shared_ptr>(new storm::models::Dtmc(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); } } /* namespace parser */ diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 0ba962f20..675a9ae8e 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -51,7 +51,7 @@ Settings::Settings(int const argc, char const * const argv[], char const * const try { // Initially fill description objects. this->initDescriptions(); - + // Take care of positional arguments. Settings::positional.add("trafile", 1); Settings::positional.add("labfile", 1); From facec2b040d491c3293d8499636e093f916f9d6b Mon Sep 17 00:00:00 2001 From: gereon Date: Sun, 20 Jan 2013 20:19:38 +0100 Subject: [PATCH 11/18] experimented with custom style checker, fixed a few minor issues --- src/models/AbstractModel.cpp | 18 ++++++------- src/parser/AtomicPropositionLabelingParser.h | 2 +- src/parser/SparseStateRewardParser.h | 2 +- src/storage/BitVector.h | 8 ++++-- src/storage/SparseMatrix.h | 27 +++++++++++--------- src/utility/Settings.h | 8 +++--- 6 files changed, 36 insertions(+), 29 deletions(-) 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/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/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 6a869e185..d75927e7b 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 @@ -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(); @@ -318,7 +322,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) { @@ -415,8 +418,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. @@ -917,7 +920,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. @@ -937,7 +940,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. * @@ -953,7 +956,7 @@ public: } return sum; } - + /*! * @brief Checks if it is a submatrix of the given matrix. * @@ -1042,7 +1045,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/utility/Settings.h b/src/utility/Settings.h index f0c2a6b23..01aa46324 100644 --- a/src/utility/Settings.h +++ b/src/utility/Settings.h @@ -57,19 +57,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,7 +118,7 @@ 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(); From c2669ccec49747a95a6fd04766381f16c5d2f684 Mon Sep 17 00:00:00 2001 From: gereon Date: Sun, 20 Jan 2013 20:54:14 +0100 Subject: [PATCH 12/18] "Creating" DeterministicModelParser this new parser is actually the old DtmcParser. It can now also create Ctmc models... --- src/parser/AutoParser.cpp | 9 ++- ...arser.cpp => DeterministicModelParser.cpp} | 26 +++++---- src/parser/DeterministicModelParser.h | 56 +++++++++++++++++++ src/parser/DtmcParser.h | 40 ------------- test/parser/ParseDtmcTest.cpp | 6 +- 5 files changed, 80 insertions(+), 57 deletions(-) rename src/parser/{DtmcParser.cpp => DeterministicModelParser.cpp} (70%) create mode 100644 src/parser/DeterministicModelParser.h delete mode 100644 src/parser/DtmcParser.h diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp index 6aaab5693..110831ff6 100644 --- a/src/parser/AutoParser.cpp +++ b/src/parser/AutoParser.cpp @@ -5,7 +5,7 @@ #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 { @@ -27,12 +27,15 @@ AutoParser::AutoParser(std::string const & transitionSystemFile, std::string con // Do actual parsing switch (type) { case storm::models::DTMC: { - DtmcParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); + DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); this->model = parser.getDtmc(); break; } - case storm::models::CTMC: + 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(); 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 3aee7b46a..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(); } - - this->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..99ce3856f --- /dev/null +++ b/src/parser/DeterministicModelParser.h @@ -0,0 +1,56 @@ +/* + * 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 = ""); + + 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; + } + 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/DtmcParser.h b/src/parser/DtmcParser.h deleted file mode 100644 index b1f746bb5..000000000 --- a/src/parser/DtmcParser.h +++ /dev/null @@ -1,40 +0,0 @@ -/* - * DtmcParser.h - * - * Created on: 19.12.2012 - * Author: thomas - */ - -#ifndef STORM_PARSER_DTMCPARSER_H_ -#define STORM_PARSER_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 /* STORM_PARSER_DTMCPARSER_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")); From e8fd897852cc8475105fbea9fd612faf4d41f8c4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 Jan 2013 13:51:49 +0100 Subject: [PATCH 13/18] Fixed bug in copy constructor of matrix. --- src/storage/SparseMatrix.h | 40 ++++++++++++++++++++++++++++++++------ 1 file changed, 34 insertions(+), 6 deletions(-) diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index d75927e7b..977c6f67a 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -118,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()); } } } @@ -665,8 +665,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; @@ -886,6 +887,31 @@ public: return result; } + void repeatedMultiply(std::vector* vector, uint_fast64_t multiplications) { + std::vector* originalVector = vector; + std::vector* swap = nullptr; + std::vector* temporaryResult = new std::vector(vector->size()); + for (uint_fast64_t iter = 0; iter < multiplications; ++iter) { + for (uint_fast64_t row = 0; row < rowCount; ++row) { + (*temporaryResult)[row] = 0; + for (uint_fast64_t col = columnIndications[row]; col < columnIndications[row + 1]; ++col) { + (*temporaryResult)[row] += valueStorage[col] * (*vector)[row]; + } + } + + swap = temporaryResult; + temporaryResult = vector; + vector = swap; + } + + if (multiplications % 2 == 1) { + *originalVector = *temporaryResult; + delete vector; + } else { + delete temporaryResult; + } + } + /*! * Returns the size of the matrix in memory measured in bytes. * @return The size of the matrix in memory measured in bytes. @@ -979,7 +1005,9 @@ public: } void print() const { - std::cout << "entries: ----------------------------" << std::endl; + std::cout << "entries in (" << rowCount << "x" << colCount << " matrix):" << std::endl; + std::cout << rowIndications << std::endl; + std::cout << columnIndications << 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; From 4fd1d672efa8ec92e2f234f57a31c6015c929a40 Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 22 Jan 2013 19:11:51 +0100 Subject: [PATCH 15/18] fixed valgrind errors creating new shared_ptr instances from a raw pointer (i.e. shared_ptr<>(this) or alike) destroys the internal reference counting. To make this work, one can use std::enable_shared_from_this(), which solves our problem here. --- src/models/AbstractModel.h | 4 ++-- src/parser/DeterministicModelParser.h | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) 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/parser/DeterministicModelParser.h b/src/parser/DeterministicModelParser.h index 99ce3856f..3065b0eb4 100644 --- a/src/parser/DeterministicModelParser.h +++ b/src/parser/DeterministicModelParser.h @@ -28,12 +28,18 @@ class DeterministicModelParser: public storm::parser::Parser { 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)); From f9923bac95a45f213c5c727881f9d95f71a5f812 Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 22 Jan 2013 20:12:30 +0100 Subject: [PATCH 16/18] Fixed memory leaks involving Settings class Settings (being a singleton) will now free it's instance itself upon program termination. --- src/storm.cpp | 7 +----- src/utility/Settings.cpp | 2 ++ src/utility/Settings.h | 47 +++++++++++++++++++++++++++++++++++++--- test/storm-tests.cpp | 2 -- 4 files changed, 47 insertions(+), 11 deletions(-) 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 675a9ae8e..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 diff --git a/src/utility/Settings.h b/src/utility/Settings.h index 01aa46324..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: /*! @@ -123,13 +124,26 @@ namespace settings { friend std::ostream& helpConfigfile(std::ostream& os); friend Settings* instance(); 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() {} + /*! * @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. */ diff --git a/test/storm-tests.cpp b/test/storm-tests.cpp index f2556a286..9165b68a8 100644 --- a/test/storm-tests.cpp +++ b/test/storm-tests.cpp @@ -42,13 +42,11 @@ bool parseOptions(int const argc, char const * const 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; } From 3a73e0838c75732327d78939cc6236f1ac38df9b Mon Sep 17 00:00:00 2001 From: gereon Date: Tue, 22 Jan 2013 21:36:25 +0100 Subject: [PATCH 17/18] make memcheck targets call the binaries with -v and --fix-deadlocks --- CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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) From 756cbd4ed19ecda70aa127af10a082c649226c75 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 24 Jan 2013 10:32:15 +0100 Subject: [PATCH 18/18] Fixed some bugs in GmmxxAdapter and added row-vector product to sparse matrix. --- src/adapters/GmmxxAdapter.h | 9 +++++---- src/storage/SparseMatrix.h | 37 ++++++++++--------------------------- 2 files changed, 15 insertions(+), 31 deletions(-) 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/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 977c6f67a..3d8009733 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -887,29 +887,16 @@ public: return result; } - void repeatedMultiply(std::vector* vector, uint_fast64_t multiplications) { - std::vector* originalVector = vector; - std::vector* swap = nullptr; - std::vector* temporaryResult = new std::vector(vector->size()); - for (uint_fast64_t iter = 0; iter < multiplications; ++iter) { - for (uint_fast64_t row = 0; row < rowCount; ++row) { - (*temporaryResult)[row] = 0; - for (uint_fast64_t col = columnIndications[row]; col < columnIndications[row + 1]; ++col) { - (*temporaryResult)[row] += valueStorage[col] * (*vector)[row]; - } - } - - swap = temporaryResult; - temporaryResult = vector; - vector = swap; - } - - if (multiplications % 2 == 1) { - *originalVector = *temporaryResult; - delete vector; - } else { - delete temporaryResult; + 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; } /*! @@ -1008,11 +995,7 @@ public: std::cout << "entries in (" << rowCount << "x" << colCount << " matrix):" << std::endl; std::cout << rowIndications << std::endl; std::cout << columnIndications << 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; - } - } + std::cout << valueStorage << std::endl; } private: