From d5eb8ccfabadcfe10a873f9bc617399c5fcc6599 Mon Sep 17 00:00:00 2001 From: gereon Date: Sat, 12 Jan 2013 22:26:41 +0100 Subject: [PATCH 01/29] 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/29] 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 54499c35ee3558a54892533b358b1e17d40d8433 Mon Sep 17 00:00:00 2001 From: gereon Date: Mon, 14 Jan 2013 23:31:48 +0100 Subject: [PATCH 03/29] 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 04/29] 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 05/29] 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 06/29] 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 07/29] 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 08/29] 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 09/29] 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 10/29] 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 11/29] "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 aea711b9f7326dc74722e98d39c0d66cf02634df Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 21 Jan 2013 14:34:01 +0100 Subject: [PATCH 12/29] JacobiDecomposition Copy Constructor should throw exception: Now it throws an InvalidAccessException. This closes #40 --- src/exceptions/InvalidAccessException.h | 19 +++++++++++++++++++ src/storage/JacobiDecomposition.h | 6 +++++- 2 files changed, 24 insertions(+), 1 deletion(-) create mode 100644 src/exceptions/InvalidAccessException.h diff --git a/src/exceptions/InvalidAccessException.h b/src/exceptions/InvalidAccessException.h new file mode 100644 index 000000000..af413b1ed --- /dev/null +++ b/src/exceptions/InvalidAccessException.h @@ -0,0 +1,19 @@ +#ifndef STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_ +#define STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace storm { + +namespace exceptions { + +/*! + * @brief This exception is thrown when a function is used/accessed that is forbidden to use (e.g. Copy Constructors) + */ +STORM_EXCEPTION_DEFINE_NEW(InvalidAccessException) + +} // namespace exceptions + +} // namespace storm + +#endif // STORM_EXCEPTIONS_INVALIDACCESSEXCEPTION_H_ diff --git a/src/storage/JacobiDecomposition.h b/src/storage/JacobiDecomposition.h index f6de68e98..d02d1ab38 100644 --- a/src/storage/JacobiDecomposition.h +++ b/src/storage/JacobiDecomposition.h @@ -6,6 +6,8 @@ #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" +#include "src/exceptions/InvalidAccessException.h" + extern log4cplus::Logger logger; namespace storm { @@ -76,7 +78,9 @@ private: * The copy constructor is disabled for this class. */ //JacobiDecomposition(const JacobiDecomposition& that) = delete; // not possible in VS2012 - JacobiDecomposition(const JacobiDecomposition& that) {} + JacobiDecomposition(const JacobiDecomposition& that) { + throw new storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled."; + } /*! * Pointer to the LU Matrix From a2c5ee805b244904d2bdc679b20e547fd32956ab Mon Sep 17 00:00:00 2001 From: PBerger Date: Mon, 21 Jan 2013 14:40:27 +0100 Subject: [PATCH 13/29] Refactored calls to SetBitCount --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index c90efc3b0..388c0e42f 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -128,7 +128,8 @@ public: std::vector* result = new std::vector(this->getModel().getNumberOfStates()); // Only try to solve system if there are states for which the probability is unknown. - if (maybeStates.getNumberOfSetBits() > 0) { + uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits(); + if (mayBeStatesSetBitCount > 0) { // Now we can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); // Converting the matrix from the fixpoint notation to the form needed for the equation @@ -142,11 +143,11 @@ public: // Initialize the x vector with 0.5 for each element. This is the initial guess for // the iterative solvers. It should be safe as for all 'maybe' states we know that the // probability is strictly larger than 0. - std::vector x(maybeStates.getNumberOfSetBits(), Type(0.5)); + std::vector x(mayBeStatesSetBitCount, Type(0.5)); // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. - std::vector b(maybeStates.getNumberOfSetBits()); + std::vector b(mayBeStatesSetBitCount); this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b); // Solve the corresponding system of linear equations. From e8fd897852cc8475105fbea9fd612faf4d41f8c4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 Jan 2013 13:51:49 +0100 Subject: [PATCH 14/29] 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 16/29] 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 17/29] 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 18/29] 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 d4b5a24757a47517add8f6ff14cc9b3659bc9dda Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 23 Jan 2013 20:08:09 +0100 Subject: [PATCH 19/29] Fixed the Jacobi Decomposition in the Matrix, Diagonal Matrix was not inverted. Implemented solveLinearEquationSystemWithJacobi for GMM based Solver. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 66 +++++++++++++++++-- src/storage/SparseMatrix.h | 6 +- 2 files changed, 67 insertions(+), 5 deletions(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 388c0e42f..c2c5663d0 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -18,6 +18,7 @@ #include "src/utility/Settings.h" #include "src/adapters/GmmxxAdapter.h" #include "src/exceptions/InvalidPropertyException.h" +#include "src/storage/JacobiDecomposition.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -260,7 +261,8 @@ public: // Check whether there are states for which we have to compute the result. storm::storage::BitVector maybeStates = ~(*targetStates) & ~infinityStates; - if (maybeStates.getNumberOfSetBits() > 0) { + const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits(); + if (maybeStatesSetBitCount > 0) { // Now we can eliminate the rows and columns from the original transition probability matrix. storm::storage::SparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); // Converting the matrix from the fixpoint notation to the form needed for the equation @@ -273,10 +275,10 @@ public: // Initialize the x vector with 1 for each element. This is the initial guess for // the iterative solvers. - std::vector x(maybeStates.getNumberOfSetBits(), storm::utility::constGetOne()); + std::vector x(maybeStatesSetBitCount, storm::utility::constGetOne()); // Prepare the right-hand side of the equation system. - std::vector* b = new std::vector(maybeStates.getNumberOfSetBits()); + std::vector* b = new std::vector(maybeStatesSetBitCount); if (this->getModel().hasTransitionRewards()) { // If a transition-based reward model is available, we initialize the right-hand // side to the vector resulting from summing the rows of the pointwise product @@ -290,7 +292,7 @@ public: // as well. As the state reward vector contains entries not just for the states // that we still consider (i.e. maybeStates), we need to extract these values // first. - std::vector* subStateRewards = new std::vector(maybeStates.getNumberOfSetBits()); + std::vector* subStateRewards = new std::vector(maybeStatesSetBitCount); storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewards()); gmm::add(*subStateRewards, *b); delete subStateRewards; @@ -445,6 +447,62 @@ private: LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); } } + + /*! + * Solves the linear equation system Ax=b with the given parameters + * using the Jacobi Method and therefor the Jacobi Decomposition of A. + * + * @param A The matrix A specifying the coefficients of the linear equations. + * @param x The vector x for which to solve the equations. The initial value of the elements of + * this vector are used as the initial guess and might thus influence performance and convergence. + * @param b The vector b specifying the values on the right-hand-sides of the equations. + * @return The solution of the system of linear equations in form of the elements of the vector + * x. + */ + void solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b) const { + + double precision = s->get("precision"); + if (precision <= 0) { + LOG4CPLUS_ERROR(logger, "Precision is not greater Zero"); + } + + // Get a Jacobi Decomposition of the Input Matrix A + storm::storage::JacobiDecomposition* jacobiDecomposition = A.getJacobiDecomposition(); + + // Convert the Diagonal matrix to GMM format + gmm::csr_matrix* gmmxxDiagonalInverted = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(jacobiDecomposition->getJacobiDInv()); + // Convert the LU Matrix to GMM format + gmm::csr_matrix* gmmxxLU = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(jacobiDecomposition->getJacobiLU()); + + delete jacobiDecomposition; + + LOG4CPLUS_INFO(logger, "Starting iterative Jacobi Solver."); + + // x_(k + 1) = D^-1 * (b - R * x_k) + std::vector* xNext = new std::vector(x.size()); + const std::vector* xCopy = xNext; + std::vector* xCurrent = &x; + + uint_fast64_t iterationCount = 0; + do { + // R * x_k -> xCurrent + gmm::mult(*gmmxxLU, *xCurrent, *xNext); + // b - R * x_k + gmm::add(b, gmm::scaled(*xNext, -1.0), *xNext); + // D^-1 * (b - R * x_k) + gmm::mult(*gmmxxDiagonalInverted, *xNext, *xNext); + + std::vector* swap = xNext; + xNext = xCurrent; + xCurrent = swap; + + ++iterationCount; + } while (gmm::vect_norminf(*xCurrent) > precision); + + delete xCopy; + + LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterationCount << " iterations."); + } }; } //namespace modelChecker diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 433501efb..481ddb93e 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -841,9 +841,13 @@ public: SparseMatrix *resultDinv = new SparseMatrix(rowCount); // no entries apart from those on the diagonal resultDinv->initialize(0); + + // constant 1 for diagonal inversion + T constOne = storm::utility::constGetOne(); + // copy diagonal entries to other matrix for (int i = 0; i < rowCount; ++i) { - resultDinv->addNextValue(i, i, resultLU->getValue(i, i)); + resultDinv->addNextValue(i, i, constOne / resultLU->getValue(i, i)); resultLU->getValue(i, i) = storm::utility::constGetZero(); } From 9e416b69e5783f8e624f9a731e35fc7fe2852212 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 23 Jan 2013 22:44:34 +0100 Subject: [PATCH 20/29] The GmmxxAdapter converts to a Row-Major Matrix, not column-major. --- src/adapters/GmmxxAdapter.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index 3fd990a46..1d0fde721 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -23,7 +23,7 @@ class GmmxxAdapter { public: /*! * Converts a sparse matrix into the sparse matrix in the gmm++ format. - * @return A pointer to a column-major sparse matrix in gmm++ format. + * @return A pointer to a row-major sparse matrix in gmm++ format. */ template static gmm::csr_matrix* toGmmxxSparseMatrix(storm::storage::SparseMatrix const& matrix) { From ad3922ec180edb25e62c8fc0778c60a653375213 Mon Sep 17 00:00:00 2001 From: PBerger Date: Wed, 23 Jan 2013 22:49:32 +0100 Subject: [PATCH 21/29] Fixed a bug in the GmmAdapter with non-square matrices being truncated. --- src/adapters/GmmxxAdapter.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h index 1d0fde721..96f3505ec 100644 --- a/src/adapters/GmmxxAdapter.h +++ b/src/adapters/GmmxxAdapter.h @@ -31,7 +31,7 @@ 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)); From 4bb76d026895426fd42f8a712fb89d79b89fdb33 Mon Sep 17 00:00:00 2001 From: PBerger Date: Thu, 24 Jan 2013 01:18:22 +0100 Subject: [PATCH 22/29] Added EigenAdapter and a Test for the Adapter. Fixed a type in EigenDtmcPrctlModelChecker.h Added missing transitions in one example input file --- src/adapters/EigenAdapter.h | 57 +++++++++++ src/modelChecker/EigenDtmcPrctlModelChecker.h | 2 +- src/storage/SparseMatrix.h | 3 +- test/eigen/EigenAdapterTest.cpp | 96 +++++++++++++++++++ 4 files changed, 156 insertions(+), 2 deletions(-) create mode 100644 src/adapters/EigenAdapter.h create mode 100644 test/eigen/EigenAdapterTest.cpp diff --git a/src/adapters/EigenAdapter.h b/src/adapters/EigenAdapter.h new file mode 100644 index 000000000..d7c8169e0 --- /dev/null +++ b/src/adapters/EigenAdapter.h @@ -0,0 +1,57 @@ +/* + * EigenAdapter.h + * + * Created on: 21.01.2013 + * Author: Philipp Berger + */ + +#ifndef STORM_ADAPTERS_EIGENADAPTER_H_ +#define STORM_ADAPTERS_EIGENADAPTER_H_ + +#include "src/storage/SparseMatrix.h" +#include "Eigen/Sparse" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { + +namespace adapters { + +class EigenAdapter { +public: + /*! + * Converts a sparse matrix into the sparse matrix in the eigen format. + * @return A pointer to a row-major sparse matrix in eigen format. + */ + template + static Eigen::SparseMatrix* toEigenSparseMatrix(storm::storage::SparseMatrix const& matrix) { + uint_fast64_t realNonZeros = matrix.getNonZeroEntryCount(); + LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to Eigen format."); + + // Prepare the resulting matrix. + Eigen::SparseMatrix* result = new Eigen::SparseMatrix(matrix.rowCount, matrix.colCount); + + result->resizeNonZeros(realNonZeros); + //result->reserve(realNonZeros); + + // Copy Row Indications + std::copy(matrix.rowIndications.begin(), matrix.rowIndications.end(), (result->outerIndexPtr())); + // Copy Columns Indications + std::copy(matrix.columnIndications.begin(), matrix.columnIndications.end(), (result->innerIndexPtr())); + // And do the same thing with the actual values. + std::copy(matrix.valueStorage.begin(), matrix.valueStorage.end(), (result->valuePtr())); + + LOG4CPLUS_DEBUG(logger, "Done converting matrix to Eigen format."); + + return result; + } +}; + +} //namespace adapters + +} //namespace storm + +#endif /* STORM_ADAPTERS_GMMXXADAPTER_H_ */ diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index e6ea58725..26a18cd8d 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -87,7 +87,7 @@ public: // First, we need to compute the states that satisfy the sub-formula of the next-formula. storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); - // Transform the transition probability matrix to the gmm++ format to use its arithmetic. + // Transform the transition probability matrix to the eigen format to use its arithmetic. Eigen::SparseMatrix* eigenMatrix = this->getModel().getTransitionProbabilityMatrix()->toEigenSparseMatrix(); // Create the vector with which to multiply and initialize it correctly. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 481ddb93e..fb06f905f 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -25,7 +25,7 @@ extern log4cplus::Logger logger; // Forward declaration for adapter classes. -namespace storm { namespace adapters{ class GmmxxAdapter; } } +namespace storm { namespace adapters{ class GmmxxAdapter; class EigenAdapter; } } namespace storm { @@ -43,6 +43,7 @@ public: * Declare adapter classes as friends to use internal data. */ friend class storm::adapters::GmmxxAdapter; + friend class storm::adapters::EigenAdapter; /*! * If we only want to iterate over the columns of the non-zero entries of diff --git a/test/eigen/EigenAdapterTest.cpp b/test/eigen/EigenAdapterTest.cpp new file mode 100644 index 000000000..bddb74dd7 --- /dev/null +++ b/test/eigen/EigenAdapterTest.cpp @@ -0,0 +1,96 @@ +#include "gtest/gtest.h" + +#include "Eigen/Sparse" +#include "src/adapters/EigenAdapter.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "boost/integer/integer_mask.hpp" + +#define STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE 5 +#define STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE 5 + +TEST(EigenAdapterTest, SimpleDenseSquareCopy) { + // 5 rows + storm::storage::SparseMatrix sm(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + + double values[STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE]; + sm.initialize(STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + + int row = 0; + int col = 0; + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { + values[i] = static_cast(i + 1); + + sm.addNextValue(row, col, values[i]); + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } + sm.finalize(); + + auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm); + + ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + ASSERT_EQ(esm->nonZeros(), STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE); + + row = 0; + col = 0; + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE; ++i) { + ASSERT_EQ(values[i], esm->coeff(row, col)); + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLEDENSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } +} + +TEST(EigenAdapterTest, SimpleSparseSquareCopy) { + // 5 rows + storm::storage::SparseMatrix sm(STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); + + double values[STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE]; + sm.initialize((STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); + + int row = 0; + int col = 0; + + bool everySecondElement = true; + + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { + values[i] = static_cast(i + 1); + if (everySecondElement) { + sm.addNextValue(row, col, values[i]); + } + everySecondElement = !everySecondElement; + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } + sm.finalize(); + + auto esm = storm::adapters::EigenAdapter::toEigenSparseMatrix(sm); + + ASSERT_EQ(esm->rows(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); + ASSERT_EQ(esm->cols(), STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE); + ASSERT_EQ(esm->nonZeros(), (STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE + 1) / 2); + + row = 0; + col = 0; + everySecondElement = true; + for (int i = 0; i < STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE * STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE; ++i) { + if (everySecondElement) { + ASSERT_EQ(values[i], esm->coeff(row, col)); + } + everySecondElement = !everySecondElement; + ++col; + if (col == STORM_EIGENADAPTERTEST_SIMPLESPARSESQUARECOPY_SIZE) { + ++row; + col = 0; + } + } +} From 756cbd4ed19ecda70aa127af10a082c649226c75 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 24 Jan 2013 10:32:15 +0100 Subject: [PATCH 23/29] 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: From 7331544377ed0cd39d48cda479cab5b4b863e324 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 26 Jan 2013 11:23:20 +0100 Subject: [PATCH 24/29] Added output functionality to bit vector and moved test-checking lines in storm.cpp to the right place. --- src/storage/BitVector.h | 22 ++++++++++++++++++---- src/storm.cpp | 8 ++++---- 2 files changed, 22 insertions(+), 8 deletions(-) diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 66baf546e..df3f86600 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -387,11 +387,11 @@ public: * 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 getNumberOfSetBits() const { return getNumberOfSetBitsBeforeIndex(bucketCount << 6); } - uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) { + uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const { uint_fast64_t result = 0; // First, count all full buckets. uint_fast64_t bucket = index >> 6; @@ -437,7 +437,7 @@ public: /*! * Retrieves the number of bits this bit vector can store. */ - uint_fast64_t getSize() { + uint_fast64_t getSize() const { return bitCount; } @@ -445,7 +445,7 @@ public: * 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() { + uint_fast64_t getSizeInMemory() const { return sizeof(*this) + sizeof(uint_fast64_t) * bucketCount; } @@ -463,6 +463,20 @@ public: return endIterator; } + /*! + * Returns a string representation of the bit vector. + */ + std::string toString() const { + std::stringstream result; + result << "bit vector(" << this->getNumberOfSetBits() << ") ["; + for (auto index : *this) { + result << index << " "; + } + result << "]"; + + return result.str(); + } + private: /*! diff --git a/src/storm.cpp b/src/storm.cpp index 250163f70..9d2fff6d7 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -216,12 +216,12 @@ void testChecking() { if (parser.getType() == storm::models::DTMC) { std::shared_ptr> dtmc = parser.getModel>(); dtmc->printModelInformationToStream(std::cout); + + // testCheckingDie(*dtmc); + // testCheckingCrowds(*dtmc); + // testCheckingSynchronousLeader(*dtmc, 4); } else std::cout << "Input is not DTMC" << std::endl; - - // testCheckingDie(*dtmc); - // testCheckingCrowds(*dtmc); - // testCheckingSynchronousLeader(*dtmc, 4); } /*! From c47b559986608a97129cc5eeeee8a3b522439b04 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 29 Jan 2013 09:13:06 +0100 Subject: [PATCH 25/29] Fixed minor bugs for Jacobi decomposition. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 4 +++- src/storage/JacobiDecomposition.h | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index c2c5663d0..0c54d63cf 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -460,10 +460,12 @@ private: * x. */ void solveLinearEquationSystemWithJacobi(storm::storage::SparseMatrix const& A, std::vector& x, std::vector const& b) const { + // Get the settings object to customize linear solving. + storm::settings::Settings* s = storm::settings::instance(); double precision = s->get("precision"); if (precision <= 0) { - LOG4CPLUS_ERROR(logger, "Precision is not greater Zero"); + LOG4CPLUS_ERROR(logger, "Selected precision for linear equation solving must be strictly greater than zero for Jacobi method."); } // Get a Jacobi Decomposition of the Input Matrix A diff --git a/src/storage/JacobiDecomposition.h b/src/storage/JacobiDecomposition.h index d02d1ab38..9aec6f061 100644 --- a/src/storage/JacobiDecomposition.h +++ b/src/storage/JacobiDecomposition.h @@ -79,7 +79,7 @@ private: */ //JacobiDecomposition(const JacobiDecomposition& that) = delete; // not possible in VS2012 JacobiDecomposition(const JacobiDecomposition& that) { - throw new storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled."; + throw storm::exceptions::InvalidAccessException() << "The copy constructor of JacobiDecomposition is explicitly disabled."; } /*! From 1edd3060322155b0a1b696c4acf40e8f271981f7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 29 Jan 2013 21:16:16 +0100 Subject: [PATCH 26/29] Silenced warning of clang: Changed NULL to nullptr as this should be used in C++11. --- src/parser/DeterministicSparseTransitionParser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 59eb336d7..632ac78ed 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -164,7 +164,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st */ LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); this->matrix = std::shared_ptr>(new storm::storage::SparseMatrix(maxnode + 1)); - if (this->matrix == NULL) { + if (this->matrix == nullptr) { LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); throw std::bad_alloc(); } From 9a9cd968d9caac0b6dd3bcdb9012fd8f68bb4d72 Mon Sep 17 00:00:00 2001 From: PBerger Date: Thu, 31 Jan 2013 00:00:47 +0100 Subject: [PATCH 27/29] Added a test to verify the RowSum Function in the Sparse Matrix. Added an option to the settings for auto-fixing missing no-selfloop states. Kind of a super-option above fix-nodeadlocks, perhaps some Cleanup later on. Modified tra Files to comply with formats... --- .../DeterministicSparseTransitionParser.cpp | 83 +++++++++++++++---- src/storage/SparseMatrix.h | 9 +- src/utility/Settings.cpp | 1 + test/storage/SparseMatrixTest.cpp | 9 ++ 4 files changed, 84 insertions(+), 18 deletions(-) diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index 632ac78ed..c5668846d 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -66,9 +66,10 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0; /* - * Check all transitions for non-zero diagonal entrys. + * Check all transitions for existing diagonal entrys. */ - int_fast64_t row, lastrow = -1, col; + int_fast64_t row, col; + int_fast64_t lastDiagonal = -1; double val; maxnode = 0; while (buf[0] != '\0') { @@ -80,17 +81,29 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast /* * Check if one is larger than the current maximum id. */ - if (row > maxnode) maxnode = row; - if (col > maxnode) maxnode = col; + if (row > maxnode) { + maxnode = row; + } + if (col > maxnode) { + maxnode = col; + } /* - * Check if a node was skipped, i.e. if a node has no outgoing - * transitions. If so, increase non_zero, as the second pass will + * Check if a self-loop was skipped. If so, increase non_zero, as the second pass will * either throw an exception (in this case, it doesn't matter * anyway) or add a self-loop (in this case, we'll need the * additional transition). */ - if (lastrow < row - 1) non_zero += row - lastrow - 1; - lastrow = row; + if (lastDiagonal < (row - 1)) { + non_zero += row - 1 - lastDiagonal; + lastDiagonal = row - 1; + } + /* + * Check if this is a self-loop and remember that + */ + if (row == col) { + lastDiagonal = row; + } + /* * Read probability of this transition. * Check, if the value is a probability, i.e. if it is between 0 and 1. @@ -103,6 +116,10 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast buf = trimWhitespaces(buf); } + if (lastDiagonal < (row - 1)) { + non_zero += row - 1 - lastDiagonal; + } + return non_zero; } @@ -171,12 +188,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st this->matrix->initialize(non_zero); int_fast64_t row, lastrow = -1, col; + int_fast64_t lastDiagonal = -1; double val; bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); + bool fixSelfloops = storm::settings::instance()->isSet("fix-selfloops"); bool hadDeadlocks = false; + bool hadNoSelfLoops = false; /* - * Read all transitions from file. Note that we assume, that the + * Read all transitions from file. Note that we assume that the * transitions are listed in canonical order, otherwise this will not * work, i.e. the values in the matrix will be at wrong places. */ @@ -189,24 +209,53 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st val = checked_strtod(buf, &buf); /* - * Check if we skipped a node, i.e. if a node does not have any - * outgoing transitions. + * Check if a self-loop was skipped. */ - for (int_fast64_t node = lastrow + 1; node < row; node++) { - hadDeadlocks = true; - if (fixDeadlocks) { - this->matrix->addNextValue(node, node, 1); - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); + if (lastDiagonal < (row - 1)) { + /* + * Check if we skipped a node entirely, i.e. a node does not have any + * outgoing transitions. + */ + if ((lastrow + 1) < row) { + for (int_fast64_t node = lastrow + 1; node < row; node++) { + hadDeadlocks = true; + if (fixDeadlocks || fixSelfloops) { + this->matrix->addNextValue(node, node, storm::utility::constGetOne()); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); + } + } } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); + // there were other transitions but no self-loop + for (int_fast64_t node = lastDiagonal + 1; node < row; node++) { + hadNoSelfLoops = true; + if (fixSelfloops) { + this->matrix->addNextValue(node, node, storm::utility::constGetZero()); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no self transition. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no self transition."); + } + } } + lastDiagonal = row - 1; + } + + + /* + * Check if this is a self-loop and remember that + */ + if (row == col) { + lastDiagonal = row; } + lastrow = row; this->matrix->addNextValue(row, col, val); buf = trimWhitespaces(buf); } if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; + if (!fixSelfloops && hadNoSelfLoops) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had no self loops. You can use --fix-selfloops to insert self-loops on the fly."; /* * Finalize Matrix. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index b7fa94d62..90807f1bc 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -799,22 +799,29 @@ public: /*! * Inverts all elements on the diagonal, i.e. sets the diagonal values to 1 minus their previous * value. + * Requires the matrix to contain each diagonal element AND to be square! */ void invertDiagonal() { if (this->getRowCount() != this->getColumnCount()) { throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to be square!"; } - T one(1); + T one = storm::utility::constGetOne(); + bool foundRow; for (uint_fast64_t row = 0; row < rowCount; ++row) { uint_fast64_t rowStart = rowIndications[row]; uint_fast64_t rowEnd = rowIndications[row + 1]; + foundRow = false; while (rowStart < rowEnd) { if (columnIndications[rowStart] == row) { valueStorage[rowStart] = one - valueStorage[rowStart]; + foundRow = true; break; } ++rowStart; } + if (!foundRow) { + throw storm::exceptions::InvalidArgumentException() << "SparseMatrix::invertDiagonal requires the Matrix to contain all diagonal entries!"; + } } } diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 26f733071..f983f22fc 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -139,6 +139,7 @@ void Settings::initDescriptions() { ("transrew", bpo::value()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") + ("fix-selfloops", "insert self-loops for states without such transitions") ; } diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp index 2a29fb736..b3eb68971 100644 --- a/test/storage/SparseMatrixTest.cpp +++ b/test/storage/SparseMatrixTest.cpp @@ -94,6 +94,10 @@ TEST(SparseMatrixTest, Test) { 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23 /* second to last row */ }; + int row_sums[25] = {}; + for (int i = 0; i < 50; ++i) { + row_sums[position_row[i]] += values[i]; + } ASSERT_NO_THROW(ssm->initialize(50)); ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::Initialized); @@ -123,6 +127,11 @@ TEST(SparseMatrixTest, Test) { } ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix::MatrixStatus::ReadReady); + // Test Row Sums + for (int row = 0; row < 25; ++row) { + ASSERT_EQ(row_sums[row], ssm->getRowSum(row)); + } + delete ssm; } From 726569d5f11c44eace4331ee18ef17606e3d0ef9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 31 Jan 2013 10:40:28 +0100 Subject: [PATCH 28/29] Fixed bug in parser that inserted 0-entries on the diagonal at the wrong places. Enabled link-time-optimizations for Release-Build when using clang. Fixed bug in base exception: what() returned a pointer to a char array belonging to a local variable, which got deallocated and thus invalidates the char array content. --- CMakeLists.txt | 2 +- src/exceptions/BaseException.h | 6 +- .../DeterministicSparseTransitionParser.cpp | 65 ++++++++----------- .../DeterministicSparseTransitionParser.h | 2 +- src/utility/Settings.cpp | 1 - 5 files changed, 35 insertions(+), 41 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8caf0b081..d17922f26 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -75,7 +75,7 @@ elseif(MSVC) add_definitions(/D_SCL_SECURE_NO_DEPRECATE) else(CLANG) # Set standard flags for clang - set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") + set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG -funroll-loops -O4") set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable") # Turn on popcnt instruction if desired (yes by default) diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h index c1b6ee054..6c670f88b 100644 --- a/src/exceptions/BaseException.h +++ b/src/exceptions/BaseException.h @@ -28,7 +28,11 @@ class BaseException : public std::exception { } virtual const char* what() const throw() { - return this->stream.str().c_str(); + std::string errorString = this->stream.str(); + char* result = new char[errorString.size() + 1]; + result[errorString.size()] = '\0'; + std::copy(errorString.begin(), errorString.end(), result); + return result; } private: diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index c5668846d..e9e430988 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -133,7 +133,7 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast * @return a pointer to the created sparse matrix. */ -DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename) +DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing) : matrix(nullptr) { /* * Enforce locale where decimal point is '.'. @@ -188,12 +188,10 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st this->matrix->initialize(non_zero); int_fast64_t row, lastrow = -1, col; - int_fast64_t lastDiagonal = -1; double val; bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); - bool fixSelfloops = storm::settings::instance()->isSet("fix-selfloops"); bool hadDeadlocks = false; - bool hadNoSelfLoops = false; + bool rowHadDiagonalEntry = false; /* * Read all transitions from file. Note that we assume that the @@ -208,45 +206,39 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st col = checked_strtol(buf, &buf); val = checked_strtod(buf, &buf); + if (row != lastrow) { + rowHadDiagonalEntry = false; + } + /* - * Check if a self-loop was skipped. + * Check if we skipped a state entirely, i.e. a state does not have any + * outgoing transitions. */ - if (lastDiagonal < (row - 1)) { - /* - * Check if we skipped a node entirely, i.e. a node does not have any - * outgoing transitions. - */ - if ((lastrow + 1) < row) { - for (int_fast64_t node = lastrow + 1; node < row; node++) { - hadDeadlocks = true; - if (fixDeadlocks || fixSelfloops) { - this->matrix->addNextValue(node, node, storm::utility::constGetOne()); - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); - } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions."); - } - } - } else { - // there were other transitions but no self-loop - for (int_fast64_t node = lastDiagonal + 1; node < row; node++) { - hadNoSelfLoops = true; - if (fixSelfloops) { - this->matrix->addNextValue(node, node, storm::utility::constGetZero()); - LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no self transition. A self-loop was inserted."); - } else { - LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no self transition."); - } + if ((lastrow + 1) < row) { + for (int_fast64_t state = lastrow + 1; state < row; ++state) { + hadDeadlocks = true; + if (fixDeadlocks) { + this->matrix->addNextValue(state, state, storm::utility::constGetOne()); + LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << state << " has no outgoing transitions. A self-loop was inserted."); + } else { + LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << state << " has no outgoing transitions."); } } - lastDiagonal = row - 1; - } - - + } + + // Insert the missing diagonal value if requested. + if (col > row && !rowHadDiagonalEntry) { + if (insertDiagonalEntriesIfMissing) { + this->matrix->addNextValue(row, row, storm::utility::constGetZero()); + } + rowHadDiagonalEntry = true; + } + /* - * Check if this is a self-loop and remember that + * Check if the transition is a self-loop */ if (row == col) { - lastDiagonal = row; + rowHadDiagonalEntry = true; } lastrow = row; @@ -255,7 +247,6 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st buf = trimWhitespaces(buf); } if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; - if (!fixSelfloops && hadNoSelfLoops) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had no self loops. You can use --fix-selfloops to insert self-loops on the fly."; /* * Finalize Matrix. diff --git a/src/parser/DeterministicSparseTransitionParser.h b/src/parser/DeterministicSparseTransitionParser.h index 099d0fa4a..2407f3398 100644 --- a/src/parser/DeterministicSparseTransitionParser.h +++ b/src/parser/DeterministicSparseTransitionParser.h @@ -17,7 +17,7 @@ namespace parser { */ class DeterministicSparseTransitionParser : public Parser { public: - DeterministicSparseTransitionParser(std::string const &filename); + DeterministicSparseTransitionParser(std::string const &filename, bool insertDiagonalEntriesIfMissing = true); std::shared_ptr> getMatrix() { return this->matrix; diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index f983f22fc..26f733071 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -139,7 +139,6 @@ void Settings::initDescriptions() { ("transrew", bpo::value()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") - ("fix-selfloops", "insert self-loops for states without such transitions") ; } From 6fb56748a630d746be69218c6a7f8bc9fc4cc62e Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 31 Jan 2013 15:10:36 +0100 Subject: [PATCH 29/29] Bugfix for correctly counting the number of values the parser inserts. --- .../DeterministicSparseTransitionParser.cpp | 159 ++++++++++-------- 1 file changed, 91 insertions(+), 68 deletions(-) diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp index e9e430988..24a5dc489 100644 --- a/src/parser/DeterministicSparseTransitionParser.cpp +++ b/src/parser/DeterministicSparseTransitionParser.cpp @@ -45,7 +45,7 @@ namespace parser { * @param maxnode Is set to highest id of all nodes. */ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast64_t& maxnode) { - uint_fast64_t non_zero = 0; + uint_fast64_t nonZeroEntryCount = 0; /* * Check file header and extract number of transitions. @@ -63,64 +63,75 @@ uint_fast64_t DeterministicSparseTransitionParser::firstPass(char* buf, int_fast return 0; } buf += 12; // skip "TRANSITIONS " - if ((non_zero = strtol(buf, &buf, 10)) == 0) return 0; + if ((nonZeroEntryCount = strtol(buf, &buf, 10)) == 0) return 0; - /* - * Check all transitions for existing diagonal entrys. - */ - int_fast64_t row, col; - int_fast64_t lastDiagonal = -1; - double val; - maxnode = 0; - while (buf[0] != '\0') { - /* - * Read row and column. - */ - row = checked_strtol(buf, &buf); - col = checked_strtol(buf, &buf); - /* - * Check if one is larger than the current maximum id. - */ - if (row > maxnode) { - maxnode = row; - } - if (col > maxnode) { - maxnode = col; - } - /* - * Check if a self-loop was skipped. If so, increase non_zero, as the second pass will - * either throw an exception (in this case, it doesn't matter - * anyway) or add a self-loop (in this case, we'll need the - * additional transition). - */ - if (lastDiagonal < (row - 1)) { - non_zero += row - 1 - lastDiagonal; - lastDiagonal = row - 1; - } - /* - * Check if this is a self-loop and remember that - */ - if (row == col) { - lastDiagonal = row; - } + /* + * Check all transitions for non-zero diagonal entries and deadlock states. + */ + int_fast64_t row, lastRow = -1, col; + bool rowHadDiagonalEntry = false; + double val; + maxnode = 0; + while (buf[0] != '\0') { + /* + * Read row and column. + */ + row = checked_strtol(buf, &buf); + col = checked_strtol(buf, &buf); - /* - * Read probability of this transition. - * Check, if the value is a probability, i.e. if it is between 0 and 1. - */ - val = checked_strtod(buf, &buf); - if ((val < 0.0) || (val > 1.0)) { - LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); - return 0; - } - buf = trimWhitespaces(buf); - } + /* + * If we have switched to the next row, we need to clear the information about + * the diagonal entry. + */ + if (row != lastRow) { + /* + * If the last row did have transitions, but no diagonal element, we need to insert + * it as well. + */ + if (!rowHadDiagonalEntry && lastRow != -1) { + ++nonZeroEntryCount; + } + rowHadDiagonalEntry = false; + } - if (lastDiagonal < (row - 1)) { - non_zero += row - 1 - lastDiagonal; - } + if (row == col) { + rowHadDiagonalEntry = true; + } - return non_zero; + /* + * Check if one is larger than the current maximum id. + */ + if (row > maxnode) maxnode = row; + if (col > maxnode) maxnode = col; + + /* + * Check if a node was skipped, i.e. if a node has no outgoing + * transitions. If so, increase non_zero, as the second pass will + * either throw an exception (in this case, it doesn't matter + * anyway) or add a self-loop (in this case, we'll need the + * additional transition). + */ + if (lastRow < row - 1) { + nonZeroEntryCount += row - lastRow - 1; + } + lastRow = row; + /* + * Read probability of this transition. + * Check, if the value is a probability, i.e. if it is between 0 and 1. + */ + val = checked_strtod(buf, &buf); + if ((val < 0.0) || (val > 1.0)) { + LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << val << "\"."); + return 0; + } + buf = trimWhitespaces(buf); + } + + if (!rowHadDiagonalEntry) { + ++nonZeroEntryCount; + } + + return nonZeroEntryCount; } @@ -149,12 +160,12 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st /* * Perform first pass, i.e. count entries that are not zero. */ - int_fast64_t maxnode; - uint_fast64_t non_zero = this->firstPass(file.data, maxnode); + int_fast64_t maxStateId; + uint_fast64_t nonZeroEntryCount = this->firstPass(file.data, maxStateId); /* * If first pass returned zero, the file format was wrong. */ - if (non_zero == 0) { + if (nonZeroEntryCount == 0) { LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); throw storm::exceptions::WrongFileFormatException(); } @@ -179,15 +190,15 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st * Creating matrix here. * The number of non-zero elements is computed by firstPass(). */ - LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); - this->matrix = std::shared_ptr>(new storm::storage::SparseMatrix(maxnode + 1)); + LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); + this->matrix = std::shared_ptr>(new storm::storage::SparseMatrix(maxStateId + 1)); if (this->matrix == nullptr) { - LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << "."); + LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxStateId+1) << " x " << (maxStateId+1) << "."); throw std::bad_alloc(); } - this->matrix->initialize(non_zero); + this->matrix->initialize(nonZeroEntryCount); - int_fast64_t row, lastrow = -1, col; + int_fast64_t row, lastRow = -1, col; double val; bool fixDeadlocks = storm::settings::instance()->isSet("fix-deadlocks"); bool hadDeadlocks = false; @@ -206,7 +217,14 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st col = checked_strtol(buf, &buf); val = checked_strtod(buf, &buf); - if (row != lastrow) { + if (row != lastRow) { + /* + * If the previous row did not have a diagonal entry, we need to insert it. + */ + if (!rowHadDiagonalEntry && lastRow != -1) { + this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero()); + } + rowHadDiagonalEntry = false; } @@ -214,8 +232,8 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st * Check if we skipped a state entirely, i.e. a state does not have any * outgoing transitions. */ - if ((lastrow + 1) < row) { - for (int_fast64_t state = lastrow + 1; state < row; ++state) { + if ((lastRow + 1) < row) { + for (int_fast64_t state = lastRow + 1; state < row; ++state) { hadDeadlocks = true; if (fixDeadlocks) { this->matrix->addNextValue(state, state, storm::utility::constGetOne()); @@ -226,7 +244,7 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st } } - // Insert the missing diagonal value if requested. + // Insert the missing diagonal value here, because the input skipped it. if (col > row && !rowHadDiagonalEntry) { if (insertDiagonalEntriesIfMissing) { this->matrix->addNextValue(row, row, storm::utility::constGetZero()); @@ -241,11 +259,16 @@ DeterministicSparseTransitionParser::DeterministicSparseTransitionParser(std::st rowHadDiagonalEntry = true; } - lastrow = row; + lastRow = row; this->matrix->addNextValue(row, col, val); buf = trimWhitespaces(buf); } + + if (!rowHadDiagonalEntry) { + this->matrix->addNextValue(lastRow, lastRow, storm::utility::constGetZero()); + } + if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly."; /*