Lanchid
12 years ago
32 changed files with 881 additions and 674 deletions
-
4CMakeLists.txt
-
466FindPantheios.cmake
-
56FindSTLSoft.cmake
-
0LICENSE-STORM.txt
-
9src/adapters/GmmxxAdapter.h
-
1src/modelChecker/DtmcPrctlModelChecker.h
-
18src/models/AbstractModel.cpp
-
4src/models/AbstractModel.h
-
39src/models/Dtmc.h
-
246src/models/Mdp.h
-
2src/parser/AtomicPropositionLabelingParser.h
-
26src/parser/AutoParser.cpp
-
2src/parser/AutoParser.h
-
26src/parser/DeterministicModelParser.cpp
-
62src/parser/DeterministicModelParser.h
-
12src/parser/DeterministicSparseTransitionParser.cpp
-
2src/parser/DeterministicSparseTransitionParser.h
-
40src/parser/DtmcParser.h
-
53src/parser/MdpParser.cpp
-
40src/parser/MdpParser.h
-
14src/parser/NonDeterministicSparseTransitionParser.cpp
-
2src/parser/NonDeterministicSparseTransitionParser.h
-
2src/parser/SparseStateRewardParser.h
-
8src/storage/BitVector.h
-
89src/storage/SparseMatrix.h
-
7src/storm.cpp
-
8src/utility/Settings.cpp
-
63src/utility/Settings.h
-
183src/vector/dense_vector.h
-
6test/parser/ParseDtmcTest.cpp
-
32test/parser/ParseMdpTest.cpp
-
33test/storm-tests.cpp
@ -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 <admin@philippberger.de> |
|||
# |
|||
# 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) |
|||
|
|||
@ -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 <admin@philippberger.de> |
|||
# |
|||
# 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) |
|||
|
|||
@ -0,0 +1,246 @@ |
|||
/* |
|||
* Mdp.h |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: Philipp Berger |
|||
*/ |
|||
|
|||
#ifndef STORM_MODELS_MDP_H_ |
|||
#define STORM_MODELS_MDP_H_ |
|||
|
|||
#include <ostream> |
|||
#include <iostream> |
|||
#include <memory> |
|||
#include <cstdlib> |
|||
|
|||
#include "AtomicPropositionsLabeling.h" |
|||
#include "GraphTransitions.h" |
|||
#include "src/storage/SparseMatrix.h" |
|||
#include "src/exceptions/InvalidArgumentException.h" |
|||
#include "src/utility/CommandLine.h" |
|||
#include "src/utility/Settings.h" |
|||
#include "src/models/AbstractModel.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace models { |
|||
|
|||
/*! |
|||
* This class represents a Markov Decision Process (MDP) whose states are |
|||
* labeled with atomic propositions. |
|||
*/ |
|||
template <class T> |
|||
class Mdp : public storm::models::AbstractModel { |
|||
|
|||
public: |
|||
//! Constructor |
|||
/*! |
|||
* Constructs a MDP object from the given transition probability matrix and |
|||
* the given labeling of the states. |
|||
* @param probabilityMatrix The transition probability relation of the |
|||
* MDP given by a matrix. |
|||
* @param stateLabeling The labeling that assigns a set of atomic |
|||
* propositions to each state. |
|||
*/ |
|||
Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix, |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling, |
|||
std::shared_ptr<std::vector<T>> stateRewards = nullptr, |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr) |
|||
: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), |
|||
stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix), |
|||
backwardTransitions(nullptr) { |
|||
if (!this->checkValidityOfProbabilityMatrix()) { |
|||
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; |
|||
} |
|||
} |
|||
|
|||
//! Copy Constructor |
|||
/*! |
|||
* Copy Constructor. Performs a deep copy of the given MDP. |
|||
* @param mdp A reference to the MDP that is to be copied. |
|||
*/ |
|||
Mdp(const Mdp<T> &mdp) : probabilityMatrix(mdp.probabilityMatrix), |
|||
stateLabeling(mdp.stateLabeling), stateRewards(mdp.stateRewards), |
|||
transitionRewardMatrix(mdp.transitionRewardMatrix) { |
|||
if (mdp.backwardTransitions != nullptr) { |
|||
this->backwardTransitions = new storm::models::GraphTransitions<T>(*mdp.backwardTransitions); |
|||
} |
|||
if (!this->checkValidityOfProbabilityMatrix()) { |
|||
LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; |
|||
} |
|||
} |
|||
|
|||
//! Destructor |
|||
/*! |
|||
* Destructor. Frees the matrix and labeling associated with this MDP. |
|||
*/ |
|||
~Mdp() { |
|||
if (this->backwardTransitions != nullptr) { |
|||
delete this->backwardTransitions; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* Returns the state space size of the MDP. |
|||
* @return The size of the state space of the MDP. |
|||
*/ |
|||
uint_fast64_t getNumberOfStates() const { |
|||
return this->probabilityMatrix->getColumnCount(); |
|||
} |
|||
|
|||
/*! |
|||
* Returns the number of (non-zero) transitions of the MDP. |
|||
* @return The number of (non-zero) transitions of the MDP. |
|||
*/ |
|||
uint_fast64_t getNumberOfTransitions() const { |
|||
return this->probabilityMatrix->getNonZeroEntryCount(); |
|||
} |
|||
|
|||
/*! |
|||
* Returns a bit vector in which exactly those bits are set to true that |
|||
* correspond to a state labeled with the given atomic proposition. |
|||
* @param ap The atomic proposition for which to get the bit vector. |
|||
* @return A bit vector in which exactly those bits are set to true that |
|||
* correspond to a state labeled with the given atomic proposition. |
|||
*/ |
|||
storm::storage::BitVector* getLabeledStates(std::string ap) const { |
|||
return this->stateLabeling->getAtomicProposition(ap); |
|||
} |
|||
|
|||
/*! |
|||
* Returns a pointer to the matrix representing the transition probability |
|||
* function. |
|||
* @return A pointer to the matrix representing the transition probability |
|||
* function. |
|||
*/ |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const { |
|||
return this->probabilityMatrix; |
|||
} |
|||
|
|||
/*! |
|||
* Returns a pointer to the matrix representing the transition rewards. |
|||
* @return A pointer to the matrix representing the transition rewards. |
|||
*/ |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const { |
|||
return this->transitionRewardMatrix; |
|||
} |
|||
|
|||
/*! |
|||
* Returns a pointer to the vector representing the state rewards. |
|||
* @return A pointer to the vector representing the state rewards. |
|||
*/ |
|||
std::shared_ptr<std::vector<T>> getStateRewards() const { |
|||
return this->stateRewards; |
|||
} |
|||
|
|||
/*! |
|||
* |
|||
*/ |
|||
std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const { |
|||
return stateLabeling->getPropositionsForState(state); |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves a reference to the backwards transition relation. |
|||
* @return A reference to the backwards transition relation. |
|||
*/ |
|||
storm::models::GraphTransitions<T>& getBackwardTransitions() { |
|||
if (this->backwardTransitions == nullptr) { |
|||
this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false); |
|||
} |
|||
return *this->backwardTransitions; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves whether this MDP has a state reward model. |
|||
* @return True if this MDP has a state reward model. |
|||
*/ |
|||
bool hasStateRewards() { |
|||
return this->stateRewards != nullptr; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves whether this MDP has a transition reward model. |
|||
* @return True if this MDP has a transition reward model. |
|||
*/ |
|||
bool hasTransitionRewards() { |
|||
return this->transitionRewardMatrix != nullptr; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves whether the given atomic proposition is a valid atomic proposition in this model. |
|||
* @param atomicProposition The atomic proposition to be checked for validity. |
|||
* @return True if the given atomic proposition is valid in this model. |
|||
*/ |
|||
bool hasAtomicProposition(std::string const& atomicProposition) { |
|||
return this->stateLabeling->containsAtomicProposition(atomicProposition); |
|||
} |
|||
|
|||
/*! |
|||
* Prints information about the model to the specified stream. |
|||
* @param out The stream the information is to be printed to. |
|||
*/ |
|||
void printModelInformationToStream(std::ostream& out) const { |
|||
storm::utility::printSeparationLine(out); |
|||
out << std::endl; |
|||
out << "Model type: \t\tMDP" << std::endl; |
|||
out << "States: \t\t" << this->getNumberOfStates() << std::endl; |
|||
out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; |
|||
this->stateLabeling->printAtomicPropositionsInformationToStream(out); |
|||
out << "Size in memory: \t" |
|||
<< (this->probabilityMatrix->getSizeInMemory() + |
|||
this->stateLabeling->getSizeInMemory() + |
|||
sizeof(*this))/1024 << " kbytes" << std::endl; |
|||
out << std::endl; |
|||
storm::utility::printSeparationLine(out); |
|||
} |
|||
|
|||
storm::models::ModelType getType() { |
|||
return MDP; |
|||
} |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* @brief Perform some sanity checks. |
|||
* |
|||
* Checks probability matrix if all rows sum up to one. |
|||
*/ |
|||
bool checkValidityOfProbabilityMatrix() { |
|||
// Get the settings object to customize linear solving. |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
double precision = s->get<double>("precision"); |
|||
for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) { |
|||
T sum = this->probabilityMatrix->getRowSum(row); |
|||
if (sum == 0) continue; |
|||
if (std::abs(sum - 1) > precision) return false; |
|||
} |
|||
return true; |
|||
} |
|||
|
|||
/*! A matrix representing the transition probability function of the MDP. */ |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix; |
|||
|
|||
/*! The labeling of the states of the MDP. */ |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling; |
|||
|
|||
/*! The state-based rewards of the MDP. */ |
|||
std::shared_ptr<std::vector<T>> stateRewards; |
|||
|
|||
/*! The transition-based rewards of the MDP. */ |
|||
std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix; |
|||
|
|||
/*! |
|||
* A data structure that stores the predecessors for all states. This is |
|||
* needed for backwards directed searches. |
|||
*/ |
|||
storm::models::GraphTransitions<T>* backwardTransitions; |
|||
}; |
|||
|
|||
} // namespace models |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_MODELS_MDP_H_ */ |
|||
@ -0,0 +1,62 @@ |
|||
/* |
|||
* DtmcParser.h |
|||
* |
|||
* Created on: 19.12.2012 |
|||
* Author: thomas |
|||
*/ |
|||
|
|||
#ifndef STORM_PARSER_DETERMINISTICMODELPARSER_H_ |
|||
#define STORM_PARSER_DETERMINISTICMODELPARSER_H_ |
|||
|
|||
#include "src/parser/Parser.h" |
|||
#include "src/models/Dtmc.h" |
|||
#include "src/models/Ctmc.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Load label and transition file and return initialized dtmc or ctmc object. |
|||
* |
|||
* @Note This class creates a new Dtmc or Ctmc object that can |
|||
* be accessed via getDtmc() or getCtmc(). However, it will not delete this object! |
|||
* |
|||
* @Note The labeling representation in the file may use at most as much nodes as are specified in the transition system. |
|||
*/ |
|||
class DeterministicModelParser: public storm::parser::Parser { |
|||
public: |
|||
DeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); |
|||
|
|||
/*! |
|||
* @brief Get the parsed dtmc model. |
|||
*/ |
|||
std::shared_ptr<storm::models::Dtmc<double>> getDtmc() { |
|||
if (this->dtmc == nullptr) { |
|||
this->dtmc = std::shared_ptr<storm::models::Dtmc<double>>(new storm::models::Dtmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); |
|||
} |
|||
return this->dtmc; |
|||
} |
|||
/*! |
|||
* @brief Get the parsed ctmc model. |
|||
*/ |
|||
std::shared_ptr<storm::models::Ctmc<double>> getCtmc() { |
|||
if (this->ctmc == nullptr) { |
|||
this->ctmc = std::shared_ptr<storm::models::Ctmc<double>>(new storm::models::Ctmc<double>(this->transitionSystem, this->labeling, this->stateRewards, this->transitionRewards)); |
|||
} |
|||
return this->ctmc; |
|||
} |
|||
|
|||
private: |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionSystem; |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> labeling; |
|||
std::shared_ptr<std::vector<double>> stateRewards; |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards; |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc; |
|||
std::shared_ptr<storm::models::Ctmc<double>> ctmc; |
|||
}; |
|||
|
|||
} /* namespace parser */ |
|||
} /* namespace storm */ |
|||
#endif /* STORM_PARSER_DETERMINISTICMODELPARSER_H_ */ |
|||
@ -1,40 +0,0 @@ |
|||
/* |
|||
* DtmcParser.h |
|||
* |
|||
* Created on: 19.12.2012 |
|||
* Author: thomas |
|||
*/ |
|||
|
|||
#ifndef DTMCPARSER_H_ |
|||
#define DTMCPARSER_H_ |
|||
|
|||
#include "src/parser/Parser.h" |
|||
#include "src/models/Dtmc.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Load label and transition file and return initialized dtmc object |
|||
* |
|||
* @Note This class creates a new Dtmc object that can |
|||
* be accessed via getDtmc(). However, it will not delete this object! |
|||
* |
|||
* @Note The labeling representation in the file may use at most as much nodes as are specified in the dtmc. |
|||
*/ |
|||
class DtmcParser: public storm::parser::Parser { |
|||
public: |
|||
DtmcParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> getDtmc() { |
|||
return this->dtmc; |
|||
} |
|||
|
|||
private: |
|||
std::shared_ptr<storm::models::Dtmc<double>> dtmc; |
|||
}; |
|||
|
|||
} /* namespace parser */ |
|||
} /* namespace storm */ |
|||
#endif /* DTMCPARSER_H_ */ |
|||
@ -0,0 +1,53 @@ |
|||
/*
|
|||
* MdpParser.cpp |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: Philipp Berger |
|||
*/ |
|||
|
|||
#include "src/parser/MdpParser.h"
|
|||
|
|||
#include <string>
|
|||
#include <vector>
|
|||
|
|||
#include "src/parser/NonDeterministicSparseTransitionParser.h"
|
|||
#include "src/parser/AtomicPropositionLabelingParser.h"
|
|||
#include "src/parser/SparseStateRewardParser.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
/*!
|
|||
* Parses a transition file and a labeling file and produces a MDP out of them; a pointer to the mdp |
|||
* is saved in the field "mdp" |
|||
* Note that the labeling file may have at most as many nodes as the transition file! |
|||
* |
|||
* @param transitionSystemFile String containing the location of the transition file (....tra) |
|||
* @param labelingFile String containing the location of the labeling file (....lab) |
|||
* @param stateRewardFile String containing the location of the state reward file (...srew) |
|||
* @param transitionRewardFile String containing the location of the transition reward file (...trew) |
|||
*/ |
|||
MdpParser::MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile, std::string const & transitionRewardFile) { |
|||
storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile); |
|||
uint_fast64_t stateCount = tp.getMatrix()->getRowCount(); |
|||
|
|||
std::shared_ptr<std::vector<double>> stateRewards = nullptr; |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards = nullptr; |
|||
|
|||
storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile); |
|||
if (stateRewardFile != "") { |
|||
storm::parser::SparseStateRewardParser srp(stateCount, stateRewardFile); |
|||
stateRewards = srp.getStateRewards(); |
|||
} |
|||
if (transitionRewardFile != "") { |
|||
storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile); |
|||
transitionRewards = trp.getMatrix(); |
|||
} |
|||
|
|||
mdp = std::shared_ptr<storm::models::Mdp<double>>(new storm::models::Mdp<double>(tp.getMatrix(), lp.getLabeling(), stateRewards, transitionRewards)); |
|||
} |
|||
|
|||
} /* namespace parser */ |
|||
|
|||
} /* namespace storm */ |
|||
@ -0,0 +1,40 @@ |
|||
/* |
|||
* MdpParser.h |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: thomas |
|||
*/ |
|||
|
|||
#ifndef STORM_PARSER_MDPPARSER_H_ |
|||
#define STORM_PARSER_MDPPARSER_H_ |
|||
|
|||
#include "src/parser/Parser.h" |
|||
#include "src/models/Mdp.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Load label and transition file and return initialized mdp object |
|||
* |
|||
* @Note This class creates a new Mdp object that can |
|||
* be accessed via getMdp(). However, it will not delete this object! |
|||
* |
|||
* @Note The labeling representation in the file may use at most as much nodes as are specified in the mdp. |
|||
*/ |
|||
class MdpParser: public storm::parser::Parser { |
|||
public: |
|||
MdpParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = ""); |
|||
|
|||
std::shared_ptr<storm::models::Mdp<double>> getMdp() { |
|||
return this->mdp; |
|||
} |
|||
|
|||
private: |
|||
std::shared_ptr<storm::models::Mdp<double>> mdp; |
|||
}; |
|||
|
|||
} /* namespace parser */ |
|||
} /* namespace storm */ |
|||
#endif /* STORM_PARSER_MDPPARSER_H_ */ |
|||
@ -0,0 +1,183 @@ |
|||
#ifndef MRMC_VECTOR_BITVECTOR_H_ |
|||
#define MRMC_VECTOR_BITVECTOR_H_ |
|||
|
|||
#include <exception> |
|||
#include <new> |
|||
#include <cmath> |
|||
#include "boost/integer/integer_mask.hpp" |
|||
|
|||
#include <pantheios/pantheios.hpp> |
|||
#include <pantheios/inserters/integer.hpp> |
|||
|
|||
#include "src/exceptions/invalid_state.h" |
|||
#include "src/exceptions/invalid_argument.h" |
|||
#include "src/exceptions/out_of_range.h" |
|||
|
|||
namespace mrmc { |
|||
|
|||
namespace vector { |
|||
|
|||
//! A Vector |
|||
/*! |
|||
A bit vector for boolean fields or quick selection schemas on Matrix entries. |
|||
Does NOT perform index bound checks! |
|||
*/ |
|||
template <class T> |
|||
class DenseVector { |
|||
public: |
|||
//! Constructor |
|||
/*! |
|||
\param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize() |
|||
*/ |
|||
BitVector(uint_fast64_t initial_length) { |
|||
bucket_count = initial_length / 64; |
|||
if (initial_length % 64 != 0) { |
|||
++bucket_count; |
|||
} |
|||
bucket_array = new uint_fast64_t[bucket_count](); |
|||
|
|||
// init all 0 |
|||
for (uint_fast64_t i = 0; i < bucket_count; ++i) { |
|||
bucket_array[i] = 0; |
|||
} |
|||
} |
|||
|
|||
//! Copy Constructor |
|||
/*! |
|||
Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other. |
|||
@param bv A reference to the bit vector that should be copied from |
|||
*/ |
|||
BitVector(const BitVector &bv) : bucket_count(bv.bucket_count) |
|||
{ |
|||
pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor."); |
|||
bucket_array = new uint_fast64_t[bucket_count](); |
|||
memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count); |
|||
} |
|||
|
|||
~BitVector() { |
|||
if (bucket_array != NULL) { |
|||
delete[] bucket_array; |
|||
} |
|||
} |
|||
|
|||
void resize(uint_fast64_t new_length) { |
|||
uint_fast64_t* tempArray = new uint_fast64_t[new_length](); |
|||
|
|||
// 64 bit/entries per uint_fast64_t |
|||
uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count); |
|||
memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize); |
|||
|
|||
bucket_count = new_length / 64; |
|||
if (new_length % 64 != 0) { |
|||
++bucket_count; |
|||
} |
|||
|
|||
delete[] bucket_array; |
|||
bucket_array = tempArray; |
|||
} |
|||
|
|||
void set(const uint_fast64_t index, const bool value) { |
|||
uint_fast64_t bucket = index / 64; |
|||
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. |
|||
// MSVC: C4334, use 1i64 or cast to __int64. |
|||
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) |
|||
uint_fast64_t mask = 1; |
|||
mask = mask << (index % 64); |
|||
if (value) { |
|||
bucket_array[bucket] |= mask; |
|||
} else { |
|||
bucket_array[bucket] &= ~mask; |
|||
} |
|||
} |
|||
|
|||
bool get(const uint_fast64_t index) { |
|||
uint_fast64_t bucket = index / 64; |
|||
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one. |
|||
// MSVC: C4334, use 1i64 or cast to __int64. |
|||
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?) |
|||
uint_fast64_t mask = 1; |
|||
mask = mask << (index % 64); |
|||
return ((bucket_array[bucket] & mask) == mask); |
|||
} |
|||
|
|||
// Operators |
|||
BitVector operator &(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
BitVector operator |(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
BitVector operator ^(BitVector const &bv) { |
|||
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count; |
|||
BitVector result(minSize * 64); |
|||
for (uint_fast64_t i = 0; i < minSize; ++i) { |
|||
result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
BitVector operator ~() { |
|||
BitVector result(this->bucket_count * 64); |
|||
for (uint_fast64_t i = 0; i < this->bucket_count; ++i) { |
|||
result.bucket_array[i] = ~this->bucket_array[i]; |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
/*! |
|||
* Returns the number of bits that are set (to one) in this bit vector. |
|||
* @return The number of bits that are set (to one) in this bit vector. |
|||
*/ |
|||
uint_fast64_t getNumberOfSetBits() { |
|||
uint_fast64_t set_bits = 0; |
|||
for (uint_fast64_t i = 0; i < bucket_count; i++) { |
|||
#ifdef __GNUG__ // check if we are using g++ and use built-in function if available |
|||
set_bits += __builtin_popcount (this->bucket_array[i]); |
|||
#else |
|||
uint_fast32_t cnt; |
|||
uint_fast64_t bitset = this->bucket_array[i]; |
|||
for (cnt = 0; bitset; cnt++) { |
|||
bitset &= bitset - 1; |
|||
} |
|||
set_bits += cnt; |
|||
#endif |
|||
} |
|||
return set_bits; |
|||
} |
|||
|
|||
/*! |
|||
* Returns the size of the bit vector in memory measured in bytes. |
|||
* @return The size of the bit vector in memory measured in bytes. |
|||
*/ |
|||
uint_fast64_t getSizeInMemory() { |
|||
return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count; |
|||
} |
|||
|
|||
private: |
|||
uint_fast64_t bucket_count; |
|||
|
|||
/*! Array containing the boolean bits for each node, 64bits/64nodes per element */ |
|||
uint_fast64_t* bucket_array; |
|||
|
|||
}; |
|||
|
|||
} // namespace vector |
|||
|
|||
} // namespace mrmc |
|||
|
|||
#endif // MRMC_SPARSE_STATIC_SPARSE_MATRIX_H_ |
|||
@ -0,0 +1,32 @@ |
|||
/*
|
|||
* ParseMdpTest.cpp |
|||
* |
|||
* Created on: 14.01.2013 |
|||
* Author: Thomas Heinemann |
|||
*/ |
|||
|
|||
|
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "src/parser/MdpParser.h"
|
|||
#include "src/utility/IoUtility.h"
|
|||
|
|||
TEST(ParseMdpTest, parseAndOutput) { |
|||
storm::parser::MdpParser* mdpParser; |
|||
ASSERT_NO_THROW(mdpParser = new storm::parser::MdpParser( |
|||
STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra", |
|||
STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab")); |
|||
|
|||
std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp(); |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionProbabilityMatrix(); |
|||
|
|||
ASSERT_EQ(mdp->getNumberOfStates(), 3); |
|||
ASSERT_EQ(mdp->getNumberOfTransitions(), 11); |
|||
ASSERT_EQ(matrix->getRowCount(), 2 * 3); |
|||
ASSERT_EQ(matrix->getColumnCount(), 3); |
|||
|
|||
|
|||
delete mdpParser; |
|||
} |
|||
|
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue