diff --git a/.gitignore b/.gitignore index 28b6c3dcc..494b270c7 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,7 @@ resources/3rdparty/log4cplus-1.1.0/ resources/3rdparty/gtest-1.6.0/ resources/3rdparty/eigen/ resources/3rdparty/gmm-4.2/ +resources/3rdparty/cudd-2.5.0/ #Visual Studio files *.[Oo]bj *.user diff --git a/CMakeLists.txt b/CMakeLists.txt index f383d1851..1a5a9a0bd 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -44,12 +44,22 @@ message(STATUS "EIGEN3_INCLUDE_DIR is ${EIGEN3_INCLUDE_DIR}") set(GMMXX_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-4.2/include) message(STATUS "GMMXX_INCLUDE_DIR is ${GMMXX_INCLUDE_DIR}") +# Set all CUDD references to the version in the repository +set(CUDD_INCLUDE_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/include ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd) +set(CUDD_LIBRARY_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/util ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/st ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj) +message(STATUS "CUDD_INCLUDE_DIRS is ${CUDD_INCLUDE_DIRS}") +message(STATUS "CUDD_LIBRARY_DIRS is ${CUDD_LIBRARY_DIRS}") + # Now define all available custom options option(DEBUG "Sets whether the DEBUG mode is used" ON) option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON) option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON) option(USE_INTELTBB "Sets whether the Intel TBB Extensions should be used." OFF) option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF) +option(LINK_LIBCXXABI "Sets whether libc++abi should be linked" OFF) +set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") +set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") +set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.") # If the DEBUG option was turned on, we will target a debug version and a release version otherwise if (DEBUG) @@ -82,9 +92,11 @@ elseif(MSVC) add_definitions(/D_SCL_SECURE_NO_DEPRECATE) else(CLANG) message(STATUS "Using CLANG") + # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. + set (CLANG ON) # Set standard flags for clang - set(CMAKE_CXX_FLAGS_RELEASE "-DNDEBUG -funroll-loops -O4") - set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable") + set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O4") + set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE") set (CMAKE_CXX_FLAGS_DEBUG "-g") @@ -154,6 +166,11 @@ find_package(Doxygen REQUIRED) set(Boost_USE_STATIC_LIBS ON) set(Boost_USE_MULTITHREADED ON) set(Boost_USE_STATIC_RUNTIME OFF) + +# If a custom boost root directory was specified, we set the corresponding hint for the script to find it. +if(CUSTOM_BOOST_ROOT) + set(BOOST_ROOT "${CUSTOM_BOOST_ROOT}") +endif(CUSTOM_BOOST_ROOT) find_package(Boost REQUIRED COMPONENTS program_options) find_package(TBB) @@ -187,6 +204,23 @@ include_directories(${EIGEN3_INCLUDE_DIR}) # Add GMMXX to the included directories include_directories(${GMMXX_INCLUDE_DIR}) +# Add custom additional include or link directories +if (ADDITIONAL_INCLUDE_DIRS) + message(STATUS "Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}") + include_directories(${ADDITIONAL_INCLUDE_DIRS}) +endif(ADDITIONAL_INCLUDE_DIRS) +if (ADDITIONAL_LINK_DIRS) + message(STATUS "Using additional link directories ${ADDITIONAL_LINK_DIRS}") + link_directories(${ADDITIONAL_LINK_DIRS}) +endif(ADDITIONAL_LINK_DIRS) + +if (CUDD_INCLUDE_DIRS) + include_directories(${CUDD_INCLUDE_DIRS}) +endif(CUDD_INCLUDE_DIRS) +if (CUDD_LIBRARY_DIRS) + link_directories(${CUDD_LIBRARY_DIRS}) +endif(CUDD_LIBRARY_DIRS) + # Add the executables # Must be created *after* Boost was added because of LINK_DIRECTORIES add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS}) @@ -222,6 +256,13 @@ if (STORM_USE_COTIRE) #cotire(storm-tests) endif() +# Link against libc++abi if requested. May be needed to build on Linux systems using clang. +if (LINK_LIBCXXABI) + message (STATUS "Linking against libc++abi.") + target_link_libraries(storm "c++abi") + target_link_libraries(storm-tests "c++abi") +endif(LINK_LIBCXXABI) + # Add a target to generate API documentation with Doxygen if(DOXYGEN_FOUND) set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") @@ -263,6 +304,11 @@ if (LOG4CPLUS_INCLUDE_DIR) endif(UNIX AND NOT APPLE) endif(LOG4CPLUS_INCLUDE_DIR) +if (CUDD_LIBRARY_DIRS) + target_link_libraries(storm "-lobj -lcudd -lmtr -lst -lutil -lepd") + target_link_libraries(storm-tests "-lobj -lcudd -lmtr -lst -lutil -lepd") +endif(CUDD_LIBRARY_DIRS) + if (THREADS_FOUND) include_directories(${THREADS_INCLUDE_DIRS}) target_link_libraries(storm ${CMAKE_THREAD_LIBS_INIT}) diff --git a/examples/dtmc/crowds/crowds15_5.pm b/examples/dtmc/crowds/crowds15_5.pm index aa4921cbf..511d962f0 100644 --- a/examples/dtmc/crowds/crowds15_5.pm +++ b/examples/dtmc/crowds/crowds15_5.pm @@ -57,7 +57,7 @@ module crowds lastSeen: [0..CrowdSize - 1] init 0; // get the protocol started - [] phase=0 & runCount (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + [] phase=0 & runCount 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); // decide whether crowd member is good or bad according to given probabilities [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); @@ -66,27 +66,27 @@ module crowds [] phase=2 & good -> 1/15 : (lastSeen'=0) & (phase'=3) + 1/15 : (lastSeen'=1) & (phase'=3) + 1/15 : (lastSeen'=2) & (phase'=3) + 1/15 : (lastSeen'=3) & (phase'=3) + 1/15 : (lastSeen'=4) & (phase'=3) + 1/15 : (lastSeen'=5) & (phase'=3) + 1/15 : (lastSeen'=6) & (phase'=3) + 1/15 : (lastSeen'=7) & (phase'=3) + 1/15 : (lastSeen'=8) & (phase'=3) + 1/15 : (lastSeen'=9) & (phase'=3) + 1/15 : (lastSeen'=10) & (phase'=3) + 1/15 : (lastSeen'=11) & (phase'=3) + 1/15 : (lastSeen'=12) & (phase'=3) + 1/15 : (lastSeen'=13) & (phase'=3) + 1/15 : (lastSeen'=14) & (phase'=3); // if the current member is a bad member, record the most recently seen index - [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); - [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); - [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); - [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); - [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); - [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4); - [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4); - [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4); - [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4); - [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+1) & (phase'=4); - [] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> (observe10'=observe10+1) & (phase'=4); - [] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> (observe11'=observe11+1) & (phase'=4); - [] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> (observe12'=observe12+1) & (phase'=4); - [] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> (observe13'=observe13+1) & (phase'=4); - [] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> (observe14'=observe14+1) & (phase'=4); + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); + [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1: (observe5'=observe5+1) & (phase'=4); + [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1: (observe6'=observe6+1) & (phase'=4); + [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1: (observe7'=observe7+1) & (phase'=4); + [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1: (observe8'=observe8+1) & (phase'=4); + [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1: (observe9'=observe9+1) & (phase'=4); + [] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1: (observe10'=observe10+1) & (phase'=4); + [] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1: (observe11'=observe11+1) & (phase'=4); + [] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1: (observe12'=observe12+1) & (phase'=4); + [] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1: (observe13'=observe13+1) & (phase'=4); + [] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1: (observe14'=observe14+1) & (phase'=4); // good crowd members forward with probability PF and deliver otherwise [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); // deliver the message and start over - [] phase=4 -> (phase'=0); + [] phase=4 -> 1: (phase'=0); endmodule diff --git a/examples/dtmc/crowds/crowds20_5.pm b/examples/dtmc/crowds/crowds20_5.pm index cdbbb61f6..31c63770a 100644 --- a/examples/dtmc/crowds/crowds20_5.pm +++ b/examples/dtmc/crowds/crowds20_5.pm @@ -67,7 +67,7 @@ module crowds lastSeen: [0..CrowdSize - 1] init 0; // get the protocol started - [] phase=0 & runCount (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + [] phase=0 & runCount 1:(phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); // decide whether crowd member is good or bad according to given probabilities [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); @@ -76,32 +76,32 @@ module crowds [] phase=2 & good -> 1/20 : (lastSeen'=0) & (phase'=3) + 1/20 : (lastSeen'=1) & (phase'=3) + 1/20 : (lastSeen'=2) & (phase'=3) + 1/20 : (lastSeen'=3) & (phase'=3) + 1/20 : (lastSeen'=4) & (phase'=3) + 1/20 : (lastSeen'=5) & (phase'=3) + 1/20 : (lastSeen'=6) & (phase'=3) + 1/20 : (lastSeen'=7) & (phase'=3) + 1/20 : (lastSeen'=8) & (phase'=3) + 1/20 : (lastSeen'=9) & (phase'=3) + 1/20 : (lastSeen'=10) & (phase'=3) + 1/20 : (lastSeen'=11) & (phase'=3) + 1/20 : (lastSeen'=12) & (phase'=3) + 1/20 : (lastSeen'=13) & (phase'=3) + 1/20 : (lastSeen'=14) & (phase'=3) + 1/20 : (lastSeen'=15) & (phase'=3) + 1/20 : (lastSeen'=16) & (phase'=3) + 1/20 : (lastSeen'=17) & (phase'=3) + 1/20 : (lastSeen'=18) & (phase'=3) + 1/20 : (lastSeen'=19) & (phase'=3); // if the current member is a bad member, record the most recently seen index - [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); - [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); - [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); - [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); - [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); - [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> (observe5'=observe5+1) & (phase'=4); - [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> (observe6'=observe6+1) & (phase'=4); - [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> (observe7'=observe7+1) & (phase'=4); - [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> (observe8'=observe8+1) & (phase'=4); - [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> (observe9'=observe9+1) & (phase'=4); - [] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> (observe10'=observe10+1) & (phase'=4); - [] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> (observe11'=observe11+1) & (phase'=4); - [] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> (observe12'=observe12+1) & (phase'=4); - [] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> (observe13'=observe13+1) & (phase'=4); - [] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> (observe14'=observe14+1) & (phase'=4); - [] phase=2 & !good & lastSeen=15 & observe15 < TotalRuns -> (observe15'=observe15+1) & (phase'=4); - [] phase=2 & !good & lastSeen=16 & observe16 < TotalRuns -> (observe16'=observe16+1) & (phase'=4); - [] phase=2 & !good & lastSeen=17 & observe17 < TotalRuns -> (observe17'=observe17+1) & (phase'=4); - [] phase=2 & !good & lastSeen=18 & observe18 < TotalRuns -> (observe18'=observe18+1) & (phase'=4); - [] phase=2 & !good & lastSeen=19 & observe19 < TotalRuns -> (observe19'=observe19+1) & (phase'=4); + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1:(observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1:(observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1:(observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1:(observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1:(observe4'=observe4+1) & (phase'=4); + [] phase=2 & !good & lastSeen=5 & observe5 < TotalRuns -> 1:(observe5'=observe5+1) & (phase'=4); + [] phase=2 & !good & lastSeen=6 & observe6 < TotalRuns -> 1:(observe6'=observe6+1) & (phase'=4); + [] phase=2 & !good & lastSeen=7 & observe7 < TotalRuns -> 1:(observe7'=observe7+1) & (phase'=4); + [] phase=2 & !good & lastSeen=8 & observe8 < TotalRuns -> 1:(observe8'=observe8+1) & (phase'=4); + [] phase=2 & !good & lastSeen=9 & observe9 < TotalRuns -> 1:(observe9'=observe9+1) & (phase'=4); + [] phase=2 & !good & lastSeen=10 & observe10 < TotalRuns -> 1:(observe10'=observe10+1) & (phase'=4); + [] phase=2 & !good & lastSeen=11 & observe11 < TotalRuns -> 1:(observe11'=observe11+1) & (phase'=4); + [] phase=2 & !good & lastSeen=12 & observe12 < TotalRuns -> 1:(observe12'=observe12+1) & (phase'=4); + [] phase=2 & !good & lastSeen=13 & observe13 < TotalRuns -> 1:(observe13'=observe13+1) & (phase'=4); + [] phase=2 & !good & lastSeen=14 & observe14 < TotalRuns -> 1:(observe14'=observe14+1) & (phase'=4); + [] phase=2 & !good & lastSeen=15 & observe15 < TotalRuns -> 1:(observe15'=observe15+1) & (phase'=4); + [] phase=2 & !good & lastSeen=16 & observe16 < TotalRuns -> 1:(observe16'=observe16+1) & (phase'=4); + [] phase=2 & !good & lastSeen=17 & observe17 < TotalRuns -> 1:(observe17'=observe17+1) & (phase'=4); + [] phase=2 & !good & lastSeen=18 & observe18 < TotalRuns -> 1:(observe18'=observe18+1) & (phase'=4); + [] phase=2 & !good & lastSeen=19 & observe19 < TotalRuns -> 1:(observe19'=observe19+1) & (phase'=4); // good crowd members forward with probability PF and deliver otherwise [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); // deliver the message and start over - [] phase=4 -> (phase'=0); + [] phase=4 -> 1:(phase'=0); endmodule diff --git a/examples/dtmc/crowds/crowds5_5.pm b/examples/dtmc/crowds/crowds5_5.pm index e1146b586..60bdaa7ea 100644 --- a/examples/dtmc/crowds/crowds5_5.pm +++ b/examples/dtmc/crowds/crowds5_5.pm @@ -37,7 +37,7 @@ module crowds lastSeen: [0..CrowdSize - 1] init 0; // get the protocol started - [] phase=0 & runCount (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); + [] phase=0 & runCount 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); // decide whether crowd member is good or bad according to given probabilities [] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); @@ -46,20 +46,24 @@ module crowds [] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); // if the current member is a bad member, record the most recently seen index - [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> (observe0'=observe0+1) & (phase'=4); - [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> (observe1'=observe1+1) & (phase'=4); - [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> (observe2'=observe2+1) & (phase'=4); - [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> (observe3'=observe3+1) & (phase'=4); - [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> (observe4'=observe4+1) & (phase'=4); + [] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); + [] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); + [] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); + [] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); + [] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); // good crowd members forward with probability PF and deliver otherwise [] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); // deliver the message and start over - [] phase=4 -> (phase'=0); + [] phase=4 -> 1: (phase'=0); endmodule -label "observe0Greater1" = observe0 > 1; -label "observeIGreater1" = observe1 > 1 | observe2 > 1 | observe3 > 1 | observe4 > 1; -label "observeOnlyTrueSender" = observe0 > 1 & observe1 <= 1 & observe2 <= 1 & observe3 <= 1 & observe4 <= 1; \ No newline at end of file +label "observe0Greater1" = observe0>1; +label "observe1Greater1" = observe1>1; +label "observe2Greater1" = observe2>1; +label "observe3Greater1" = observe3>1; +label "observe4Greater1" = observe4>1; +label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; +label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; diff --git a/examples/dtmc/die/die.pm b/examples/dtmc/die/die.pm index f32a1c04b..700951a05 100644 --- a/examples/dtmc/die/die.pm +++ b/examples/dtmc/die/die.pm @@ -1,31 +1,24 @@ -dtmc - -module die - - // local state - s : [0..7] init 0; - // value of the die - d : [0..6] init 0; - - [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); - [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); - [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); - [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); - [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); - [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); - [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); - [] s=7 -> (s'=7); - -endmodule - -rewards "coin_flips" - [] s<7 : 1; -endrewards - -label "one" = s=7&d=1; -label "two" = s=7&d=2; -label "three" = s=7&d=3; -label "four" = s=7&d=4; -label "five" = s=7&d=5; -label "six" = s=7&d=6; -label "done" = s=7; \ No newline at end of file +// Knuth's model of a fair die using only fair coins +dtmc + +module die + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); + [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); + [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); + [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); + [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); + [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); + [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); + [] s=7 -> 1: (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards diff --git a/examples/dtmc/sync/sync.pm b/examples/dtmc/sync/sync.pm new file mode 100644 index 000000000..8bc7f94ce --- /dev/null +++ b/examples/dtmc/sync/sync.pm @@ -0,0 +1,22 @@ +// A simple model using synchronization +dtmc + +module generator + + s : [0..2] init 0; + + [] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=0); + [yield] s=1 -> 1 : (s'=2); + [] s=2 -> 0.5 : (s'=0) + 0.5 : (s'=2); + +endmodule + +module consumer + + t : [0..2] init 0; + + [] t=0 -> 0.8 : (t'=1) + 0.2 : (t'=0); + [yield] t=1 -> 1 : (t'=2); + [] t=2 -> 0.2 : (t'=0) + 0.8 : (t'=2); + +endmodule diff --git a/examples/dtmc/synchronous_leader/leader3_5.pm b/examples/dtmc/synchronous_leader/leader3_5.pm index 0a45ad217..0703e733d 100644 --- a/examples/dtmc/synchronous_leader/leader3_5.pm +++ b/examples/dtmc/synchronous_leader/leader3_5.pm @@ -4,8 +4,8 @@ dtmc // CONSTANTS -const N = 3; // number of processes -const K = 5; // range of probabilistic choice +const int N = 3; // number of processes +const int K = 5; // range of probabilistic choice // counter module used to count the number of processes that have been read // and to know when a process has decided @@ -15,15 +15,15 @@ module counter c : [1..N-1]; // reading - [read] c (c'=c+1); + [read] c 1:(c'=c+1); // finished reading - [read] c=N-1 -> (c'=c); + [read] c=N-1 -> 1:(c'=c); //decide - [done] u1|u2|u3 -> (c'=c); + [done] u1|u2|u3 -> 1:(c'=c); // pick again reset counter - [retry] !(u1|u2|u3) -> (c'=1); + [retry] !(u1|u2|u3) -> 1:(c'=1); // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (c'=c); + [loop] s1=3 -> 1:(c'=c); endmodule @@ -56,18 +56,18 @@ module process1 + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); // read - [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); - [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); + [read] s1=1 & u1 & c 1:(u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c 1:(u1'=false) & (v1'=v2) & (p1'=0); // read and move to decide - [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); - [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); + [read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); + [read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0); // deciding // done - [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); + [done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); //retry - [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); + [retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (s1'=3); + [loop] s1=3 -> 1:(s1'=3); endmodule diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp new file mode 100644 index 000000000..1bc602797 --- /dev/null +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -0,0 +1,563 @@ +#include "src/adapters/ExplicitModelAdapter.h" + +#include "src/storage/SparseMatrix.h" +#include "src/utility/Settings.h" +#include "src/exceptions/WrongFileFormatException.h" + +#include "src/ir/Program.h" +#include "src/ir/RewardModel.h" +#include "src/ir/StateReward.h" +#include "src/ir/TransitionReward.h" + +#include "src/models/AbstractModel.h" +#include "src/models/Dtmc.h" +#include "src/models/Ctmc.h" +#include "src/models/Mdp.h" + +typedef std::pair, std::vector> StateType; + +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +namespace storm { + +namespace adapters { + +ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), + booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), + allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() { + this->initializeVariables(); + storm::settings::Settings* s = storm::settings::instance(); + this->precision = s->get("precision"); +} + +ExplicitModelAdapter::~ExplicitModelAdapter() { + this->clearInternalState(); +} + + std::shared_ptr ExplicitModelAdapter::getModel(std::string const & rewardModelName) { + + + this->buildTransitionMap(); + + std::shared_ptr stateLabeling = this->getStateLabeling(this->program.getLabels()); + std::shared_ptr> stateRewards = nullptr; + + this->rewardModel = nullptr; + if (rewardModelName != "") { + this->rewardModel = std::unique_ptr(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName)));; + if (this->rewardModel != nullptr) { + if (this->rewardModel->hasStateRewards()) { + stateRewards = this->getStateRewards(this->rewardModel->getStateRewards()); + } + } + } + + switch (this->program.getModelType()) + { + case storm::ir::Program::DTMC: + { + std::shared_ptr> matrix = this->buildDeterministicMatrix(); + return std::shared_ptr(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards)); + break; + } + case storm::ir::Program::CTMC: + { + std::shared_ptr> matrix = this->buildDeterministicMatrix(); + return std::shared_ptr(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, this->transitionRewards)); + break; + } + case storm::ir::Program::MDP: + { + std::shared_ptr> matrix = this->buildNondeterministicMatrix(); + return std::shared_ptr(new storm::models::Mdp(matrix, stateLabeling, stateRewards, this->transitionRewards)); + break; + } + case storm::ir::Program::CTMDP: + // Todo + //return std::shared_ptr(new storm::models::Ctmdp(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); + break; + default: + LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: We can't handle this model type."); + throw storm::exceptions::WrongFileFormatException() << "Error while creating model from probabilistic program: We can't handle this model type."; + break; + } + + return std::shared_ptr(nullptr); + } + + void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, bool const value) { + std::get<0>(*state)[index] = value; + } + + void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value) { + std::get<1>(*state)[index] = value; + } + + std::string ExplicitModelAdapter::toString(StateType const * const state) { + std::stringstream ss; + for (unsigned int i = 0; i < state->first.size(); i++) ss << state->first[i] << "\t"; + for (unsigned int i = 0; i < state->second.size(); i++) ss << state->second[i] << "\t"; + return ss.str(); + } + + std::shared_ptr> ExplicitModelAdapter::getStateRewards(std::vector const & rewards) { + std::shared_ptr> results(new std::vector(this->allStates.size())); + for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { + for (auto reward: rewards) { + (*results)[index] = reward.getReward(this->allStates[index]); + } + } + return results; + } + + std::shared_ptr ExplicitModelAdapter::getStateLabeling(std::map> labels) { + std::shared_ptr results(new storm::models::AtomicPropositionsLabeling(this->allStates.size(), labels.size())); + for (auto it: labels) { + results->addAtomicProposition(it.first); + } + for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { + for (auto label: labels) { + if (label.second->getValueAsBool(this->allStates[index])) { + results->addAtomicPropositionToState(label.first, index); + } + } + } + return results; + } + + void ExplicitModelAdapter::initializeVariables() { + uint_fast64_t numberOfIntegerVariables = 0; + uint_fast64_t numberOfBooleanVariables = 0; + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); + numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); + } + + this->booleanVariables.resize(numberOfBooleanVariables); + this->integerVariables.resize(numberOfIntegerVariables); + + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + + for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { + storm::ir::BooleanVariable var = module.getBooleanVariable(j); + this->booleanVariables[var.getIndex()] = var; + this->booleanVariableToIndexMap[var.getName()] = var.getIndex(); + } + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + storm::ir::IntegerVariable var = module.getIntegerVariable(j); + this->integerVariables[var.getIndex()] = var; + this->integerVariableToIndexMap[var.getName()] = var.getIndex(); + } + } + } + + /*! + * Retrieves all active command labeled by some label, ordered by modules. + * + * This function will iterate over all modules and retrieve all commands that are labeled with the given action and active for the current state. + * The result will be a list of lists of commands. + * + * For each module that has appropriately labeled commands, there will be a list. + * If none of these commands is active, this list is empty. + * Note the difference between *no list* and *empty list*: Modules that produce no list are not relevant for this action while an empty list means, that it is not possible to do anything with this label. + * @param state Current state. + * @param action Action label. + * @return Active commands. + */ + std::unique_ptr>> ExplicitModelAdapter::getActiveCommandsByAction(StateType const * state, std::string& action) { + std::unique_ptr>> res = std::unique_ptr>>(new std::list>()); + + // Iterate over all modules. + for (uint_fast64_t i = 0; i < this->program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = this->program.getModule(i); + + std::shared_ptr> ids = module.getCommandsByAction(action); + if (ids->size() == 0) continue; + std::list commands; + + // Look up commands by their id. Add, if guard holds. + for (uint_fast64_t id : *ids) { + storm::ir::Command cmd = module.getCommand(id); + if (cmd.getGuard()->getValueAsBool(state)) { + commands.push_back(module.getCommand(id)); + } + } + res->push_back(commands); + } + // Sort the result in the vague hope that having small lists at the beginning will speed up the expanding. + // This is how lambdas may look like in C++... + res->sort([](const std::list& a, const std::list& b){ return a.size() < b.size(); }); + return res; + } + + /*! + * Apply an update to the given state and return resulting state. + * @params state Current state. + * @params update Update to be applied. + * @return Resulting state. + */ + StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, storm::ir::Update const& update) const { + return this->applyUpdate(state, state, update); + } + + StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const { + StateType* newState = new StateType(*state); + for (auto assignedVariable : update.getBooleanAssignments()) { + setValue(newState, this->booleanVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsBool(baseState)); + } + for (auto assignedVariable : update.getIntegerAssignments()) { + setValue(newState, this->integerVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsInt(baseState)); + } + return newState; + } + + /*! + * Generates all initial states and adds them to allStates. + */ + void ExplicitModelAdapter::generateInitialStates() { + // Create a fresh state which can hold as many boolean and integer variables as there are. + this->allStates.clear(); + this->allStates.push_back(new StateType()); + this->allStates[0]->first.resize(this->booleanVariables.size()); + this->allStates[0]->second.resize(this->integerVariables.size()); + + // Start with boolean variables. + for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) { + // Check if an initial value is given + if (this->booleanVariables[i].getInitialValue().get() == nullptr) { + // No initial value was given. + uint_fast64_t size = this->allStates.size(); + for (uint_fast64_t pos = 0; pos < size; pos++) { + // Duplicate each state, one with true and one with false. + this->allStates.push_back(new StateType(*this->allStates[pos])); + std::get<0>(*this->allStates[pos])[i] = false; + std::get<0>(*this->allStates[size + pos])[i] = true; + } + } else { + // Initial value was given. + bool initialValue = this->booleanVariables[i].getInitialValue()->getValueAsBool(this->allStates[0]); + for (auto it : this->allStates) { + std::get<0>(*it)[i] = initialValue; + } + } + } + // Now process integer variables. + for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) { + // Check if an initial value was given. + if (this->integerVariables[i].getInitialValue().get() == nullptr) { + // No initial value was given. + uint_fast64_t size = this->allStates.size(); + int_fast64_t lower = this->integerVariables[i].getLowerBound()->getValueAsInt(this->allStates[0]); + int_fast64_t upper = this->integerVariables[i].getUpperBound()->getValueAsInt(this->allStates[0]); + + // Duplicate all states for all values in variable interval. + for (int_fast64_t value = lower; value <= upper; value++) { + for (uint_fast64_t pos = 0; pos < size; pos++) { + // If value is lower bound, we reuse the existing state, otherwise we create a new one. + if (value > lower) this->allStates.push_back(new StateType(*this->allStates[pos])); + // Set value to current state. + std::get<1>(*this->allStates[(value - lower) * size + pos])[i] = value; + } + } + } else { + // Initial value was given. + int_fast64_t initialValue = this->integerVariables[i].getInitialValue()->getValueAsInt(this->allStates[0]); + for (auto it : this->allStates) { + std::get<1>(*it)[i] = initialValue; + } + } + } + stateToIndexMap[this->allStates[0]] = 0; + LOG4CPLUS_DEBUG(logger, "Generated " << this->allStates.size() << " initial states."); + } + + /*! + * Retrieves the state id of the given state. + * If the state has not been hit yet, it will be added to allStates and given a new id. + * In this case, the pointer must not be deleted, as it is used within allStates. + * If the state is already known, the pointer is deleted and the old state id is returned. + * Hence, the given state pointer should not be used afterwards. + * @param state Pointer to state, shall not be used afterwards. + * @returns State id of given state. + */ + uint_fast64_t ExplicitModelAdapter::getOrAddStateId(StateType * state) { + // Check, if we already know this state at all. + auto indexIt = this->stateToIndexMap.find(state); + if (indexIt == this->stateToIndexMap.end()) { + // No, add to allStates, initialize index. + allStates.push_back(state); + stateToIndexMap[state] = allStates.size()-1; + return allStates.size()-1; + } else { + // Yes, obtain index and delete state object. + delete state; + return indexIt->second; + } + } + + /*! + * Expands all unlabeled transitions for a given state and adds them to the given list of results. + * @params state State to be explored. + * @params res Intermediate transition map. + */ + void ExplicitModelAdapter::addUnlabeledTransitions(const uint_fast64_t stateID, std::list>>& res) { + const StateType* state = this->allStates[stateID]; + // Iterate over all modules. + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + // Iterate over all commands. + for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { + storm::ir::Command const& command = module.getCommand(j); + // Only consider unlabeled commands. + if (command.getActionName() != "") continue; + // Omit, if command is not active. + if (!command.getGuard()->getValueAsBool(state)) continue; + + // Add a new map and get pointer. + res.emplace_back(); + std::map* states = &res.back().second; + double probSum = 0; + + // Iterate over all updates. + for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { + // Obtain new state id. + storm::ir::Update const& update = command.getUpdate(k); + uint_fast64_t newStateId = this->getOrAddStateId(this->applyUpdate(state, update)); + + probSum += update.getLikelihoodExpression()->getValueAsDouble(state); + // Check, if we already know this state, add up probabilities for every state. + auto stateIt = states->find(newStateId); + if (stateIt == states->end()) { + (*states)[newStateId] = update.getLikelihoodExpression()->getValueAsDouble(state); + this->numberOfTransitions++; + } else { + (*states)[newStateId] += update.getLikelihoodExpression()->getValueAsDouble(state); + } + } + if (std::abs(1 - probSum) > this->precision) { + LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString()); + throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString(); + } + } + } + } + + /*! + * Explores reachable state from given state by using labeled transitions. + * Found transitions are stored in given map. + * @param stateID State to be explored. + * @param res Intermediate transition map. + */ + void ExplicitModelAdapter::addLabeledTransitions(const uint_fast64_t stateID, std::list>>& res) { + // Create a copy of the current state, as we will free intermediate states... + for (std::string action : this->program.getActions()) { + StateType* state = new StateType(*this->allStates[stateID]); + std::unique_ptr>> cmds = this->getActiveCommandsByAction(state, action); + + // Start with current state + std::unordered_map resultStates; + resultStates[state] = 1.0; + + for (std::list module : *cmds) { + if (resultStates.size() == 0) break; + std::unordered_map newStates; + + // Iterate over all commands within this module. + for (storm::ir::Command command : module) { + // Iterate over all updates of this command. + double probSum = 0; + for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { + storm::ir::Update const update = command.getUpdate(k); + + // Iterate over all resultStates. + for (auto it : resultStates) { + // Apply the new update and get resulting state. + StateType* newState = this->applyUpdate(it.first, this->allStates[stateID], update); + probSum += update.getLikelihoodExpression()->getValueAsDouble(it.first); + // Insert the new state into newStates array. + // Take care of calculation of likelihood, combine identical states. + auto s = newStates.find(newState); + if (s == newStates.end()) { + newStates[newState] = it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); + } else { + newStates[newState] += it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); + } + } + } + if (std::abs(1 - probSum) > this->precision) { + LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString()); + throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString(); + } + } + for (auto it: resultStates) { + delete it.first; + } + // Move new states to resultStates. + resultStates.clear(); + resultStates.insert(newStates.begin(), newStates.end()); + + } + + if (resultStates.size() > 0) { + res.push_back(std::make_pair(action, std::map())); + std::map* states = &res.back().second; + + // Now add our final result states to our global result. + for (auto it : resultStates) { + uint_fast64_t newStateID = this->getOrAddStateId(it.first); + (*states)[newStateID] = it.second; + } + this->numberOfTransitions += states->size(); + } + } + + } + + /*! + * Create matrix from intermediate mapping, assuming it is a dtmc model. + * @param intermediate Intermediate representation of transition mapping. + * @return result matrix. + */ + std::shared_ptr> ExplicitModelAdapter::buildDeterministicMatrix() { + // ***** ATTENTION ***** + // this->numberOfTransitions is meaningless, as we combine all choices into one for each state. + // Hence, we compute the correct number of transitions now. + uint_fast64_t numberOfTransitions = 0; + for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { + // Collect all target nodes in a set to get number of distinct nodes. + std::set set; + for (auto choice : transitionMap[state]) { + for (auto elem : choice.second) { + set.insert(elem.first); + } + } + numberOfTransitions += set.size(); + } + LOG4CPLUS_INFO(logger, "Building deterministic transition matrix: " << allStates.size() << " x " << allStates.size() << " with " << numberOfTransitions << " transitions."); + // Now build matrix. + + std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size())); + result->initialize(numberOfTransitions); + if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { + this->transitionRewards = std::shared_ptr>(new storm::storage::SparseMatrix(allStates.size())); + this->transitionRewards->initialize(numberOfTransitions); + } + for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { + if (transitionMap[state].size() > 1) { + LOG4CPLUS_WARN(logger, "State " << state << " has " << transitionMap[state].size() << " overlapping guards in deterministic model."); + } + // Combine choices to one map. + std::map map; + std::map rewardMap; + for (auto choice : transitionMap[state]) { + for (auto elem : choice.second) { + map[elem.first] += elem.second; + if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { + for (auto reward : this->rewardModel->getTransitionRewards()) { + rewardMap[elem.first] += reward.getReward(choice.first, this->allStates[state]); + } + } + } + } + // Scale probabilities by number of choices. + double factor = 1.0 / transitionMap[state].size(); + for (auto it : map) { + result->addNextValue(state, it.first, it.second * factor); + if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { + this->transitionRewards->addNextValue(state, it.first, rewardMap[it.first] * factor); + } + } + + } + result->finalize(); + return result; + } + + /*! + * Create matrix from intermediate mapping, assuming it is a mdp model. + * @param intermediate Intermediate representation of transition mapping. + * @param choices Overall number of choices for all nodes. + * @return result matrix. + */ + std::shared_ptr> ExplicitModelAdapter::buildNondeterministicMatrix() { + LOG4CPLUS_INFO(logger, "Building nondeterministic transition matrix: " << this->numberOfChoices << " x " << allStates.size() << " with " << this->numberOfTransitions << " transitions."); + std::shared_ptr> result(new storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); + result->initialize(this->numberOfTransitions); + if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { + this->transitionRewards = std::shared_ptr>(new storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); + this->transitionRewards->initialize(this->numberOfTransitions); + } + // Build matrix. + uint_fast64_t nextRow = 0; + for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { + for (auto choice : transitionMap[state]) { + for (auto it : choice.second) { + result->addNextValue(nextRow, it.first, it.second); + if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { + double rewardValue = 0; + for (auto reward : this->rewardModel->getTransitionRewards()) { + rewardValue = reward.getReward(choice.first, this->allStates[state]); + } + this->transitionRewards->addNextValue(nextRow, it.first, rewardValue); + } + } + nextRow++; + } + } + result->finalize(); + return result; + } + + /*! + * Build matrix from model. Starts with all initial states and explores the reachable state space. + * While exploring, the transitions are stored in a temporary map. + * Afterwards, we transform this map into the actual matrix. + * @return result matrix. + */ + void ExplicitModelAdapter::buildTransitionMap() { + LOG4CPLUS_DEBUG(logger, "Starting to create transition map from program..."); + this->clearInternalState(); + + this->generateInitialStates(); + for (uint_fast64_t curIndex = 0; curIndex < this->allStates.size(); curIndex++) + { + this->addUnlabeledTransitions(curIndex, this->transitionMap[curIndex]); + this->addLabeledTransitions(curIndex, this->transitionMap[curIndex]); + + this->numberOfChoices += this->transitionMap[curIndex].size(); + if (this->transitionMap[curIndex].size() == 0) { + // This is a deadlock state. + if (storm::settings::instance()->isSet("fix-deadlocks")) { + this->numberOfTransitions++; + this->numberOfChoices++; + this->transitionMap[curIndex].emplace_back(); + this->transitionMap[curIndex].back().second[curIndex] = 1; + } else { + LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state."); + throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state."; + } + } + } + LOG4CPLUS_DEBUG(logger, "Finished creating transition map."); + } + + void ExplicitModelAdapter::clearInternalState() { + for (auto it : allStates) { + delete it; + } + allStates.clear(); + stateToIndexMap.clear(); + this->numberOfTransitions = 0; + this->numberOfChoices = 0; + this->transitionRewards = nullptr; + this->transitionMap.clear(); + } + +} // namespace adapters + +} // namespace storm diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h new file mode 100644 index 000000000..63cd91646 --- /dev/null +++ b/src/adapters/ExplicitModelAdapter.h @@ -0,0 +1,206 @@ +/* + * File: ExplicitModelAdapter.h + * Author: Gereon Kremer + * + * Created on March 15, 2013, 11:42 AM + */ + +#ifndef EXPLICITMODELADAPTER_H +#define EXPLICITMODELADAPTER_H + +#include +#include +#include +#include +#include + +#include "src/ir/Program.h" +#include "src/ir/StateReward.h" +#include "src/ir/TransitionReward.h" + +#include "src/models/AbstractModel.h" +#include "src/models/AtomicPropositionsLabeling.h" +#include "src/storage/SparseMatrix.h" + +namespace storm { +namespace adapters { + +/*! + * Model state, represented by the values of all variables. + */ +typedef std::pair, std::vector> StateType; + +class StateHash { +public: + std::size_t operator()(StateType* state) const { + size_t seed = 0; + for (auto it : state->first) { + boost::hash_combine(seed, it); + } + for (auto it : state->second) { + boost::hash_combine(seed, it); + } + return seed; + } +}; + +class StateCompare { +public: + bool operator()(StateType* state1, StateType* state2) const { + return *state1 == *state2; + } +}; + +class ExplicitModelAdapter { +public: + ExplicitModelAdapter(storm::ir::Program program); + ~ExplicitModelAdapter(); + + std::shared_ptr getModel(std::string const & rewardModelName = ""); + +private: + + double precision; + + // First some generic routines to operate on states. + + /*! + * Set some boolean variable in the given state object. + * @param state State to be changed. + * @param index Index of boolean variable. + * @param value New value. + */ + static void setValue(StateType* const state, uint_fast64_t const index, bool const value); + /*! + * Set some integer variable in the given state object. + * @param state State to be changed. + * @param index Index of integer variable. + * @param value New value. + */ + static void setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value); + static std::string toString(StateType const * const state); + /*! + * Apply an update to the given state and return the resulting new state object. + * This methods creates a copy of the given state. + * @params state Current state. + * @params update Update to be applied. + * @return Resulting state. + */ + StateType* applyUpdate(StateType const * const state, storm::ir::Update const& update) const; + /*! + * Apply an update to a given state and return the resulting new state object. + * Updates are done using the variable values from a given baseState. + * @params state State to be updated. + * @params baseState State used for update variables. + * @params update Update to be applied. + * @return Resulting state. + */ + StateType* applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const; + + /*! + * Reads and combines variables from all program modules and stores them. + * Also creates a map to obtain a variable index from a variable map efficiently. + */ + void initializeVariables(); + + std::shared_ptr> getStateRewards(std::vector const & rewards); + std::shared_ptr getStateLabeling(std::map> labels); + + /*! + * Retrieves all active command labeled by some label, ordered by modules. + * + * This function will iterate over all modules and retrieve all commands that are labeled with the given action and active for the current state. + * The result will be a list of lists of commands. + * + * For each module that has appropriately labeled commands, there will be a list. + * If none of these commands is active, this list is empty. + * Note the difference between *no list* and *empty list*: Modules that produce no list are not relevant for this action while an empty list means, that it is not possible to do anything with this label. + * @param state Current state. + * @param action Action label. + * @return Active commands. + */ + std::unique_ptr>> getActiveCommandsByAction(StateType const * state, std::string& action); + + /*! + * Generates all initial states and adds them to allStates. + */ + void generateInitialStates(); + + /*! + * Retrieves the state id of the given state. + * If the state has not been hit yet, it will be added to allStates and given a new id. + * In this case, the pointer must not be deleted, as it is used within allStates. + * If the state is already known, the pointer is deleted and the old state id is returned. + * Hence, the given state pointer should not be used afterwards. + * @param state Pointer to state, shall not be used afterwards. + * @returns State id of given state. + */ + uint_fast64_t getOrAddStateId(StateType * state); + + /*! + * Expands all unlabeled transitions for a given state and adds them to the given list of results. + * @params state State to be explored. + * @params res Intermediate transition map. + */ + void addUnlabeledTransitions(const uint_fast64_t stateID, std::list>>& res); + + /*! + * Explores reachable state from given state by using labeled transitions. + * Found transitions are stored in given map. + * @param stateID State to be explored. + * @param res Intermediate transition map. + */ + void addLabeledTransitions(const uint_fast64_t stateID, std::list>>& res); + + /*! + * Create matrix from intermediate mapping, assuming it is a dtmc model. + * @param intermediate Intermediate representation of transition mapping. + * @return result matrix. + */ + std::shared_ptr> buildDeterministicMatrix(); + + /*! + * Create matrix from intermediate mapping, assuming it is a mdp model. + * @param intermediate Intermediate representation of transition mapping. + * @param choices Overall number of choices for all nodes. + * @return result matrix. + */ + std::shared_ptr> buildNondeterministicMatrix(); + + /*! + * Build matrix from model. Starts with all initial states and explores the reachable state space. + * While exploring, the transitions are stored in a temporary map. + * Afterwards, we transform this map into the actual matrix. + * @return result matrix. + */ + void buildTransitionMap(); + + void clearInternalState(); + + // Program that should be converted. + storm::ir::Program program; + std::vector booleanVariables; + std::vector integerVariables; + std::map booleanVariableToIndexMap; + std::map integerVariableToIndexMap; + + // Members that are filled during the conversion. + std::unique_ptr rewardModel; + std::vector allStates; + std::unordered_map stateToIndexMap; + uint_fast64_t numberOfTransitions; + uint_fast64_t numberOfChoices; + std::shared_ptr> transitionRewards; + + /*! + * Maps a source node to a list of probability distributions over target nodes. + * Each such distribution corresponds to an unlabeled command or a feasible combination of labeled commands. + * Therefore, each distribution is represented by a label and a mapping from target nodes to their probabilities. + */ + std::map>>> transitionMap; +}; + +} // namespace adapters +} // namespace storm + +#endif /* EXPLICITMODELADAPTER_H */ diff --git a/src/adapters/SymbolicExpressionAdapter.h b/src/adapters/SymbolicExpressionAdapter.h new file mode 100644 index 000000000..2e07bae83 --- /dev/null +++ b/src/adapters/SymbolicExpressionAdapter.h @@ -0,0 +1,231 @@ +/* + * SymbolicExpressionAdapter.h + * + * Created on: 27.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ +#define STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ + +#include "src/ir/expressions/ExpressionVisitor.h" +#include "src/exceptions/ExpressionEvaluationException.h" + +#include "cuddObj.hh" + +#include +#include + +namespace storm { + +namespace adapters { + +class SymbolicExpressionAdapter : public storm::ir::expressions::ExpressionVisitor { +public: + SymbolicExpressionAdapter(std::unordered_map>& variableToDecisionDiagramVariableMap) : stack(), variableToDecisionDiagramVariableMap(variableToDecisionDiagramVariableMap) { + + } + + ADD* translateExpression(std::shared_ptr expression) { + expression->accept(this); + return stack.top(); + } + + virtual void visit(storm::ir::expressions::BaseExpression* expression) { + std::cout << expression->toString() << std::endl; + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression " + << " of abstract superclass type."; + } + + virtual void visit(storm::ir::expressions::BinaryBooleanFunctionExpression* expression) { + expression->getLeft()->accept(this); + expression->getRight()->accept(this); + + ADD* rightResult = stack.top(); + stack.pop(); + ADD* leftResult = stack.top(); + stack.pop(); + + switch(expression->getFunctionType()) { + case storm::ir::expressions::BinaryBooleanFunctionExpression::AND: + stack.push(new ADD(leftResult->Times(*rightResult))); + break; + case storm::ir::expressions::BinaryBooleanFunctionExpression::OR: + stack.push(new ADD(leftResult->Plus(*rightResult))); + break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; + } + + // delete leftResult; + // delete rightResult; + } + + virtual void visit(storm::ir::expressions::BinaryNumericalFunctionExpression* expression) { + expression->getLeft()->accept(this); + expression->getRight()->accept(this); + + ADD* rightResult = stack.top(); + stack.pop(); + ADD* leftResult = stack.top(); + stack.pop(); + + switch(expression->getFunctionType()) { + case storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS: + stack.push(new ADD(leftResult->Plus(*rightResult))); + break; + case storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS: + stack.push(new ADD(leftResult->Minus(*rightResult))); + break; + case storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES: + stack.push(new ADD(leftResult->Times(*rightResult))); + break; + case storm::ir::expressions::BinaryNumericalFunctionExpression::DIVIDE: + stack.push(new ADD(leftResult->Divide(*rightResult))); + break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; + } + } + + virtual void visit(storm::ir::expressions::BinaryRelationExpression* expression) { + expression->getLeft()->accept(this); + expression->getRight()->accept(this); + + ADD* rightResult = stack.top(); + stack.pop(); + ADD* leftResult = stack.top(); + stack.pop(); + + switch(expression->getRelationType()) { + case storm::ir::expressions::BinaryRelationExpression::EQUAL: + stack.push(new ADD(leftResult->Equals(*rightResult))); + break; + case storm::ir::expressions::BinaryRelationExpression::NOT_EQUAL: + stack.push(new ADD(leftResult->NotEquals(*rightResult))); + break; + case storm::ir::expressions::BinaryRelationExpression::LESS: + stack.push(new ADD(leftResult->LessThan(*rightResult))); + break; + case storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL: + stack.push(new ADD(leftResult->LessThanOrEqual(*rightResult))); + break; + case storm::ir::expressions::BinaryRelationExpression::GREATER: + stack.push(new ADD(leftResult->GreaterThan(*rightResult))); + break; + case storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL: + stack.push(new ADD(leftResult->GreaterThanOrEqual(*rightResult))); + break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << expression->getRelationType() << "'."; + } + } + + virtual void visit(storm::ir::expressions::BooleanConstantExpression* expression) { + if (!expression->isDefined()) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Boolean constant '" << expression->getConstantName() << "' is undefined."; + } + + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + stack.push(new ADD(*cuddUtility->getConstant(expression->getValue() ? 1 : 0))); + } + + virtual void visit(storm::ir::expressions::BooleanLiteral* expression) { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsBool(nullptr) ? 1 : 0))); + } + + virtual void visit(storm::ir::expressions::DoubleConstantExpression* expression) { + if (expression->isDefined()) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Double constant '" << expression->getConstantName() << "' is undefined."; + } + + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + stack.push(new ADD(*cuddUtility->getConstant(expression->getValue()))); + } + + virtual void visit(storm::ir::expressions::DoubleLiteral* expression) { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsDouble(nullptr)))); + } + + virtual void visit(storm::ir::expressions::IntegerConstantExpression* expression) { + if (!expression->isDefined()) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Integer constant '" << expression->getConstantName() << "' is undefined."; + } + + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + stack.push(new ADD(*cuddUtility->getConstant(expression->getValue()))); + } + + virtual void visit(storm::ir::expressions::IntegerLiteral* expression) { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsInt(nullptr)))); + } + + virtual void visit(storm::ir::expressions::UnaryBooleanFunctionExpression* expression) { + expression->getChild()->accept(this); + + ADD* childResult = stack.top(); + stack.pop(); + + switch (expression->getFunctionType()) { + case storm::ir::expressions::UnaryBooleanFunctionExpression::NOT: + stack.push(new ADD(~(*childResult))); + break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean unary operator: '" << expression->getFunctionType() << "'."; + } + } + + virtual void visit(storm::ir::expressions::UnaryNumericalFunctionExpression* expression) { + expression->getChild()->accept(this); + + ADD* childResult = stack.top(); + stack.pop(); + + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + ADD* result = cuddUtility->getConstant(0); + switch(expression->getFunctionType()) { + case storm::ir::expressions::UnaryNumericalFunctionExpression::MINUS: + stack.push(new ADD(result->Minus(*childResult))); + break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numerical unary operator: '" << expression->getFunctionType() << "'."; + } + + } + + virtual void visit(storm::ir::expressions::VariableExpression* expression) { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + + std::vector const& variables = variableToDecisionDiagramVariableMap[expression->getVariableName()]; + + ADD* result = cuddUtility->getConstant(0); + if (expression->getType() == storm::ir::expressions::BaseExpression::bool_) { + cuddUtility->setValueAtIndex(result, 1, variables, 1); + } else { + int64_t low = expression->getLowerBound()->getValueAsInt(nullptr); + int64_t high = expression->getUpperBound()->getValueAsInt(nullptr); + + for (uint_fast64_t i = low; i <= high; ++i) { + cuddUtility->setValueAtIndex(result, i - low, variables, i); + } + } + + stack.push(result); + } + +private: + std::stack stack; + std::unordered_map>& variableToDecisionDiagramVariableMap; +}; + +} // namespace adapters + +} // namespace storm + +#endif /* STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ */ diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h new file mode 100644 index 000000000..f42d8f873 --- /dev/null +++ b/src/adapters/SymbolicModelAdapter.h @@ -0,0 +1,289 @@ +/* + * SymbolicModelAdapter.h + * + * Created on: 25.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ +#define STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ + +#include "src/exceptions/WrongFileFormatException.h" + +#include "src/utility/CuddUtility.h" +#include "SymbolicExpressionAdapter.h" + +#include "cuddObj.hh" +#include +#include + +namespace storm { + +namespace adapters { + +class SymbolicModelAdapter { +public: + + SymbolicModelAdapter() : cuddUtility(storm::utility::cuddUtilityInstance()), allDecisionDiagramVariables(), + allRowDecisionDiagramVariables(), allColumnDecisionDiagramVariables(), booleanRowDecisionDiagramVariables(), + integerRowDecisionDiagramVariables(), booleanColumnDecisionDiagramVariables(), integerColumnDecisionDiagramVariables(), + variableToRowDecisionDiagramVariableMap(), variableToColumnDecisionDiagramVariableMap(), + variableToIdentityDecisionDiagramMap(), + rowExpressionAdapter(variableToRowDecisionDiagramVariableMap), columnExpressionAdapter(variableToColumnDecisionDiagramVariableMap) { + + } + + void toMTBDD(storm::ir::Program const& program) { + LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program."); + createDecisionDiagramVariables(program); + createIdentityDecisionDiagrams(program); + + ADD* systemAdd = cuddUtility->getZero(); + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + + ADD* moduleAdd = cuddUtility->getZero(); + for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { + storm::ir::Command const& command = module.getCommand(j); + + ADD* commandAdd = cuddUtility->getZero(); + + ADD* guard = rowExpressionAdapter.translateExpression(command.getGuard()); + if (*guard != *cuddUtility->getZero()) { + for (uint_fast64_t i = 0; i < command.getNumberOfUpdates(); ++i) { + ADD* updateAdd = cuddUtility->getOne(); + + storm::ir::Update const& update = command.getUpdate(i); + + std::map booleanAssignments = update.getBooleanAssignments(); + for (auto assignmentPair : booleanAssignments) { + ADD* updateExpr = rowExpressionAdapter.translateExpression(assignmentPair.second.getExpression()); + + ADD* temporary = cuddUtility->getZero(); + cuddUtility->setValueAtIndex(temporary, 0, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], 0); + cuddUtility->setValueAtIndex(temporary, 1, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], 1); + + ADD* result = new ADD(*updateExpr * *guard); + result = new ADD(result->Equals(*temporary)); + + *updateAdd = *updateAdd * *result; + } + + std::map integerAssignments = update.getIntegerAssignments(); + for (auto assignmentPair : integerAssignments) { + ADD* updateExpr = rowExpressionAdapter.translateExpression(assignmentPair.second.getExpression()); + + ADD* temporary = cuddUtility->getZero(); + + uint_fast64_t variableIndex = module.getIntegerVariableIndex(assignmentPair.first); + storm::ir::IntegerVariable integerVariable = module.getIntegerVariable(variableIndex); + int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr); + int_fast64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr); + + for (uint_fast64_t i = low; i <= high; ++i) { + cuddUtility->setValueAtIndex(temporary, i - low, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], i); + } + + ADD* result = new ADD(*updateExpr * *guard); + result = new ADD(result->Equals(*temporary)); + *result *= *guard; + + *updateAdd = *updateAdd * *result; + } + for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); ++i) { + storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(i); + + if (update.getBooleanAssignments().find(booleanVariable.getName()) == update.getBooleanAssignments().end()) { + *updateAdd = *updateAdd * *variableToIdentityDecisionDiagramMap[booleanVariable.getName()]; + } + } + for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); ++i) { + storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(i); + + if (update.getIntegerAssignments().find(integerVariable.getName()) == update.getIntegerAssignments().end()) { + *updateAdd = *updateAdd * *variableToIdentityDecisionDiagramMap[integerVariable.getName()]; + } + } + + *commandAdd += *updateAdd * *cuddUtility->getConstant(update.getLikelihoodExpression()->getValueAsDouble(nullptr)); + } + *moduleAdd += *commandAdd; + } else { + LOG4CPLUS_WARN(logger, "Guard " << command.getGuard()->toString() << " is unsatisfiable."); + } + } + *systemAdd += *moduleAdd; + } + + performReachability(program, systemAdd); + + LOG4CPLUS_INFO(logger, "Done creating MTBDD representation for probabilistic program."); + } + +private: + storm::utility::CuddUtility* cuddUtility; + + std::vector allDecisionDiagramVariables; + std::vector allRowDecisionDiagramVariables; + std::vector allColumnDecisionDiagramVariables; + std::vector booleanRowDecisionDiagramVariables; + std::vector integerRowDecisionDiagramVariables; + std::vector booleanColumnDecisionDiagramVariables; + std::vector integerColumnDecisionDiagramVariables; + std::unordered_map> variableToRowDecisionDiagramVariableMap; + std::unordered_map> variableToColumnDecisionDiagramVariableMap; + + std::unordered_map variableToIdentityDecisionDiagramMap; + + SymbolicExpressionAdapter rowExpressionAdapter; + SymbolicExpressionAdapter columnExpressionAdapter; + + ADD* getInitialStateDecisionDiagram(storm::ir::Program const& program) { + ADD* initialStates = cuddUtility->getOne(); + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + + for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { + storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); + bool initialValue = booleanVariable.getInitialValue()->getValueAsBool(nullptr); + *initialStates *= *cuddUtility->getConstantEncoding(1, variableToRowDecisionDiagramVariableMap[booleanVariable.getName()]); + } + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); + int_fast64_t initialValue = integerVariable.getInitialValue()->getValueAsInt(nullptr); + int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr); + *initialStates *= *cuddUtility->getConstantEncoding(initialValue - low, variableToRowDecisionDiagramVariableMap[integerVariable.getName()]); + } + } + + cuddUtility->dumpDotToFile(initialStates, "initstates.add"); + return initialStates; + } + + void performReachability(storm::ir::Program const& program, ADD* systemAdd) { + ADD* systemAdd01 = new ADD(systemAdd->GreaterThan(*cuddUtility->getZero())); + cuddUtility->dumpDotToFile(systemAdd01, "system01.add"); + + cuddUtility->dumpDotToFile(systemAdd, "reachtransold.add"); + ADD* reachableStates = getInitialStateDecisionDiagram(program); + cuddUtility->dumpDotToFile(reachableStates, "init.add"); + ADD* newReachableStates = new ADD(*reachableStates); + + ADD* rowCube = cuddUtility->getOne(); + for (auto variablePtr : allRowDecisionDiagramVariables) { + *rowCube *= *variablePtr; + } + + bool changed; + int iter = 0; + do { + changed = false; + *newReachableStates = *reachableStates * *systemAdd01; + newReachableStates = new ADD(newReachableStates->ExistAbstract(*rowCube)); + + cuddUtility->dumpDotToFile(newReachableStates, "reach1.add"); + + newReachableStates = cuddUtility->permuteVariables(newReachableStates, allColumnDecisionDiagramVariables, allRowDecisionDiagramVariables, allDecisionDiagramVariables.size()); + + *newReachableStates += *reachableStates; + newReachableStates = new ADD(newReachableStates->GreaterThan(*cuddUtility->getZero())); + + if (*newReachableStates != *reachableStates) changed = true; + *reachableStates = *newReachableStates; + } while (changed); + + *systemAdd *= *reachableStates; + std::cout << "got " << systemAdd->nodeCount() << " nodes" << std::endl; + std::cout << "and " << systemAdd->CountMinterm(allRowDecisionDiagramVariables.size() + allColumnDecisionDiagramVariables.size()) << std::endl; + } + + void createIdentityDecisionDiagrams(storm::ir::Program const& program) { + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + + for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { + storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); + ADD* identity = cuddUtility->getZero(); + cuddUtility->setValueAtIndices(identity, 0, 0, + variableToRowDecisionDiagramVariableMap[booleanVariable.getName()], + variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()], 1); + cuddUtility->setValueAtIndices(identity, 1, 1, + variableToRowDecisionDiagramVariableMap[booleanVariable.getName()], + variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()], 1); + variableToIdentityDecisionDiagramMap[booleanVariable.getName()] = identity; + } + + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); + + ADD* identity = cuddUtility->getZero(); + + int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr); + int_fast64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr); + + for (uint_fast64_t i = low; i <= high; ++i) { + cuddUtility->setValueAtIndices(identity, i - low, i - low, + variableToRowDecisionDiagramVariableMap[integerVariable.getName()], + variableToColumnDecisionDiagramVariableMap[integerVariable.getName()], 1); + } + variableToIdentityDecisionDiagramMap[integerVariable.getName()] = identity; + } + } + } + + void createDecisionDiagramVariables(storm::ir::Program const& program) { + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + + for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { + storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); + + ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + variableToRowDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newRowDecisionDiagramVariable); + booleanRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + + ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newColumnDecisionDiagramVariable); + booleanColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + } + + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); + uint_fast64_t integerRange = integerVariable.getUpperBound()->getValueAsInt(nullptr) - integerVariable.getLowerBound()->getValueAsInt(nullptr); + if (integerRange <= 0) { + throw storm::exceptions::WrongFileFormatException() << "Range of variable " + << integerVariable.getName() << " is empty or negativ."; + } + uint_fast64_t numberOfDecisionDiagramVariables = static_cast(std::ceil(std::log2(integerRange))); + + std::vector allRowDecisionDiagramVariablesForVariable; + std::vector allColumnDecisionDiagramVariablesForVariable; + for (uint_fast64_t k = 0; k < numberOfDecisionDiagramVariables; ++k) { + ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + allRowDecisionDiagramVariablesForVariable.push_back(newRowDecisionDiagramVariable); + integerRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + + ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + allColumnDecisionDiagramVariablesForVariable.push_back(newColumnDecisionDiagramVariable); + integerColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + } + variableToRowDecisionDiagramVariableMap[integerVariable.getName()] = allRowDecisionDiagramVariablesForVariable; + variableToColumnDecisionDiagramVariableMap[integerVariable.getName()] = allColumnDecisionDiagramVariablesForVariable; + } + } + } +}; + +} // namespace adapters + +} // namespace storm + +#endif /* STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ */ diff --git a/src/exceptions/ExpressionEvaluationException.h b/src/exceptions/ExpressionEvaluationException.h new file mode 100644 index 000000000..390991c1d --- /dev/null +++ b/src/exceptions/ExpressionEvaluationException.h @@ -0,0 +1,23 @@ +/* + * ExpressionEvaluationException.h + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ +#define STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace storm { + +namespace exceptions { + +STORM_EXCEPTION_DEFINE_NEW(ExpressionEvaluationException) + +} + +} + +#endif /* STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ */ diff --git a/src/exceptions/NotImplementedException.h b/src/exceptions/NotImplementedException.h new file mode 100644 index 000000000..cf98d4d99 --- /dev/null +++ b/src/exceptions/NotImplementedException.h @@ -0,0 +1,23 @@ +/* + * NotImplementedException.h + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ +#define STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ + +#include "src/exceptions/BaseException.h" + +namespace storm { + +namespace exceptions { + +STORM_EXCEPTION_DEFINE_NEW(NotImplementedException) + +} + +} + +#endif /* STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ */ diff --git a/src/ir/Assignment.cpp b/src/ir/Assignment.cpp new file mode 100644 index 000000000..232472857 --- /dev/null +++ b/src/ir/Assignment.cpp @@ -0,0 +1,53 @@ +/* + * Assignment.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "Assignment.h" + +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +Assignment::Assignment() : variableName(), expression() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +Assignment::Assignment(std::string variableName, std::shared_ptr expression) + : variableName(variableName), expression(expression) { + // Nothing to do here. +} + +Assignment::Assignment(const Assignment& assignment, const std::map& renaming, const std::map& bools, const std::map& ints) + : variableName(assignment.variableName), expression(assignment.expression->clone(renaming, bools, ints)) { + if (renaming.count(assignment.variableName) > 0) { + this->variableName = renaming.at(assignment.variableName); + } +} + +// Returns the name of the variable associated with this assignment. +std::string const& Assignment::getVariableName() const { + return variableName; +} + +// Returns the expression associated with this assignment. +std::shared_ptr const& Assignment::getExpression() const { + return expression; +} + +// Build a string representation of the assignment. +std::string Assignment::toString() const { + std::stringstream result; + result << "(" << variableName << "' = " << expression->toString() << ")"; + return result.str(); +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h new file mode 100644 index 000000000..b17693bf0 --- /dev/null +++ b/src/ir/Assignment.h @@ -0,0 +1,68 @@ +/* + * Assignment.h + * + * Created on: 06.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_ASSIGNMENT_H_ +#define STORM_IR_ASSIGNMENT_H_ + +#include "expressions/BaseExpression.h" + +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing the assignment of an expression to a variable. + */ +class Assignment { +public: + /*! + * Default constructor. Creates an empty assignment. + */ + Assignment(); + + /*! + * Constructs an assignment using the given variable name and expression. + * @param variableName the variable that this assignment targets. + * @param expression the expression to assign to the variable. + */ + Assignment(std::string variableName, std::shared_ptr expression); + + Assignment(const Assignment& assignment, const std::map& renaming, const std::map& bools, const std::map& ints); + + /*! + * Retrieves the name of the variable that this assignment targets. + * @returns the name of the variable that this assignment targets. + */ + std::string const& getVariableName() const; + + /*! + * Retrieves the expression that is assigned to the variable. + * @returns the expression that is assigned to the variable. + */ + std::shared_ptr const& getExpression() const; + + /*! + * Retrieves a string representation of this assignment. + * @returns a string representation of this assignment. + */ + std::string toString() const; + +private: + // The name of the variable that this assignment targets. + std::string variableName; + + // The expression that is assigned to the variable. + std::shared_ptr expression; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_ASSIGNMENT_H_ */ diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp new file mode 100644 index 000000000..2c03e1c44 --- /dev/null +++ b/src/ir/BooleanVariable.cpp @@ -0,0 +1,45 @@ +/* + * BooleanVariable.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "BooleanVariable.h" + +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +BooleanVariable::BooleanVariable() : Variable() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName, + std::shared_ptr initialValue) + : Variable(index, variableName, initialValue) { + // Nothing to do here. +} + +BooleanVariable::BooleanVariable(const BooleanVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints) + : Variable(var, newName, bools.at(newName), renaming, bools, ints) { +} + +// Build a string representation of the variable. +std::string BooleanVariable::toString() const { + std::stringstream result; + result << this->getName() << ": bool"; + if (this->getInitialValue() != nullptr) { + result << " init " << this->getInitialValue()->toString(); + } + result << ";"; + return result.str(); +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h new file mode 100644 index 000000000..bf70f01d1 --- /dev/null +++ b/src/ir/BooleanVariable.h @@ -0,0 +1,51 @@ +/* + * BooleanVariable.h + * + * Created on: 08.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_BOOLEANVARIABLE_H_ +#define STORM_IR_BOOLEANVARIABLE_H_ + +#include "src/ir/Variable.h" +#include +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing a boolean variable. + */ +class BooleanVariable : public Variable { +public: + /*! + * Default constructor. Creates a boolean variable without a name. + */ + BooleanVariable(); + + /*! + * Creates a boolean variable with the given name and the given initial value. + * @param index a unique (among the variables of equal type) index for the variable. + * @param variableName the name of the variable. + * @param initialValue the expression that defines the initial value of the variable. + */ + BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue = std::shared_ptr(nullptr)); + + + BooleanVariable(const BooleanVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints); + + /*! + * Retrieves a string representation of this variable. + * @returns a string representation of this variable. + */ + std::string toString() const; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_BOOLEANVARIABLE_H_ */ diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp new file mode 100644 index 000000000..05fe1084c --- /dev/null +++ b/src/ir/Command.cpp @@ -0,0 +1,75 @@ +/* + * Command.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "Command.h" + +#include +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +Command::Command() : actionName(), guardExpression(), updates() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +Command::Command(std::string actionName, std::shared_ptr guardExpression, std::vector updates) + : actionName(actionName), guardExpression(guardExpression), updates(updates) { + // Nothing to do here. +} + +Command::Command(const Command& cmd, const std::map& renaming, const std::map& bools, const std::map& ints) + : actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) { + if (renaming.count(this->actionName) > 0) { + this->actionName = renaming.at(this->actionName); + } + this->updates.reserve(cmd.updates.size()); + for (Update u : cmd.updates) { + this->updates.emplace_back(u, renaming, bools, ints); + } +} + +// Return the action name. +std::string const& Command::getActionName() const { + return this->actionName; +} + +// Return the expression for the guard. +std::shared_ptr const& Command::getGuard() const { + return guardExpression; +} + +// Return the number of updates. +uint_fast64_t Command::getNumberOfUpdates() const { + return this->updates.size(); +} + +// Return the requested update. +storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const { + return this->updates[index]; +} + +// Build a string representation of the command. +std::string Command::toString() const { + std::stringstream result; + result << "[" << actionName << "] " << guardExpression->toString() << " -> "; + for (uint_fast64_t i = 0; i < updates.size(); ++i) { + result << updates[i].toString(); + if (i < updates.size() - 1) { + result << " + "; + } + } + result << ";"; + return result.str(); +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/Command.h b/src/ir/Command.h new file mode 100644 index 000000000..b4049307c --- /dev/null +++ b/src/ir/Command.h @@ -0,0 +1,85 @@ +/* + * Command.h + * + * Created on: 06.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_COMMAND_H_ +#define STORM_IR_COMMAND_H_ + +#include "expressions/BaseExpression.h" +#include "Update.h" + +#include +#include +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing a command. + */ +class Command { +public: + /*! + * Default constructor. Creates a a command without name, guard and updates. + */ + Command(); + + /*! + * Creates a command with the given name, guard and updates. + * @param actionName the action name of the command. + * @param guardExpression the expression that defines the guard of the command. + */ + Command(std::string actionName, std::shared_ptr guardExpression, std::vector updates); + + Command(const Command& cmd, const std::map& renaming, const std::map& bools, const std::map& ints); + /*! + * Retrieves the action name of this command. + * @returns the action name of this command. + */ + std::string const& getActionName() const; + + /*! + * Retrieves a reference to the guard of the command. + * @returns a reference to the guard of the command. + */ + std::shared_ptr const& getGuard() const; + + /*! + * Retrieves the number of updates associated with this command. + * @returns the number of updates associated with this command. + */ + uint_fast64_t getNumberOfUpdates() const; + + /*! + * Retrieves a reference to the update with the given index. + * @returns a reference to the update with the given index. + */ + storm::ir::Update const& getUpdate(uint_fast64_t index) const; + + /*! + * Retrieves a string representation of this command. + * @returns a string representation of this command. + */ + std::string toString() const; + +private: + // The name of the command. + std::string actionName; + + // The expression that defines the guard of the command. + std::shared_ptr guardExpression; + + // The list of updates of the command. + std::vector updates; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_COMMAND_H_ */ diff --git a/src/ir/IR.h b/src/ir/IR.h new file mode 100644 index 000000000..80a794002 --- /dev/null +++ b/src/ir/IR.h @@ -0,0 +1,25 @@ +/* + * IR.h + * + * Created on: 06.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_IR_H_ +#define STORM_IR_IR_H_ + +// Bundle all headers to make it easy to include them. +#include "expressions/Expressions.h" +#include "Assignment.h" +#include "Update.h" +#include "Command.h" +#include "Variable.h" +#include "BooleanVariable.h" +#include "IntegerVariable.h" +#include "Module.h" +#include "StateReward.h" +#include "TransitionReward.h" +#include "RewardModel.h" +#include "Program.h" + +#endif /* STORM_IR_IR_H_ */ diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp new file mode 100644 index 000000000..a8926b046 --- /dev/null +++ b/src/ir/IntegerVariable.cpp @@ -0,0 +1,60 @@ +/* + * IntegerVariable.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "IntegerVariable.h" + +#include + +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +IntegerVariable::IntegerVariable() : lowerBound(), upperBound() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue) + : Variable(index, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) { + // TODO: This behaves like prism... + if (this->getInitialValue() == nullptr) { + this->setInitialValue(lowerBound); + } +} + +IntegerVariable::IntegerVariable(const IntegerVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints) + : Variable(var, newName, ints.at(newName), renaming, bools, ints), lowerBound(var.lowerBound->clone(renaming, bools, ints)), upperBound(var.upperBound->clone(renaming, bools, ints)) { +} + +// Return lower bound for variable. +std::shared_ptr IntegerVariable::getLowerBound() const { + return this->lowerBound; +} + +// Return upper bound for variable. +std::shared_ptr IntegerVariable::getUpperBound() const { + return this->upperBound; +} + + +// Build a string representation of the variable. +std::string IntegerVariable::toString() const { + std::stringstream result; + result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]"; + if (this->getInitialValue() != nullptr) { + result << " init " + this->getInitialValue()->toString(); + } + result << ";"; + return result.str(); +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h new file mode 100644 index 000000000..8233cbe09 --- /dev/null +++ b/src/ir/IntegerVariable.h @@ -0,0 +1,72 @@ +/* + * IntegerVariable.h + * + * Created on: 08.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_INTEGERVARIABLE_H_ +#define STORM_IR_INTEGERVARIABLE_H_ + +#include "expressions/BaseExpression.h" +#include "src/ir/Variable.h" +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing an integer variable. + */ +class IntegerVariable : public Variable { +public: + /*! + * Default constructor. Creates an integer variable without a name and lower and upper bounds. + */ + IntegerVariable(); + + /*! + * Creates an integer variable with the given name, lower and upper bounds and the given initial + * value. + * @param index A unique (among the variables of equal type) index for the variable. + * @param variableName the name of the variable. + * @param lowerBound the lower bound of the domain of the variable. + * @param upperBound the upper bound of the domain of the variable. + * @param initialValue the expression that defines the initial value of the variable. + */ + IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = std::shared_ptr(nullptr)); + + IntegerVariable(const IntegerVariable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints); + + /*! + * Retrieves the lower bound for this integer variable. + * @returns the lower bound for this integer variable. + */ + std::shared_ptr getLowerBound() const; + + /*! + * Retrieves the upper bound for this integer variable. + * @returns the upper bound for this integer variable. + */ + std::shared_ptr getUpperBound() const; + + /*! + * Retrieves a string representation of this variable. + * @returns a string representation of this variable. + */ + std::string toString() const; + +private: + // The lower bound of the domain of the variable. + std::shared_ptr lowerBound; + + // The upper bound of the domain of the variable. + std::shared_ptr upperBound; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_INTEGERVARIABLE_H_ */ diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp new file mode 100644 index 000000000..624f1876c --- /dev/null +++ b/src/ir/Module.cpp @@ -0,0 +1,182 @@ +/* + * Module.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "Module.h" + +#include "src/exceptions/InvalidArgumentException.h" + +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariablesToIndexMap(), + integerVariablesToIndexMap(), commands(), actions(), actionsToCommandIndexMap() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +Module::Module(std::string moduleName, + std::vector booleanVariables, + std::vector integerVariables, + std::map booleanVariableToIndexMap, + std::map integerVariableToIndexMap, + std::vector commands) + : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), + booleanVariablesToIndexMap(booleanVariableToIndexMap), + integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands), actions(), actionsToCommandIndexMap() { + this->collectActions(); +} + +Module::Module(const Module& module, const std::string& moduleName, const std::map& renaming, std::shared_ptr adder) + : moduleName(moduleName) { + LOG4CPLUS_TRACE(logger, "Start renaming " << module.moduleName << " to " << moduleName); + + // First step: Create new Variables via the adder. + adder->performRenaming(renaming); + + // Second step: Get all indices of variables that are produced by the renaming. + for (auto it: renaming) { + std::shared_ptr var = adder->getVariable(it.second); + if (var != nullptr) { + if (var->getType() == expressions::BaseExpression::bool_) { + this->booleanVariablesToIndexMap[it.second] = var->getVariableIndex(); + } else if (var->getType() == expressions::BaseExpression::int_) { + this->integerVariablesToIndexMap[it.second] = var->getVariableIndex(); + } + } + } + + // Third step: Create new Variable objects. + this->booleanVariables.reserve(module.booleanVariables.size()); + for (BooleanVariable it: module.booleanVariables) { + if (renaming.count(it.getName()) > 0) { + this->booleanVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); + } else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); + } + this->integerVariables.reserve(module.integerVariables.size()); + for (IntegerVariable it: module.integerVariables) { + if (renaming.count(it.getName()) > 0) { + this->integerVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); + } else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); + } + + // Fourth step: Clone commands. + this->commands.reserve(module.commands.size()); + for (Command cmd: module.commands) { + this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); + } + this->collectActions(); + + LOG4CPLUS_TRACE(logger, "Finished renaming..."); +} + +// Return the number of boolean variables. +uint_fast64_t Module::getNumberOfBooleanVariables() const { + return this->booleanVariables.size(); +} + +// Return the requested boolean variable. +storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const { + return this->booleanVariables[index]; +} + +// Return the number of integer variables. +uint_fast64_t Module::getNumberOfIntegerVariables() const { + return this->integerVariables.size(); +} + +// Return the requested integer variable. +storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const { + return this->integerVariables[index]; +} + +// Return the number of commands. +uint_fast64_t Module::getNumberOfCommands() const { + return this->commands.size(); +} + +// Return the index of the variable if it exists and throw exception otherwise. +uint_fast64_t Module::getBooleanVariableIndex(std::string variableName) const { + auto it = booleanVariablesToIndexMap.find(variableName); + if (it != booleanVariablesToIndexMap.end()) { + return it->second; + } + throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown " + << "boolean variable " << variableName << "."; +} + +// Return the index of the variable if it exists and throw exception otherwise. +uint_fast64_t Module::getIntegerVariableIndex(std::string variableName) const { + auto it = integerVariablesToIndexMap.find(variableName); + if (it != integerVariablesToIndexMap.end()) { + return it->second; + } + throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown " + << "variable " << variableName << "."; +} + +// Return the requested command. +storm::ir::Command const Module::getCommand(uint_fast64_t index) const { + return this->commands[index]; +} + +// Build a string representation of the variable. +std::string Module::toString() const { + std::stringstream result; + result << "module " << moduleName << std::endl; + for (auto variable : booleanVariables) { + result << "\t" << variable.toString() << std::endl; + } + for (auto variable : integerVariables) { + result << "\t" << variable.toString() << std::endl; + } + for (auto command : commands) { + result << "\t" << command.toString() << std::endl; + } + result << "endmodule" << std::endl; + return result.str(); +} + +// Return set of actions. +std::set const& Module::getActions() const { + return this->actions; +} + +// Return commands with given action. +std::shared_ptr> const Module::getCommandsByAction(std::string const& action) const { + auto res = this->actionsToCommandIndexMap.find(action); + if (res == this->actionsToCommandIndexMap.end()) { + return std::shared_ptr>(new std::set()); + } else { + return res->second; + } +} + +void Module::collectActions() { + for (unsigned int id = 0; id < this->commands.size(); id++) { + std::string action = this->commands[id].getActionName(); + if (action != "") { + if (this->actionsToCommandIndexMap.count(action) == 0) { + this->actionsToCommandIndexMap[action] = std::shared_ptr>(new std::set()); + } + this->actionsToCommandIndexMap[action]->insert(id); + this->actions.insert(action); + } + } +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/Module.h b/src/ir/Module.h new file mode 100644 index 000000000..e4343e357 --- /dev/null +++ b/src/ir/Module.h @@ -0,0 +1,171 @@ +/* + * Module.h + * + * Created on: 04.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_MODULE_H_ +#define STORM_IR_MODULE_H_ + +#include "BooleanVariable.h" +#include "IntegerVariable.h" +#include "expressions/VariableExpression.h" +#include "Command.h" + +#include +#include +#include +#include +#include + +namespace storm { + +namespace ir { + + struct VariableAdder { + virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper) = 0; + virtual uint_fast64_t addBooleanVariable(const std::string& name) = 0; + virtual std::shared_ptr getVariable(const std::string& name) = 0; + virtual void performRenaming(const std::map& renaming) = 0; + }; + +/*! + * A class representing a module. + */ +class Module { +public: + /*! + * Default constructor. Creates an empty module. + */ + Module(); + + /*! + * Creates a module with the given name, variables and commands. + * @param moduleName the name of the module. + * @param booleanVariables a map of boolean variables. + * @param integerVariables a map of integer variables. + * @param commands the vector of commands. + */ + Module(std::string moduleName, std::vector booleanVariables, + std::vector integerVariables, + std::map booleanVariableToIndexMap, + std::map integerVariableToIndexMap, + std::vector commands); + + typedef uint_fast64_t (*addIntegerVariablePtr)(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init); + typedef uint_fast64_t (*addBooleanVariablePtr)(const std::string& name, const std::shared_ptr init); + + /*! + * Special copy constructor, implementing the module renaming functionality. + * This will create a new module having all identifier renamed according to the given map. + * @param module Module to be copied. + * @param moduleName Name of the new module. + * @param renaming Renaming map. + */ + Module(const Module& module, const std::string& moduleName, const std::map& renaming, std::shared_ptr adder); + + /*! + * Retrieves the number of boolean variables in the module. + * @returns the number of boolean variables in the module. + */ + uint_fast64_t getNumberOfBooleanVariables() const; + + /*! + * Retrieves a reference to the boolean variable with the given index. + * @returns a reference to the boolean variable with the given index. + */ + storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const; + + /*! + * Retrieves the number of integer variables in the module. + * @returns the number of integer variables in the module. + */ + uint_fast64_t getNumberOfIntegerVariables() const; + + /*! + * Retrieves a reference to the integer variable with the given index. + * @returns a reference to the integer variable with the given index. + */ + storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const; + + /*! + * Retrieves the number of commands of this module. + * @returns the number of commands of this module. + */ + uint_fast64_t getNumberOfCommands() const; + + /*! + * Retrieves the index of the boolean variable with the given name. + * @param variableName the name of the variable whose index to retrieve. + * @returns the index of the boolean variable with the given name. + */ + uint_fast64_t getBooleanVariableIndex(std::string variableName) const; + + /*! + * Retrieves the index of the integer variable with the given name. + * @param variableName the name of the variable whose index to retrieve. + * @returns the index of the integer variable with the given name. + */ + uint_fast64_t getIntegerVariableIndex(std::string variableName) const; + + /*! + * Retrieves a reference to the command with the given index. + * @returns a reference to the command with the given index. + */ + storm::ir::Command const getCommand(uint_fast64_t index) const; + + /*! + * Retrieves a string representation of this variable. + * @returns a string representation of this variable. + */ + std::string toString() const; + + /*! + * Retrieves the set of actions present in this module. + * @returns the set of actions present in this module. + */ + std::set const& getActions() const; + + /*! + * Retrieves the indices of all commands within this module that are labelled + * by the given action. + * @param action Name of the action. + * @returns Indices of all matching commands. + */ + std::shared_ptr> const getCommandsByAction(std::string const& action) const; + +private: + + void collectActions(); + + // The name of the module. + std::string moduleName; + + // A list of boolean variables. + std::vector booleanVariables; + + // A list of integer variables. + std::vector integerVariables; + + // A map of boolean variable names to their index. + std::map booleanVariablesToIndexMap; + + // A map of integer variable names to their index. + std::map integerVariablesToIndexMap; + + // The commands associated with the module. + std::vector commands; + + // The set of actions present in this module. + std::set actions; + + // A map of actions to the set of commands labeled with this action. + std::map>> actionsToCommandIndexMap; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_MODULE_H_ */ diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp new file mode 100644 index 000000000..96ad94b2b --- /dev/null +++ b/src/ir/Program.cpp @@ -0,0 +1,145 @@ +/* + * Program.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "Program.h" +#include "exceptions/InvalidArgumentException.h" + +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +Program::Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards, std::map> labels) + : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap() { + // Build actionsToModuleIndexMap + for (unsigned int id = 0; id < this->modules.size(); id++) { + for (auto action : this->modules[id].getActions()) { + if (this->actionsToModuleIndexMap.count(action) == 0) { + this->actionsToModuleIndexMap[action] = std::set(); + } + this->actionsToModuleIndexMap[action].insert(id); + this->actions.insert(action); + } + } +} + +Program::ModelType Program::getModelType() const { + return modelType; +} + +// Build a string representation of the program. +std::string Program::toString() const { + std::stringstream result; + switch (modelType) { + case UNDEFINED: result << "undefined"; break; + case DTMC: result << "dtmc"; break; + case CTMC: result << "ctmc"; break; + case MDP: result << "mdp"; break; + case CTMDP: result << "ctmdp"; break; + } + result << std::endl; + + for (auto element : booleanUndefinedConstantExpressions) { + result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + } + for (auto element : integerUndefinedConstantExpressions) { + result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + } + for (auto element : doubleUndefinedConstantExpressions) { + result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; + } + result << std::endl; + + for (auto module : modules) { + result << module.toString() << std::endl; + } + + for (auto rewardModel : rewards) { + result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl; + } + + for (auto label : labels) { + result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl; + } + + return result.str(); +} + +uint_fast64_t Program::getNumberOfModules() const { + return this->modules.size(); +} + +storm::ir::Module const& Program::getModule(uint_fast64_t index) const { + return this->modules[index]; +} + +// Return set of actions. +std::set const& Program::getActions() const { + return this->actions; +} + +// Return modules with given action. +std::set const Program::getModulesByAction(std::string const& action) const { + auto res = this->actionsToModuleIndexMap.find(action); + if (res == this->actionsToModuleIndexMap.end()) { + return std::set(); + } else { + return res->second; + } +} + +storm::ir::RewardModel Program::getRewardModel(std::string const & name) const { + auto it = this->rewards.find(name); + if (it == this->rewards.end()) { + LOG4CPLUS_ERROR(logger, "The given reward model \"" << name << "\" does not exist. We will proceed without rewards."); + throw "Rewardmodel does not exist."; + } else { + return it->second; + } +} + +std::map> Program::getLabels() const { + return this->labels; +} + +std::string Program::getVariableString() const { + std::map bools; + std::map ints; + unsigned maxInt = 0, maxBool = 0; + for (Module module: this->modules) { + for (unsigned int i = 0; i < module.getNumberOfBooleanVariables(); i++) { + storm::ir::BooleanVariable var = module.getBooleanVariable(i); + bools[var.getIndex()] = var.getName(); + if (var.getIndex() >= maxBool) maxBool = var.getIndex()+1; + } + for (unsigned int i = 0; i < module.getNumberOfIntegerVariables(); i++) { + storm::ir::IntegerVariable var = module.getIntegerVariable(i); + ints[var.getIndex()] = var.getName(); + if (var.getIndex() >= maxInt) maxInt = var.getIndex()+1; + } + } + std::stringstream ss; + for (unsigned int i = 0; i < maxBool; i++) ss << bools[i] << "\t"; + for (unsigned int i = 0; i < maxInt; i++) ss << ints[i] << "\t"; + return ss.str(); +} + +} // namespace ir + +} // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h new file mode 100644 index 000000000..c12b6dddd --- /dev/null +++ b/src/ir/Program.h @@ -0,0 +1,151 @@ +/* + * Program.h + * + * Created on: 04.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_PROGRAM_H_ +#define STORM_IR_PROGRAM_H_ + +#include "expressions/BaseExpression.h" +#include "expressions/BooleanConstantExpression.h" +#include "expressions/IntegerConstantExpression.h" +#include "expressions/DoubleConstantExpression.h" +#include "Module.h" +#include "RewardModel.h" + +#include +#include +#include +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing a program. + */ +class Program { +public: + + /*! + * An enum for the different model types. + */ + enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP}; + + /*! + * Default constructor. Creates an empty program. + */ + Program(); + + /*! + * Creates a program with the given model type, undefined constants, modules, rewards and labels. + * @param modelType the type of the model that this program gives rise to. + * @param booleanUndefinedConstantExpressions a map of undefined boolean constants to their + * expression nodes. + * @param integerUndefinedConstantExpressions a map of undefined integer constants to their + * expression nodes. + * @param doubleUndefinedConstantExpressions a map of undefined double constants to their + * expression nodes. + * @param modules The modules of the program. + * @param rewards The reward models of the program. + * @param labels The labels defined for this model. + */ + Program( + ModelType modelType, + std::map> booleanUndefinedConstantExpressions, + std::map> integerUndefinedConstantExpressions, + std::map> doubleUndefinedConstantExpressions, + std::vector modules, + std::map rewards, + std::map> labels); + + /*! + * Retrieves the number of modules in the program. + * @returns the number of modules in the program. + */ + uint_fast64_t getNumberOfModules() const; + + /*! + * Retrieves a reference to the module with the given index. + * @param index the index of the module to retrieve. + */ + storm::ir::Module const& getModule(uint_fast64_t index) const; + + /*! + * Retrieves the model type of the model. + * @returns the type of the model. + */ + ModelType getModelType() const; + + /*! + * Retrieves a string representation of this program. + * @returns a string representation of this program. + */ + std::string toString() const; + + /*! + * Retrieves the set of actions present in this module. + * @returns the set of actions present in this module. + */ + std::set const& getActions() const; + + /*! + * Retrieved the indices of all Modules within this program that contain + * commands that are labelled with the given action. + * @param action Name of the action. + * @returns Indices of all matching modules. + */ + std::set const getModulesByAction(std::string const& action) const; + + /*! + * Retrieve reward model with given name. + * @param name Name of the reward model. + * @return Reward model with given name. + */ + storm::ir::RewardModel getRewardModel(std::string const & name) const; + + /*! + * Retrieves all labels. + * @return All labels. + */ + std::map> getLabels() const; + + std::string getVariableString() const; + +private: + // The type of the model. + ModelType modelType; + + // A map of undefined boolean constants to their expression nodes. + std::map> booleanUndefinedConstantExpressions; + + // A map of undefined integer constants to their expressions nodes. + std::map> integerUndefinedConstantExpressions; + + // A map of undefined double constants to their expressions nodes. + std::map> doubleUndefinedConstantExpressions; + + // The modules associated with the program. + std::vector modules; + + // The reward models associated with the program. + std::map rewards; + + // The labels that are defined for this model. + std::map> labels; + + // The set of actions present in this program. + std::set actions; + + // A map of actions to the set of modules containing commands labelled with this action. + std::map> actionsToModuleIndexMap; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_PROGRAM_H_ */ diff --git a/src/ir/RewardModel.cpp b/src/ir/RewardModel.cpp new file mode 100644 index 000000000..d6611e4ec --- /dev/null +++ b/src/ir/RewardModel.cpp @@ -0,0 +1,58 @@ +/* + * RewardModel.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "RewardModel.h" + +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +RewardModel::RewardModel(std::string rewardModelName, std::vector stateRewards, std::vector transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { + // Nothing to do here. +} + +// Build a string representation of the reward model. +std::string RewardModel::toString() const { + std::stringstream result; + result << "rewards \"" << rewardModelName << "\"" << std::endl; + for (auto reward : stateRewards) { + result << reward.toString() << std::endl; + } + for (auto reward : transitionRewards) { + result << reward.toString() << std::endl; + } + result << "endrewards" << std::endl; + return result.str(); +} + +bool RewardModel::hasStateRewards() const { + return this->stateRewards.size() > 0; +} + +std::vector RewardModel::getStateRewards() const { + return this->stateRewards; +} + +bool RewardModel::hasTransitionRewards() const { + return this->transitionRewards.size() > 0; +} + +std::vector RewardModel::getTransitionRewards() const { + return this->transitionRewards; +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/RewardModel.h b/src/ir/RewardModel.h new file mode 100644 index 000000000..cb538f173 --- /dev/null +++ b/src/ir/RewardModel.h @@ -0,0 +1,84 @@ +/* + * RewardModel.h + * + * Created on: 04.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_REWARDMODEL_H_ +#define STORM_IR_REWARDMODEL_H_ + +#include "StateReward.h" +#include "TransitionReward.h" + +#include +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing a reward model. + */ +class RewardModel { +public: + /*! + * Default constructor. Creates an empty reward model. + */ + RewardModel(); + + /*! + * Creates a reward module with the given name, state and transition rewards. + * @param rewardModelName the name of the reward model. + * @param stateRewards A vector of state-based reward. + * @param transitionRewards A vector of transition-based reward. + */ + RewardModel(std::string rewardModelName, std::vector stateRewards, std::vector transitionRewards); + + /*! + * Retrieves a string representation of this variable. + * @returns a string representation of this variable. + */ + std::string toString() const; + + /*! + * Check, if there are any state rewards. + * @return True, iff there are any state rewards. + */ + bool hasStateRewards() const; + + /*! + * Retrieve state rewards. + * @return State rewards. + */ + std::vector getStateRewards() const; + + /*! + * Check, if there are any transition rewards. + * @return True, iff there are any transition rewards. + */ + bool hasTransitionRewards() const; + + /*! + * Retrieve transition rewards. + * @return Transition rewards. + */ + std::vector getTransitionRewards() const; + +private: + // The name of the reward model. + std::string rewardModelName; + + // The state-based rewards associated with this reward model. + std::vector stateRewards; + + // The transition-based rewards associated with this reward model. + std::vector transitionRewards; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_REWARDMODEL_H_ */ diff --git a/src/ir/StateReward.cpp b/src/ir/StateReward.cpp new file mode 100644 index 000000000..93bf738db --- /dev/null +++ b/src/ir/StateReward.cpp @@ -0,0 +1,42 @@ +/* + * StateReward.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "StateReward.h" + +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +StateReward::StateReward() : statePredicate(), rewardValue() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +StateReward::StateReward(std::shared_ptr statePredicate, std::shared_ptr rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { + // Nothing to do here. +} + +// Build a string representation of the state reward. +std::string StateReward::toString() const { + std::stringstream result; + result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";"; + return result.str(); +} + +double StateReward::getReward(std::pair, std::vector> const * state) const { + if (this->statePredicate->getValueAsBool(state)) { + return this->rewardValue->getValueAsDouble(state); + } + return 0; +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/StateReward.h b/src/ir/StateReward.h new file mode 100644 index 000000000..638b42ed7 --- /dev/null +++ b/src/ir/StateReward.h @@ -0,0 +1,65 @@ +/* + * StateReward.h + * + * Created on: Jan 10, 2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_STATEREWARD_H_ +#define STORM_IR_STATEREWARD_H_ + +#include "expressions/BaseExpression.h" + +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing a state reward. + */ +class StateReward { +public: + /*! + * Default constructor. Creates an empty state reward. + */ + StateReward(); + + /*! + * Creates a state reward for the states satisfying the given expression with the value given + * by a second expression. + * @param statePredicate the predicate that states earning this state-based reward need to + * satisfy. + * @param rewardValue an expression specifying the values of the rewards to attach to the + * states. + */ + StateReward(std::shared_ptr statePredicate, std::shared_ptr rewardValue); + + /*! + * Retrieves a string representation of this state reward. + * @returns a string representation of this state reward. + */ + std::string toString() const; + + /*! + * Returns the reward for the given state. + * It the state fulfills the predicate, the reward value is returned, zero otherwise. + * @param state State object. + * @return Reward for given state. + */ + double getReward(std::pair, std::vector> const * state) const; + +private: + // The predicate that characterizes the states that obtain this reward. + std::shared_ptr statePredicate; + + // The expression that specifies the value of the reward obtained. + std::shared_ptr rewardValue; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_STATEREWARD_H_ */ diff --git a/src/ir/TransitionReward.cpp b/src/ir/TransitionReward.cpp new file mode 100644 index 000000000..680df77e6 --- /dev/null +++ b/src/ir/TransitionReward.cpp @@ -0,0 +1,43 @@ +/* + * TransitionReward.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "TransitionReward.h" + +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +TransitionReward::TransitionReward(std::string commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { + // Nothing to do here. +} + +// Build a string representation of the transition reward. +std::string TransitionReward::toString() const { + std::stringstream result; + result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";"; + return result.str(); +} + +double TransitionReward::getReward(std::string const & label, std::pair, std::vector> const * state) const { + if (this->commandName != label) return 0; + if (this->statePredicate->getValueAsBool(state)) { + return this->rewardValue->getValueAsDouble(state); + } + return 0; +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h new file mode 100644 index 000000000..89480109a --- /dev/null +++ b/src/ir/TransitionReward.h @@ -0,0 +1,68 @@ +/* + * TransitionReward.h + * + * Created on: Jan 10, 2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_TRANSITIONREWARD_H_ +#define STORM_IR_TRANSITIONREWARD_H_ + +#include "expressions/BaseExpression.h" + +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing a transition reward. + */ +class TransitionReward { +public: + /*! + * Default constructor. Creates an empty transition reward. + */ + TransitionReward(); + + /*! + * Creates a transition reward for the transitions with the given name emanating from states + * satisfying the given expression with the value given by another expression. + * @param commandName the name of the command that obtains this reward. + * @param statePredicate the predicate that needs to hold before taking a transition with the + * previously specified name in order to obtain the reward. + * @param rewardValue an expression specifying the values of the rewards to attach to the + * transitions. + */ + TransitionReward(std::string commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue); + + /*! + * Retrieves a string representation of this transition reward. + * @returns a string representation of this transition reward. + */ + std::string toString() const; + + /*! + * Retrieves reward for given transition. + * Returns reward value if source state fulfills predicate and the transition is labeled correctly, zero otherwise. + */ + double getReward(std::string const & label, std::pair, std::vector> const * state) const; + +private: + // The name of the command this transition-based reward is attached to. + std::string commandName; + + // A predicate that needs to be satisfied by states for the reward to be obtained (by taking + // a corresponding command transition). + std::shared_ptr statePredicate; + + // The expression specifying the value of the reward obtained along the transitions. + std::shared_ptr rewardValue; +}; + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_TRANSITIONREWARD_H_ */ diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp new file mode 100644 index 000000000..2d0dc5d2a --- /dev/null +++ b/src/ir/Update.cpp @@ -0,0 +1,118 @@ +/* + * Update.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "Update.h" + +#include "src/exceptions/OutOfRangeException.h" + +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +Update::Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments) + : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) { + // Nothing to do here. +} + +Update::Update(const Update& update, const std::map& renaming, const std::map& bools, const std::map& ints) { + for (auto it : update.booleanAssignments) { + if (renaming.count(it.first) > 0) { + this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints); + } else { + this->booleanAssignments[it.first] = Assignment(it.second, renaming, bools, ints); + } + } + for (auto it : update.integerAssignments) { + if (renaming.count(it.first) > 0) { + this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints); + } else { + this->integerAssignments[it.first] = Assignment(it.second, renaming, bools, ints); + } + } + this->likelihoodExpression = update.likelihoodExpression->clone(renaming, bools, ints); +} + +// Return the expression for the likelihood of the update. +std::shared_ptr const& Update::getLikelihoodExpression() const { + return likelihoodExpression; +} + +// Return the number of assignments. +uint_fast64_t Update::getNumberOfBooleanAssignments() const { + return booleanAssignments.size(); +} + +uint_fast64_t Update::getNumberOfIntegerAssignments() const { + return integerAssignments.size(); +} + +// Return the boolean variable name to assignment map. +std::map const& Update::getBooleanAssignments() const { + return booleanAssignments; +} + +// Return the integer variable name to assignment map. +std::map const& Update::getIntegerAssignments() const { + return integerAssignments; +} + +// Return the assignment for the boolean variable if it exists and throw an exception otherwise. +storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableName) const { + auto it = booleanAssignments.find(variableName); + if (it == booleanAssignments.end()) { + throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '" + << variableName << "' in update " << this->toString() << "."; + } + + return (*it).second; +} + +// Return the assignment for the boolean variable if it exists and throw an exception otherwise. +storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableName) const { + auto it = integerAssignments.find(variableName); + if (it == integerAssignments.end()) { + throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '" + << variableName << "' in update " << this->toString() << "."; + } + + return (*it).second; +} + +// Build a string representation of the update. +std::string Update::toString() const { + std::stringstream result; + result << likelihoodExpression->toString() << " : "; + uint_fast64_t i = 0; + for (auto assignment : booleanAssignments) { + result << assignment.second.toString(); + if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { + result << " & "; + } + ++i; + } + i = 0; + for (auto assignment : integerAssignments) { + result << assignment.second.toString(); + if (i < integerAssignments.size() - 1) { + result << " & "; + } + ++i; + } + return result.str(); +} + +} // namespace ir + +} // namespace storm diff --git a/src/ir/Update.h b/src/ir/Update.h new file mode 100644 index 000000000..4ce6a2fbf --- /dev/null +++ b/src/ir/Update.h @@ -0,0 +1,104 @@ +/* + * Update.h + * + * Created on: 06.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_UPDATE_H_ +#define STORM_IR_UPDATE_H_ + +#include "expressions/BaseExpression.h" +#include "Assignment.h" + +#include +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing an update of a command. + */ +class Update { +public: + /*! + * Default constructor. Creates an empty update. + */ + Update(); + + /*! + * Creates an update with the given expression specifying the likelihood and the mapping of + * variable to their assignments. + * @param likelihoodExpression an expression specifying the likelihood of this update. + * @param assignments a map of variable names to their assignments. + */ + Update(std::shared_ptr likelihoodExpression, std::map booleanAssignments, std::map integerAssignments); + + Update(const Update& update, const std::map& renaming, const std::map& bools, const std::map& ints); + + /*! + * Retrieves the expression for the likelihood of this update. + * @returns the expression for the likelihood of this update. + */ + std::shared_ptr const& getLikelihoodExpression() const; + + /*! + * Retrieves the number of boolean assignments associated with this update. + * @returns the number of boolean assignments associated with this update. + */ + uint_fast64_t getNumberOfBooleanAssignments() const; + + /*! + * Retrieves the number of integer assignments associated with this update. + * @returns the number of integer assignments associated with this update. + */ + uint_fast64_t getNumberOfIntegerAssignments() const; + + /*! + * Retrieves a reference to the map of boolean variable names to their respective assignments. + * @returns a reference to the map of boolean variable names to their respective assignments. + */ + std::map const& getBooleanAssignments() const; + + /*! + * Retrieves a reference to the map of integer variable names to their respective assignments. + * @returns a reference to the map of integer variable names to their respective assignments. + */ + std::map const& getIntegerAssignments() const; + + /*! + * Retrieves a reference to the assignment for the boolean variable with the given name. + * @returns a reference to the assignment for the boolean variable with the given name. + */ + storm::ir::Assignment const& getBooleanAssignment(std::string variableName) const; + + /*! + * Retrieves a reference to the assignment for the integer variable with the given name. + * @returns a reference to the assignment for the integer variable with the given name. + */ + storm::ir::Assignment const& getIntegerAssignment(std::string variableName) const; + + /*! + * Retrieves a string representation of this update. + * @returns a string representation of this update. + */ + std::string toString() const; + +private: + // An expression specifying the likelihood of taking this update. + std::shared_ptr likelihoodExpression; + + // A mapping of boolean variable names to their assignments in this update. + std::map booleanAssignments; + + // A mapping of integer variable names to their assignments in this update. + std::map integerAssignments; +}; + +} // namespace ir + +} // namespace storm + +#endif /*STORM_IR_UPDATE_H_ */ diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp new file mode 100644 index 000000000..421603f4f --- /dev/null +++ b/src/ir/Variable.cpp @@ -0,0 +1,58 @@ +/* + * Variable.cpp + * + * Created on: 12.01.2013 + * Author: Christian Dehnert + */ + +#include "Variable.h" + +#include +#include +#include + +namespace storm { + +namespace ir { + +// Initializes all members with their default constructors. +Variable::Variable() : index(0), variableName(), initialValue() { + // Nothing to do here. +} + +// Initializes all members according to the given values. +Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue) : index(index), variableName(variableName), initialValue(initialValue) { + // Nothing to do here. +} + +Variable::Variable(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, const std::map& renaming, const std::map& bools, const std::map& ints) { + this->index = newIndex; + this->variableName = newName; + if (var.initialValue != nullptr) { + this->initialValue = var.initialValue->clone(renaming, bools, ints); + } +} + +// Return the name of the variable. +std::string const& Variable::getName() const { + return variableName; +} + +uint_fast64_t Variable::getIndex() const { + return index; +} + +// Return the expression for the initial value of the variable. +std::shared_ptr const& Variable::getInitialValue() const { + return initialValue; +} + +// Set the initial value expression to the one provided. +void Variable::setInitialValue(std::shared_ptr const& initialValue) { + this->initialValue = initialValue; +} + + +} // namespace ir + +} // namespace storm diff --git a/src/ir/Variable.h b/src/ir/Variable.h new file mode 100644 index 000000000..610ef903a --- /dev/null +++ b/src/ir/Variable.h @@ -0,0 +1,85 @@ +/* + * Variable.h + * + * Created on: 06.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_VARIABLE_H_ +#define STORM_IR_VARIABLE_H_ + +#include "expressions/BaseExpression.h" + +#include +#include + +namespace storm { + +namespace ir { + +/*! + * A class representing a untyped variable. + */ +class Variable { +public: + /*! + * Default constructor. Creates an unnamed, untyped variable without initial value. + */ + Variable(); + + /*! + * Creates an untyped variable with the given name and initial value. + * @param index A unique (among the variables of equal type) index for the variable. + * @param variableName the name of the variable. + * @param initialValue the expression that defines the initial value of the variable. + */ + Variable(uint_fast64_t index, std::string variableName, std::shared_ptr initialValue = std::shared_ptr()); + + /*! + * Creates a copy of the given Variable and gives it a new name. + * @param var Variable to copy. + * @param newName New name of this variable. + */ + Variable(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, const std::map& renaming, const std::map& bools, const std::map& ints); + + /*! + * Retrieves the name of the variable. + * @returns the name of the variable. + */ + std::string const& getName() const; + + /*! + * Retrieves the index of the variable. + * @returns the index of the variable. + */ + uint_fast64_t getIndex() const; + + /*! + * Retrieves the expression defining the initial value of the variable. + * @returns the expression defining the initial value of the variable. + */ + std::shared_ptr const& getInitialValue() const; + + /*! + * Sets the initial value to the given expression. + * @param initialValue the new initial value. + */ + void setInitialValue(std::shared_ptr const& initialValue); + +private: + // A unique (among the variables of equal type) index for the variable + uint_fast64_t index; + + // The name of the variable. + std::string variableName; + + // The expression defining the initial value of the variable. + std::shared_ptr initialValue; +}; + +} // namespace ir + +} // namespace storm + + +#endif /* STORM_IR_VARIABLE_H_ */ diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h new file mode 100644 index 000000000..98f8f2ee2 --- /dev/null +++ b/src/ir/expressions/BaseExpression.h @@ -0,0 +1,105 @@ +/* + * Expression.h + * + * Created on: 03.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ + +#include "src/exceptions/ExpressionEvaluationException.h" +#include "src/exceptions/NotImplementedException.h" + +#include "ExpressionVisitor.h" + +#include +#include +#include +#include + +namespace storm { +namespace ir { +namespace expressions { + +class BaseExpression { + +public: + enum ReturnType {undefined, bool_, int_, double_}; + + BaseExpression() : type(undefined) { + + } + + BaseExpression(ReturnType type) : type(type) { + + } + BaseExpression(const BaseExpression& be) + : type(be.type) { + } + + virtual ~BaseExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) = 0; + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { + if (type != int_) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" + << this->getTypeName() << "' as 'int'."; + } + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" + << this->getTypeName() << " because evaluation implementation is missing."; + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { + if (type != bool_) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" + << this->getTypeName() << "' as 'bool'."; + } + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" + << this->getTypeName() << " because evaluation implementation is missing."; + } + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { + if (type != bool_) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" + << this->getTypeName() << "' as 'double'."; + } + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" + << this->getTypeName() << " because evaluation implementation is missing."; + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const = 0; + + std::string getTypeName() const { + switch(type) { + case bool_: return std::string("bool"); + case int_: return std::string("int"); + case double_: return std::string("double"); + default: return std::string("undefined"); + } + } + + ReturnType getType() const { + return type; + } + + virtual std::string dump(std::string prefix) const = 0; + +private: + ReturnType type; +}; + +} // namespace expressions + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ */ diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h new file mode 100644 index 000000000..4882c0d92 --- /dev/null +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -0,0 +1,91 @@ +/* + * BinaryBooleanFunctionExpression.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ + +#include "src/ir/expressions/BinaryExpression.h" + +#include +#include + +namespace storm { + +namespace ir { + +namespace expressions { + +class BinaryBooleanFunctionExpression : public BinaryExpression { +public: + enum FunctionType {AND, OR}; + + BinaryBooleanFunctionExpression(std::shared_ptr left, std::shared_ptr right, FunctionType functionType) : BinaryExpression(bool_, left, right), functionType(functionType) { + + } + + virtual ~BinaryBooleanFunctionExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType)); + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { + bool resultLeft = this->getLeft()->getValueAsBool(variableValues); + bool resultRight = this->getRight()->getValueAsBool(variableValues); + switch(functionType) { + case AND: return resultLeft & resultRight; break; + case OR: return resultLeft | resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << functionType << "'."; + } + } + + FunctionType getFunctionType() const { + return functionType; + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::stringstream result; + result << this->getLeft()->toString(); + switch (functionType) { + case AND: result << " & "; break; + case OR: result << " | "; break; + } + result << this->getRight()->toString(); + + return result.str(); + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BinaryBooleanFunctionExpression" << std::endl; + result << this->getLeft()->dump(prefix + "\t"); + switch (functionType) { + case AND: result << prefix << "&" << std::endl; break; + case OR: result << prefix << "|" << std::endl; break; + } + result << this->getRight()->dump(prefix + "\t"); + return result.str(); + } + +private: + FunctionType functionType; +}; + +} // namespace expressions + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/BinaryExpression.h b/src/ir/expressions/BinaryExpression.h new file mode 100644 index 000000000..529f6ea90 --- /dev/null +++ b/src/ir/expressions/BinaryExpression.h @@ -0,0 +1,46 @@ +/* + * BinaryExpression.h + * + * Created on: 27.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ + +#include "src/ir/expressions/BaseExpression.h" +#include +#include + +namespace storm { + +namespace ir { + +namespace expressions { + +class BinaryExpression : public BaseExpression { +public: + BinaryExpression(ReturnType type, std::shared_ptr left, std::shared_ptr right) + : BaseExpression(type), left(left), right(right) { + } + + std::shared_ptr const& getLeft() const { + return left; + } + + std::shared_ptr const& getRight() const { + return right; + } + +private: + std::shared_ptr left; + std::shared_ptr right; +}; + +} // namespace expressions + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ */ diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h new file mode 100644 index 000000000..54239c46a --- /dev/null +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -0,0 +1,112 @@ +/* + * BinaryFunctionExpression.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef BINARYFUNCTIONEXPRESSION_H_ +#define BINARYFUNCTIONEXPRESSION_H_ + +#include "src/ir/expressions/BaseExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class BinaryNumericalFunctionExpression : public BinaryExpression { +public: + enum FunctionType {PLUS, MINUS, TIMES, DIVIDE}; + + BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr left, std::shared_ptr right, FunctionType functionType) : BinaryExpression(type, left, right), functionType(functionType) { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType)); + } + + virtual ~BinaryNumericalFunctionExpression() { + + } + + FunctionType getFunctionType() const { + return functionType; + } + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { + if (this->getType() != int_) { + BaseExpression::getValueAsInt(variableValues); + } + + int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues); + int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues); + switch(functionType) { + case PLUS: return resultLeft + resultRight; break; + case MINUS: return resultLeft - resultRight; break; + case TIMES: return resultLeft * resultRight; break; + case DIVIDE: return resultLeft / resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numeric binary operator: '" << functionType << "'."; + } + } + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { + if (this->getType() != double_) { + BaseExpression::getValueAsDouble(variableValues); + } + + double resultLeft = this->getLeft()->getValueAsDouble(variableValues); + double resultRight = this->getRight()->getValueAsDouble(variableValues); + switch(functionType) { + case PLUS: return resultLeft + resultRight; break; + case MINUS: return resultLeft - resultRight; break; + case TIMES: return resultLeft * resultRight; break; + case DIVIDE: return resultLeft / resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numeric binary operator: '" << functionType << "'."; + } + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::string result = this->getLeft()->toString(); + switch (functionType) { + case PLUS: result += " + "; break; + case MINUS: result += " - "; break; + case TIMES: result += " * "; break; + case DIVIDE: result += " / "; break; + } + result += this->getRight()->toString(); + return result; + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BinaryNumericalFunctionExpression" << std::endl; + result << this->getLeft()->dump(prefix + "\t"); + switch (functionType) { + case PLUS: result << prefix << "+" << std::endl; break; + case MINUS: result << prefix << "-" << std::endl; break; + case TIMES: result << prefix << "*" << std::endl; break; + case DIVIDE: result << prefix << "/" << std::endl; break; + } + result << this->getRight()->dump(prefix + "\t"); + return result.str(); + } +private: + FunctionType functionType; +}; + +} + +} + +} + +#endif /* BINARYFUNCTIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h new file mode 100644 index 000000000..8d6184ff7 --- /dev/null +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -0,0 +1,98 @@ +/* + * BinaryRelationExpression.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef BINARYRELATIONEXPRESSION_H_ +#define BINARYRELATIONEXPRESSION_H_ + +#include "src/ir/expressions/BinaryExpression.h" +#include + +namespace storm { + +namespace ir { + +namespace expressions { + +class BinaryRelationExpression : public BinaryExpression { +public: + enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; + + BinaryRelationExpression(std::shared_ptr left, std::shared_ptr right, RelationType relationType) : BinaryExpression(bool_, left, right), relationType(relationType) { + } + + virtual ~BinaryRelationExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType)); + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { + int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues); + int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues); + switch(relationType) { + case EQUAL: return resultLeft == resultRight; break; + case NOT_EQUAL: return resultLeft != resultRight; break; + case LESS: return resultLeft < resultRight; break; + case LESS_OR_EQUAL: return resultLeft <= resultRight; break; + case GREATER: return resultLeft > resultRight; break; + case GREATER_OR_EQUAL: return resultLeft >= resultRight; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary relation: '" << relationType << "'."; + } + } + + RelationType getRelationType() const { + return relationType; + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::string result = this->getLeft()->toString(); + switch (relationType) { + case EQUAL: result += " = "; break; + case NOT_EQUAL: result += " != "; break; + case LESS: result += " < "; break; + case LESS_OR_EQUAL: result += " <= "; break; + case GREATER: result += " > "; break; + case GREATER_OR_EQUAL: result += " >= "; break; + } + result += this->getRight()->toString(); + + return result; + } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BinaryRelationExpression" << std::endl; + result << this->getLeft()->dump(prefix + "\t"); + switch (relationType) { + case EQUAL: result << prefix << "=" << std::endl; break; + case NOT_EQUAL: result << prefix << "!=" << std::endl; break; + case LESS: result << prefix << "<" << std::endl; break; + case LESS_OR_EQUAL: result << prefix << "<=" << std::endl; break; + case GREATER: result << prefix << ">" << std::endl; break; + case GREATER_OR_EQUAL: result << prefix << ">=" << std::endl; break; + } + result << this->getRight()->dump(prefix + "\t"); + return result.str(); + } + +private: + RelationType relationType; +}; + +} + +} + +} + +#endif /* BINARYRELATIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h new file mode 100644 index 000000000..2f3889b01 --- /dev/null +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -0,0 +1,89 @@ +/* + * BooleanConstantExpression.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef BOOLEANCONSTANTEXPRESSION_H_ +#define BOOLEANCONSTANTEXPRESSION_H_ + +#include "ConstantExpression.h" + +#include + +namespace storm { + +namespace ir { + +namespace expressions { + +class BooleanConstantExpression : public ConstantExpression { +public: + BooleanConstantExpression(std::string constantName) : ConstantExpression(bool_, constantName) { + defined = false; + value = false; + } + BooleanConstantExpression(const BooleanConstantExpression& bce) + : ConstantExpression(bce), value(bce.value), defined(bce.defined) { + } + + virtual ~BooleanConstantExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new BooleanConstantExpression(*this)); + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Boolean constant '" << this->getConstantName() << "' is undefined."; + } else { + return value; + } + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::string result = this->constantName; + if (defined) { + result += "[" + boost::lexical_cast(value) + "]"; + } + return result; + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BooleanConstantExpression " << this->toString() << std::endl; + return result.str(); + } + + bool isDefined() { + return defined; + } + + bool getValue() { + return value; + } + + void define(bool value) { + defined = true; + this->value = value; + } + + bool value; + bool defined; +}; + +} + +} + +} + +#endif /* BOOLEANCONSTANTEXPRESSION_H_ */ diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h new file mode 100644 index 000000000..f6bcd3ab3 --- /dev/null +++ b/src/ir/expressions/BooleanLiteral.h @@ -0,0 +1,62 @@ +/* + * BooleanLiteral.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef BOOLEANLITERAL_H_ +#define BOOLEANLITERAL_H_ + +#include "src/ir/expressions/BaseExpression.h" + +namespace storm { +namespace ir { +namespace expressions { + +class BooleanLiteral : public BaseExpression { +public: + bool value; + + BooleanLiteral(bool value) : BaseExpression(bool_), value(value) { + + } + + virtual ~BooleanLiteral() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new BooleanLiteral(this->value)); + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { + return value; + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + if (value) { + return std::string("true"); + } else { + return std::string("false"); + } + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "BooleanLiteral " << this->toString() << std::endl; + return result.str(); + } +}; + +} + +} + +} + +#endif /* BOOLEANLITERAL_H_ */ diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h new file mode 100644 index 000000000..239dca81c --- /dev/null +++ b/src/ir/expressions/ConstantExpression.h @@ -0,0 +1,55 @@ +/* + * ConstantExpression.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef CONSTANTEXPRESSION_H_ +#define CONSTANTEXPRESSION_H_ + +#include "src/ir/expressions/BaseExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class ConstantExpression : public BaseExpression { +public: + std::string constantName; + + ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) { + } + ConstantExpression(const ConstantExpression& ce) + : BaseExpression(ce), constantName(ce.constantName) { + + } + + virtual ~ConstantExpression() { + + } + + std::string const& getConstantName() const { + return constantName; + } + + virtual std::string toString() const { + return constantName; + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "ConstantExpression " << this->toString() << std::endl; + return result.str(); + } +}; + +} + +} + +} + +#endif /* CONSTANTEXPRESSION_H_ */ diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h new file mode 100644 index 000000000..f6e26271d --- /dev/null +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -0,0 +1,87 @@ +/* + * DoubleConstantExpression.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef DOUBLECONSTANTEXPRESSION_H_ +#define DOUBLECONSTANTEXPRESSION_H_ + +#include "ConstantExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class DoubleConstantExpression : public ConstantExpression { +public: + DoubleConstantExpression(std::string constantName) : ConstantExpression(double_, constantName), defined(false), value(0) { + } + + DoubleConstantExpression(const DoubleConstantExpression& dce) + : ConstantExpression(dce), defined(dce.defined), value(dce.value) { + } + + virtual ~DoubleConstantExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new DoubleConstantExpression(*this)); + } + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Double constant '" << this->getConstantName() << "' is undefined."; + } else { + return value; + } + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::string result = this->constantName; + if (defined) { + result += "[" + boost::lexical_cast(value) + "]"; + } + return result; + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "DoubleConstantExpression " << this->toString() << std::endl; + return result.str(); + } + + bool isDefined() { + return defined; + } + + double getValue() { + return value; + } + + void define(double value) { + defined = true; + this->value = value; + } + +private: + bool defined; + double value; +}; + +} + +} + +} + +#endif /* DOUBLECONSTANTEXPRESSION_H_ */ diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h new file mode 100644 index 000000000..4717b6708 --- /dev/null +++ b/src/ir/expressions/DoubleLiteral.h @@ -0,0 +1,62 @@ +/* + * DoubleLiteral.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef DOUBLELITERAL_H_ +#define DOUBLELITERAL_H_ + +#include "src/ir/expressions/BaseExpression.h" + +#include "boost/lexical_cast.hpp" + +namespace storm { + +namespace ir { + +namespace expressions { + +class DoubleLiteral : public BaseExpression { +public: + double value; + + DoubleLiteral(double value) : BaseExpression(double_), value(value) { + + } + + virtual ~DoubleLiteral() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new DoubleLiteral(this->value)); + } + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { + return value; + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + return boost::lexical_cast(value); + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "DoubleLiteral " << this->toString() << std::endl; + return result.str(); + } +}; + +} + +} + +} + +#endif /* DOUBLELITERAL_H_ */ diff --git a/src/ir/expressions/ExpressionVisitor.h b/src/ir/expressions/ExpressionVisitor.h new file mode 100644 index 000000000..6a8d9d813 --- /dev/null +++ b/src/ir/expressions/ExpressionVisitor.h @@ -0,0 +1,55 @@ +/* + * ExpressionVisitor.h + * + * Created on: 26.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ +#define STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ + +namespace storm { + +namespace ir { + +namespace expressions { + +class BaseExpression; +class BinaryBooleanFunctionExpression; +class BinaryNumericalFunctionExpression; +class BinaryRelationExpression; +class BooleanConstantExpression; +class BooleanLiteral; +class DoubleConstantExpression; +class DoubleLiteral; +class IntegerConstantExpression; +class IntegerLiteral; +class UnaryBooleanFunctionExpression; +class UnaryNumericalFunctionExpression; +class VariableExpression; + +class ExpressionVisitor { +public: + virtual void visit(BaseExpression* expression) = 0; + virtual void visit(BinaryBooleanFunctionExpression* expression) = 0; + virtual void visit(BinaryNumericalFunctionExpression* expression) = 0; + virtual void visit(BinaryRelationExpression* expression) = 0; + virtual void visit(BooleanConstantExpression* expression) = 0; + virtual void visit(BooleanLiteral* expression) = 0; + virtual void visit(DoubleConstantExpression* expression) = 0; + virtual void visit(DoubleLiteral* expression) = 0; + virtual void visit(IntegerConstantExpression* expression) = 0; + virtual void visit(IntegerLiteral* expression) = 0; + virtual void visit(UnaryBooleanFunctionExpression* expression) = 0; + virtual void visit(UnaryNumericalFunctionExpression* expression) = 0; + virtual void visit(VariableExpression* expression) = 0; +}; + +} // namespace expressions + +} // namespace ir + +} // namespace storm + + +#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ diff --git a/src/ir/expressions/Expressions.h b/src/ir/expressions/Expressions.h new file mode 100644 index 000000000..0de025b9f --- /dev/null +++ b/src/ir/expressions/Expressions.h @@ -0,0 +1,26 @@ +/* + * Expressions.h + * + * Created on: 03.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ +#define STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ + +#include "BaseExpression.h" +#include "BinaryBooleanFunctionExpression.h" +#include "BinaryNumericalFunctionExpression.h" +#include "BinaryRelationExpression.h" +#include "BooleanLiteral.h" +#include "DoubleLiteral.h" +#include "IntegerLiteral.h" +#include "UnaryBooleanFunctionExpression.h" +#include "UnaryNumericalFunctionExpression.h" +#include "VariableExpression.h" +#include "ConstantExpression.h" +#include "BooleanConstantExpression.h" +#include "IntegerConstantExpression.h" +#include "DoubleConstantExpression.h" + +#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ */ diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h new file mode 100644 index 000000000..c4ad56ed7 --- /dev/null +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -0,0 +1,85 @@ +/* + * IntegerConstantExpression.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef INTEGERCONSTANTEXPRESSION_H_ +#define INTEGERCONSTANTEXPRESSION_H_ + +#include "ConstantExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class IntegerConstantExpression : public ConstantExpression { +public: + IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) { + } + IntegerConstantExpression(const IntegerConstantExpression& ice) + : ConstantExpression(ice), defined(ice.defined), value(ice.value) { + } + + virtual ~IntegerConstantExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new IntegerConstantExpression(*this)); + } + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Integer constant '" << this->getConstantName() << "' is undefined."; + } else { + return value; + } + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::string result = this->constantName; + if (defined) { + result += "[" + boost::lexical_cast(value) + "]"; + } + return result; + } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "IntegerConstantExpression " << this->toString() << std::endl; + return result.str(); + } + + bool isDefined() { + return defined; + } + + int getValue() { + return value; + } + + void define(int_fast64_t value) { + defined = true; + this->value = value; + } + +private: + bool defined; + int_fast64_t value; +}; + +} + +} + +} + +#endif /* INTEGERCONSTANTEXPRESSION_H_ */ diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h new file mode 100644 index 000000000..5a42671cd --- /dev/null +++ b/src/ir/expressions/IntegerLiteral.h @@ -0,0 +1,57 @@ +/* + * IntegerLiteral.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef INTEGERLITERAL_H_ +#define INTEGERLITERAL_H_ + +#include "src/ir/expressions/BaseExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class IntegerLiteral : public BaseExpression { +public: + int_fast64_t value; + + IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) { + } + + virtual ~IntegerLiteral() { + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new IntegerLiteral(this->value)); + } + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { + return value; + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + return boost::lexical_cast(value); + } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "IntegerLiteral " << this->toString() << std::endl; + return result.str(); + } +}; + +} + +} + +} + +#endif /* INTEGERLITERAL_H_ */ diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h new file mode 100644 index 000000000..9883d6276 --- /dev/null +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -0,0 +1,81 @@ +/* + * UnaryBooleanFunctionExpression.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef UNARYBOOLEANFUNCTIONEXPRESSION_H_ +#define UNARYBOOLEANFUNCTIONEXPRESSION_H_ + +#include "src/ir/expressions/UnaryExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class UnaryBooleanFunctionExpression : public UnaryExpression { +public: + enum FunctionType {NOT}; + + UnaryBooleanFunctionExpression(std::shared_ptr child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) { + + } + + virtual ~UnaryBooleanFunctionExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, bools, ints), this->functionType)); + } + + FunctionType getFunctionType() const { + return functionType; + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { + bool resultChild = this->getChild()->getValueAsBool(variableValues); + switch(functionType) { + case NOT: return !resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean unary operator: '" << functionType << "'."; + } + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::string result = ""; + switch (functionType) { + case NOT: result += "!"; break; + } + result += "(" + this->getChild()->toString() + ")"; + + return result; + } + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "UnaryBooleanFunctionExpression" << std::endl; + switch (functionType) { + case NOT: result << prefix << "!" << std::endl; break; + } + result << this->getChild()->dump(prefix + "\t"); + return result.str(); + } + +private: + FunctionType functionType; +}; + +} + +} + +} + +#endif /* UNARYBOOLEANFUNCTIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/UnaryExpression.h b/src/ir/expressions/UnaryExpression.h new file mode 100644 index 000000000..177b5593e --- /dev/null +++ b/src/ir/expressions/UnaryExpression.h @@ -0,0 +1,39 @@ +/* + * UnaryExpression.h + * + * Created on: 27.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ +#define STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ + +#include "BaseExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class UnaryExpression : public BaseExpression { +public: + UnaryExpression(ReturnType type, std::shared_ptr child) : BaseExpression(type), child(child) { + + } + + std::shared_ptr const& getChild() const { + return child; + } + +private: + std::shared_ptr child; +}; + +} // namespace expressions + +} // namespace ir + +} // namespace storm + +#endif /* STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ */ diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h new file mode 100644 index 000000000..d0a770494 --- /dev/null +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -0,0 +1,99 @@ +/* + * UnaryFunctionExpression.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef UNARYFUNCTIONEXPRESSION_H_ +#define UNARYFUNCTIONEXPRESSION_H_ + +#include "src/ir/expressions/UnaryExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class UnaryNumericalFunctionExpression : public UnaryExpression { +public: + enum FunctionType {MINUS}; + + UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) { + + } + + virtual ~UnaryNumericalFunctionExpression() { + + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + return std::shared_ptr(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, bools, ints), this->functionType)); + } + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { + if (this->getType() != int_) { + BaseExpression::getValueAsInt(variableValues); + } + + int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues); + switch(functionType) { + case MINUS: return -resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numerical unary operator: '" << functionType << "'."; + } + } + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { + if (this->getType() != double_) { + BaseExpression::getValueAsDouble(variableValues); + } + + double resultChild = this->getChild()->getValueAsDouble(variableValues); + switch(functionType) { + case MINUS: return -resultChild; break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown numerical unary operator: '" << functionType << "'."; + } + } + + FunctionType getFunctionType() const { + return functionType; + } + + virtual void accept(ExpressionVisitor* visitor) { + visitor->visit(this); + } + + virtual std::string toString() const { + std::string result = ""; + switch (functionType) { + case MINUS: result += "-"; break; + } + result += this->getChild()->toString(); + + return result; + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << "UnaryNumericalFunctionExpression" << std::endl; + switch (functionType) { + case MINUS: result << prefix << "-" << std::endl; break; + } + result << this->getChild()->dump(prefix + "\t"); + return result.str(); + } + +private: + FunctionType functionType; +}; + +} + +} + +} + +#endif /* UNARYFUNCTIONEXPRESSION_H_ */ diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h new file mode 100644 index 000000000..54bebce72 --- /dev/null +++ b/src/ir/expressions/VariableExpression.h @@ -0,0 +1,146 @@ +/* + * VariableExpression.h + * + * Created on: 03.01.2013 + * Author: chris + */ + +#ifndef VARIABLEEXPRESSION_H_ +#define VARIABLEEXPRESSION_H_ + +#include "src/ir/expressions/BaseExpression.h" + +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +namespace storm { + +namespace ir { + +namespace expressions { + +class VariableExpression : public BaseExpression { +public: + VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName, + std::shared_ptr lowerBound = std::shared_ptr(nullptr), + std::shared_ptr upperBound = std::shared_ptr(nullptr)) + : BaseExpression(type), index(index), variableName(variableName), + lowerBound(lowerBound), upperBound(upperBound) { + } + + virtual ~VariableExpression() { + } + + virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { + std::shared_ptr lower = this->lowerBound, upper = this->upperBound; + if (lower != nullptr) lower = lower->clone(renaming, bools, ints); + if (upper != nullptr) upper = upper->clone(renaming, bools, ints); + if (renaming.count(this->variableName) > 0) { + std::string newName = renaming.at(this->variableName); + if (this->getType() == bool_) { + return std::shared_ptr(new VariableExpression(bool_, bools.at(newName), newName, lower, upper)); + } else if (this->getType() == int_) { + return std::shared_ptr(new VariableExpression(int_, ints.at(newName), newName, lower, upper)); + } else { + LOG4CPLUS_ERROR(logger, "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int."); + return std::shared_ptr(nullptr); + } + } else { + return std::shared_ptr(new VariableExpression(this->getType(), this->index, this->variableName, lower, upper)); + } + } + + + virtual void accept(ExpressionVisitor* visitor) { + std::cout << "Visitor!" << std::endl; + visitor->visit(this); + } + + virtual std::string toString() const { + return this->variableName; + } + + virtual std::string dump(std::string prefix) const { + std::stringstream result; + result << prefix << this->variableName << " " << index << std::endl; + if (this->lowerBound != nullptr) { + result << prefix << "lower bound" << std::endl; + result << this->lowerBound->dump(prefix + "\t"); + } + if (this->upperBound != nullptr) { + result << prefix << "upper bound" << std::endl; + result << this->upperBound->dump(prefix + "\t"); + } + return result.str(); + } + + virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const { + if (this->getType() != int_) { + BaseExpression::getValueAsInt(variableValues); + } + + if (variableValues != nullptr) { + return variableValues->second[index]; + } else { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" + << " involving variables without variable values."; + } + } + + virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const { + if (this->getType() != bool_) { + BaseExpression::getValueAsBool(variableValues); + } + + if (variableValues != nullptr) { + return variableValues->first[index]; + } else { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" + << " involving variables without variable values."; + } + } + + virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const { + if (this->getType() != double_) { + BaseExpression::getValueAsDouble(variableValues); + } + + throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with " + << " variable '" << variableName << "' of type double."; + } + + std::string const& getVariableName() const { + return variableName; + } + + std::shared_ptr const& getLowerBound() const { + return lowerBound; + } + + std::shared_ptr const& getUpperBound() const { + return upperBound; + } + + uint_fast64_t getVariableIndex() const { + return this->index; + } + +private: + uint_fast64_t index; + std::string variableName; + + std::shared_ptr lowerBound; + std::shared_ptr upperBound; +}; + +} + +} + +} + +#endif /* VARIABLEEXPRESSION_H_ */ diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 586de6e5e..87c2322d7 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -70,6 +70,14 @@ public: ~Mdp() { // Intentionally left empty. } + + /*! + * Returns the number of choices for all states of the MDP. + * @return The number of choices for all states of the MDP. + */ + uint_fast64_t getNumberOfChoices() const { + return this->probabilityMatrix->getRowCount(); + } storm::models::ModelType getType() const { return MDP; diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp new file mode 100644 index 000000000..648962689 --- /dev/null +++ b/src/parser/PrismParser.cpp @@ -0,0 +1,128 @@ +/* + * PrismParser.cpp + * + * Created on: 11.01.2013 + * Author: chris + */ + +#include "PrismParser.h" + +#include "src/utility/OsDetection.h" + +#include "src/parser/PrismParser/PrismGrammar.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/WrongFileFormatException.h" + +// Needed for file IO. +#include +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + + +namespace storm { +namespace parser { + +/*! + * Opens the given file for parsing, invokes the helper function to parse the actual content and + * closes the file properly, even if an exception is thrown in the parser. In this case, the + * exception is passed on to the caller. + */ +storm::ir::Program PrismParser::parseFile(std::string const& filename) const { + // Open file and initialize result. + std::ifstream inputFileStream(filename, std::ios::in); + storm::ir::Program result; + + // Now try to parse the contents of the file. + try { + result = parse(inputFileStream, filename); + } catch(std::exception& e) { + // In case of an exception properly close the file before passing exception. + inputFileStream.close(); + throw e; + } + + // Close the stream in case everything went smoothly and return result. + inputFileStream.close(); + return result; +} + +/*! + * Passes iterators to the input stream to the Boost spirit parser and thereby parses the input. + * If the parser throws an expectation failure exception, i.e. expected input different than the one + * provided, this is caught and displayed properly before the exception is passed on. + */ +storm::ir::Program PrismParser::parse(std::istream& inputStream, std::string const& filename) const { + // Prepare iterators to input. + // TODO: Right now, this parses the whole contents of the file into a string first. + // While this is usually not necessary, because there exist adapters that make an input stream + // iterable in both directions without storing it into a string, using the corresponding + // Boost classes gives an awful output under valgrind and is thus disabled for the time being. + std::string fileContent((std::istreambuf_iterator(inputStream)), (std::istreambuf_iterator())); + BaseIteratorType stringIteratorBegin = fileContent.begin(); + BaseIteratorType stringIteratorEnd = fileContent.end(); + PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename); + PositionIteratorType positionIteratorBegin2(stringIteratorBegin, stringIteratorEnd, filename); + PositionIteratorType positionIteratorEnd; + + // Prepare resulting intermediate representation of input. + storm::ir::Program result; + + // In order to instantiate the grammar, we have to pass the type of the skipping parser. + // As this is more complex, we let Boost figure out the actual type for us. + prism::PrismGrammar grammar; + try { + // Now parse the content using phrase_parse in order to be able to supply a skipping parser. + // First run. + LOG4CPLUS_INFO(logger, "Start parsing..."); + qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); + grammar.prepareForSecondRun(); + result = storm::ir::Program(); + LOG4CPLUS_INFO(logger, "Start second parsing run..."); + // Second run. + qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); + LOG4CPLUS_INFO(logger, "Finished parsing, here is the parsed program:" << std::endl << result.toString()); + // Reset grammars. + grammar.resetGrammars(); + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + std::string line = e.first.get_currentline(); + while (line.find('\t') != std::string::npos) line.replace(line.find('\t'),1," "); + msg << pos.file << ", line " << pos.line << ", column " << pos.column + << ": parse error: expected " << e.what_ << std::endl << "\t" + << line << std::endl << "\t"; + int i = 0; + for (i = 1; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; + + std::cerr << msg.str(); + + // Reset grammars in any case. + grammar.resetGrammars(); + + // Now propagate exception. + throw storm::exceptions::WrongFileFormatException() << msg.str(); + } + + return result; +} + +} // namespace parser + +} // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h new file mode 100644 index 000000000..48326713f --- /dev/null +++ b/src/parser/PrismParser.h @@ -0,0 +1,52 @@ +/* * PrismParser.h + * + * Created on: Jan 3, 2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_PARSER_PRISMPARSER_H_ +#define STORM_PARSER_PRISMPARSER_H_ + +// All classes of the intermediate representation are used. +#include "src/ir/IR.h" + +// Used for file input. +#include +#include + +namespace storm { + +namespace parser { + +using namespace storm::ir; +using namespace storm::ir::expressions; + +/*! + * This class parses the format of the PRISM model checker into an intermediate representation. + */ +class PrismParser { +public: + /*! + * Parses the given file into the intermediate representation assuming it complies with the + * PRISM syntax. + * @param filename the name of the file to parse. + * @return a shared pointer to the intermediate representation of the PRISM file. + */ + storm::ir::Program parseFile(std::string const& filename) const; + +private: + /*! + * Parses the given input stream into the intermediate representation assuming it complies with + * the PRISM syntax. + * @param inputStream the input stream to parse. + * @param filename the name of the file the input stream belongs to. Used for diagnostics. + * @return a shared pointer to the intermediate representation of the PRISM file. + */ + storm::ir::Program parse(std::istream& inputStream, std::string const& filename) const; +}; + +} // namespace parser + +} // namespace storm + +#endif /* STORM_PARSER_PRISMPARSER_H_ */ diff --git a/src/parser/PrismParser/BaseGrammar.h b/src/parser/PrismParser/BaseGrammar.h new file mode 100644 index 000000000..345a377e0 --- /dev/null +++ b/src/parser/PrismParser/BaseGrammar.h @@ -0,0 +1,112 @@ +/* + * File: Keywords.h + * Author: nafur + * + * Created on April 10, 2013, 6:03 PM + */ + +#ifndef BASEGRAMMAR_H +#define BASEGRAMMAR_H + +#include "Includes.h" + +#include "VariableState.h" + +namespace storm { +namespace parser { +namespace prism { + + template + class BaseGrammar { + public: + BaseGrammar(std::shared_ptr& state) : state(state) {} + + static T& instance(std::shared_ptr state = nullptr) { + if (BaseGrammar::instanceObject == nullptr) { + BaseGrammar::instanceObject = std::shared_ptr(new T(state)); + if (!state->firstRun) BaseGrammar::instanceObject->secondRun(); + } + return *BaseGrammar::instanceObject; + } + + static void resetInstance() { + BaseGrammar::instanceObject = nullptr; + } + + static void secondRun() { + if (BaseGrammar::instanceObject != nullptr) { + BaseGrammar::instanceObject->prepareSecondRun(); + } + } + + std::shared_ptr createBoolLiteral(const bool value) { + return std::shared_ptr(new BooleanLiteral(value)); + } + std::shared_ptr createDoubleLiteral(const double value) { + return std::shared_ptr(new DoubleLiteral(value)); + } + std::shared_ptr createIntLiteral(const int_fast64_t value) { + return std::shared_ptr(new IntegerLiteral(value)); + } + + std::shared_ptr createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right, BaseExpression::ReturnType type) { + if (addition) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::PLUS)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::MINUS)); + } + } + std::shared_ptr createDoublePlus(const std::shared_ptr left, bool addition, const std::shared_ptr right) { + return this->createPlus(left, addition, right, BaseExpression::double_); + } + std::shared_ptr createIntPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right) { + return this->createPlus(left, addition, right, BaseExpression::int_); + } + + std::shared_ptr createIntMult(const std::shared_ptr left, const std::shared_ptr right) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left, right, BinaryNumericalFunctionExpression::TIMES)); + } + std::shared_ptr createDoubleMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right) { + if (multiplication) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); + } + } + + std::shared_ptr createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right) { + return std::shared_ptr(new BinaryRelationExpression(left, right, relationType)); + } + std::shared_ptr createNot(std::shared_ptr child) { + return std::shared_ptr(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); + } + std::shared_ptr createAnd(std::shared_ptr left, std::shared_ptr right) { + //std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl; + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); + } + std::shared_ptr createOr(std::shared_ptr left, std::shared_ptr right) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); + } + std::shared_ptr getBoolVariable(const std::string name) { + return state->getBooleanVariable(name); + } + std::shared_ptr getIntVariable(const std::string name) { + return state->getIntegerVariable(name); + } + + virtual void prepareSecondRun() {} + protected: + std::shared_ptr state; + + private: + static std::shared_ptr instanceObject; + static bool inSecondRun; + }; + + template + std::shared_ptr BaseGrammar::instanceObject; +} +} +} +#endif /* BASEGRAMMAR_H */ + diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.cpp b/src/parser/PrismParser/BooleanExpressionGrammar.cpp new file mode 100644 index 000000000..6a2d421bb --- /dev/null +++ b/src/parser/PrismParser/BooleanExpressionGrammar.cpp @@ -0,0 +1,42 @@ +#include "BooleanExpressionGrammar.h" + +#include "IntegerExpressionGrammar.h" +#include "ConstBooleanExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + + BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr& state) + : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) { + + booleanExpression %= orExpression; + booleanExpression.name("boolean expression"); + + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)]; + orExpression.name("boolean expression"); + + andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)]; + andExpression.name("boolean expression"); + + notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)]; + notExpression.name("boolean expression"); + + atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state)); + atomicBooleanExpression.name("boolean expression"); + + relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; + relativeExpression.name("relative expression"); + + booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)]; + booleanVariableExpression.name("boolean variable"); + } + + void BooleanExpressionGrammar::prepareSecondRun() { + booleanVariableExpression %= this->state->booleanVariables_; + booleanVariableExpression.name("boolean variable"); + } + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.h b/src/parser/PrismParser/BooleanExpressionGrammar.h new file mode 100644 index 000000000..9e976e64d --- /dev/null +++ b/src/parser/PrismParser/BooleanExpressionGrammar.h @@ -0,0 +1,44 @@ +/* + * File: BooleanExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 6:27 PM + */ + +#ifndef BOOLEANEXPRESSIONGRAMMAR_H +#define BOOLEANEXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "VariableState.h" +#include "IdentifierGrammars.h" +#include "Tokens.h" + +#include + +namespace storm { +namespace parser { +namespace prism { + +class BooleanExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { +public: + BooleanExpressionGrammar(std::shared_ptr& state); + virtual void prepareSecondRun(); + +private: + qi::rule(), Skipper, Unused> booleanExpression; + qi::rule(), Skipper> orExpression; + qi::rule(), Skipper> andExpression; + qi::rule(), Skipper> notExpression; + qi::rule(), Skipper> atomicBooleanExpression; + qi::rule(), Skipper> relativeExpression; + qi::rule(), Skipper> booleanVariableExpression; + + storm::parser::prism::relationalOperatorStruct relations_; +}; + + +} +} +} + +#endif /* BOOLEANEXPRESSIONGRAMMAR_H */ diff --git a/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp b/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp new file mode 100644 index 000000000..203894638 --- /dev/null +++ b/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp @@ -0,0 +1,54 @@ +#include "ConstBooleanExpressionGrammar.h" + +#include "ConstIntegerExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + + std::shared_ptr ConstBooleanExpressionGrammar::createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right) { + return std::shared_ptr(new BinaryRelationExpression(left, right, relationType)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createNot(std::shared_ptr child) { + return std::shared_ptr(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createAnd(std::shared_ptr left, std::shared_ptr right) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createOr(std::shared_ptr left, std::shared_ptr right) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createLiteral(const bool value) { + return std::shared_ptr(new BooleanLiteral(value)); + } + + ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr& state) + : ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), BaseGrammar(state) { + + constantBooleanExpression %= constantOrExpression; + constantBooleanExpression.name("constant boolean expression"); + + constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createOr, this, qi::_val, qi::_1)]; + constantOrExpression.name("constant boolean expression"); + + constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createAnd, this, qi::_val, qi::_1)]; + constantAndExpression.name("constant boolean expression"); + + constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createNot, this, qi::_1)]; + constantNotExpression.name("constant boolean expression"); + + constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); + constantAtomicBooleanExpression.name("constant boolean expression"); + + constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; + constantRelativeExpression.name("constant boolean expression"); + + booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression); + booleanConstantExpression.name("boolean constant or literal"); + + booleanLiteralExpression = qi::bool_[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createLiteral, this, qi::_1)]; + booleanLiteralExpression.name("boolean literal"); + } +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/ConstBooleanExpressionGrammar.h b/src/parser/PrismParser/ConstBooleanExpressionGrammar.h new file mode 100644 index 000000000..4c8a5f7fb --- /dev/null +++ b/src/parser/PrismParser/ConstBooleanExpressionGrammar.h @@ -0,0 +1,50 @@ +/* + * File: ConstBooleanExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 6:34 PM + */ + +#ifndef CONSTBOOLEANEXPRESSIONGRAMMAR_H +#define CONSTBOOLEANEXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "VariableState.h" +#include "IdentifierGrammars.h" +#include "Tokens.h" + +namespace storm { +namespace parser { +namespace prism { + +class ConstBooleanExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { +public: + ConstBooleanExpressionGrammar(std::shared_ptr& state); + + +private: + qi::rule(), Skipper, Unused> constantBooleanExpression; + qi::rule(), Skipper> constantOrExpression; + qi::rule(), Skipper> constantAndExpression; + qi::rule(), Skipper> constantNotExpression; + qi::rule(), Skipper> constantAtomicBooleanExpression; + qi::rule(), Skipper> constantRelativeExpression; + qi::rule(), Skipper> booleanConstantExpression; + qi::rule(), Skipper> booleanLiteralExpression; + + storm::parser::prism::relationalOperatorStruct relations_; + + std::shared_ptr createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right); + std::shared_ptr createNot(std::shared_ptr child); + std::shared_ptr createAnd(std::shared_ptr left, std::shared_ptr right); + std::shared_ptr createOr(std::shared_ptr left, std::shared_ptr right); + std::shared_ptr createLiteral(const bool value); +}; + + +} +} +} + +#endif /* CONSTBOOLEANEXPRESSIONGRAMMAR_H */ + diff --git a/src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp b/src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp new file mode 100644 index 000000000..ddd1341f5 --- /dev/null +++ b/src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp @@ -0,0 +1,53 @@ +#include "ConstDoubleExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + + + std::shared_ptr ConstDoubleExpressionGrammar::createLiteral(double value) { + return std::shared_ptr(new DoubleLiteral(value)); + } + std::shared_ptr ConstDoubleExpressionGrammar::createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right) { + if (addition) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::PLUS)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::MINUS)); + } + } + std::shared_ptr ConstDoubleExpressionGrammar::createMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right) { + if (multiplication) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); + } + } + +ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr& state) + : ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) { + + constantDoubleExpression %= constantDoublePlusExpression; + constantDoubleExpression.name("constant double expression"); + + constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression) + [qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createPlus, this, qi::_val, qi::_a, qi::_1)]; + constantDoublePlusExpression.name("constant double expression"); + + constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> constantAtomicDoubleExpression) + [qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createMult, this, qi::_val, qi::_a, qi::_1)]; + constantDoubleMultExpression.name("constant double expression"); + + constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); + constantAtomicDoubleExpression.name("constant double expression"); + + doubleConstantExpression %= (this->state->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression); + doubleConstantExpression.name("double constant or literal"); + + doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createLiteral, this, qi::_1)]; + doubleLiteralExpression.name("double literal"); +} + + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/ConstDoubleExpressionGrammar.h b/src/parser/PrismParser/ConstDoubleExpressionGrammar.h new file mode 100644 index 000000000..9d70f9877 --- /dev/null +++ b/src/parser/PrismParser/ConstDoubleExpressionGrammar.h @@ -0,0 +1,43 @@ +/* + * File: ConstDoubleExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 7:04 PM + */ + +#ifndef CONSTDOUBLEEXPRESSIONGRAMMAR_H +#define CONSTDOUBLEEXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "VariableState.h" +#include "IdentifierGrammars.h" + +namespace storm { +namespace parser { +namespace prism { + +class ConstDoubleExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { +public: + ConstDoubleExpressionGrammar(std::shared_ptr& state); + + +private: + qi::rule(), Skipper, Unused> constantDoubleExpression; + qi::rule(), qi::locals, Skipper> constantDoublePlusExpression; + qi::rule(), qi::locals, Skipper> constantDoubleMultExpression; + qi::rule(), Skipper> constantAtomicDoubleExpression; + qi::rule(), Skipper> doubleConstantExpression; + qi::rule(), Skipper> doubleLiteralExpression; + + std::shared_ptr createLiteral(double value); + std::shared_ptr createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right); + std::shared_ptr createMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right); +}; + + +} +} +} + +#endif /* CONSTDOUBLEEXPRESSIONGRAMMAR_H */ + diff --git a/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp b/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp new file mode 100644 index 000000000..233b4492a --- /dev/null +++ b/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp @@ -0,0 +1,35 @@ +#include "ConstIntegerExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + + +ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr& state) + : ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) { + + constantIntegerExpression %= constantIntegerPlusExpression; + constantIntegerExpression.name("constant integer expression"); + + constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression) + [qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; + constantIntegerPlusExpression.name("constant integer expression"); + + constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression) + [qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]; + constantIntegerMultExpression.name("constant integer expression"); + + constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); + constantAtomicIntegerExpression.name("constant integer expression"); + + integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression); + integerConstantExpression.name("integer constant or literal"); + + integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)]; + integerLiteralExpression.name("integer literal"); + +} + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/ConstIntegerExpressionGrammar.h b/src/parser/PrismParser/ConstIntegerExpressionGrammar.h new file mode 100644 index 000000000..847892e10 --- /dev/null +++ b/src/parser/PrismParser/ConstIntegerExpressionGrammar.h @@ -0,0 +1,37 @@ +/* + * File: ConstIntegerExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 6:02 PM + */ + +#ifndef CONSTINTEGEREXPRESSIONGRAMMAR_H +#define CONSTINTEGEREXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "VariableState.h" +#include "IdentifierGrammars.h" + +namespace storm { +namespace parser { +namespace prism { + +class ConstIntegerExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { +public: + ConstIntegerExpressionGrammar(std::shared_ptr& state); + +private: + qi::rule(), Skipper, Unused> constantIntegerExpression; + qi::rule(), qi::locals, Skipper> constantIntegerPlusExpression; + qi::rule(), Skipper> constantIntegerMultExpression; + qi::rule(), Skipper> constantAtomicIntegerExpression; + qi::rule(), Skipper> integerConstantExpression; + qi::rule(), Skipper> integerLiteralExpression; +}; + + +} +} +} + +#endif /* CONSTINTEGEREXPRESSIONGRAMMAR_H */ diff --git a/src/parser/PrismParser/IdentifierGrammars.cpp b/src/parser/PrismParser/IdentifierGrammars.cpp new file mode 100644 index 000000000..552b6e2c0 --- /dev/null +++ b/src/parser/PrismParser/IdentifierGrammars.cpp @@ -0,0 +1,23 @@ +#include "IdentifierGrammars.h" + +namespace storm { +namespace parser { +namespace prism { + +IdentifierGrammar::IdentifierGrammar(std::shared_ptr& state) + : IdentifierGrammar::base_type(identifierName), BaseGrammar(state) { + + identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ]; + identifierName.name("identifier"); +} + +FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr& state) + : FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) { + + freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ]; + freeIdentifierName.name("identifier"); +} + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/IdentifierGrammars.h b/src/parser/PrismParser/IdentifierGrammars.h new file mode 100644 index 000000000..936ee732a --- /dev/null +++ b/src/parser/PrismParser/IdentifierGrammars.h @@ -0,0 +1,36 @@ +/* + * File: Keywords.h + * Author: nafur + * + * Created on April 10, 2013, 6:03 PM + */ + +#ifndef IDENTIFIERGRAMMARS_H +#define IDENTIFIERGRAMMARS_H + +#include "Includes.h" +#include "BaseGrammar.h" +#include "VariableState.h" + +namespace storm { +namespace parser { +namespace prism { + + class IdentifierGrammar : public qi::grammar, public BaseGrammar { + public: + IdentifierGrammar(std::shared_ptr& state); + private: + qi::rule identifierName; + }; + + class FreeIdentifierGrammar : public qi::grammar, public BaseGrammar { + public: + FreeIdentifierGrammar(std::shared_ptr& state); + private: + qi::rule freeIdentifierName; + }; +} +} +} +#endif /* IDENTIFIERGRAMMARS_H */ + diff --git a/src/parser/PrismParser/Includes.h b/src/parser/PrismParser/Includes.h new file mode 100644 index 000000000..3bce26d00 --- /dev/null +++ b/src/parser/PrismParser/Includes.h @@ -0,0 +1,41 @@ +/* + * File: BoostIncludes.h + * Author: nafur + * + * Created on April 10, 2013, 4:46 PM + */ + +#ifndef BOOSTINCLUDES_H +#define BOOSTINCLUDES_H + +#define DEBUGPRISM + +// Used for Boost spirit. +#include +#include +#include + +// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. +#include +#include + +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +typedef PositionIteratorType Iterator; +typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper; +typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2; +typedef boost::spirit::unused_type Unused; + +#include "src/ir/IR.h" +using namespace storm::ir; +using namespace storm::ir::expressions; + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +#endif /* BOOSTINCLUDES_H */ + diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.cpp b/src/parser/PrismParser/IntegerExpressionGrammar.cpp new file mode 100644 index 000000000..ba1a35eb6 --- /dev/null +++ b/src/parser/PrismParser/IntegerExpressionGrammar.cpp @@ -0,0 +1,36 @@ +#include "IntegerExpressionGrammar.h" + +#include "IdentifierGrammars.h" +#include "ConstIntegerExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + + IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr& state) + : IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) { + + integerExpression %= integerPlusExpression; + integerExpression.name("integer expression"); + + integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; + integerPlusExpression.name("integer expression"); + + integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]); + integerMultExpression.name("integer expression"); + + atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state)); + atomicIntegerExpression.name("integer expression"); + + integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)]; + integerVariableExpression.name("integer variable"); + } + + void IntegerExpressionGrammar::prepareSecondRun() { + integerVariableExpression %= this->state->integerVariables_; + integerVariableExpression.name("integer variable"); + } + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.h b/src/parser/PrismParser/IntegerExpressionGrammar.h new file mode 100644 index 000000000..0f44b0d01 --- /dev/null +++ b/src/parser/PrismParser/IntegerExpressionGrammar.h @@ -0,0 +1,40 @@ +/* + * File: IntegerExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 4:39 PM + */ + +#ifndef INTEGEREXPRESSIONGRAMMAR_H +#define INTEGEREXPRESSIONGRAMMAR_H + +#include "src/ir/IR.h" +#include "VariableState.h" +#include "Includes.h" +#include "IdentifierGrammars.h" + +#include + +namespace storm { +namespace parser { +namespace prism { + +class IntegerExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { +public: + IntegerExpressionGrammar(std::shared_ptr& state); + virtual void prepareSecondRun(); + +private: + qi::rule(), Skipper, Unused> integerExpression; + qi::rule(), qi::locals, Skipper> integerPlusExpression; + qi::rule(), Skipper> integerMultExpression; + qi::rule(), Skipper> atomicIntegerExpression; + qi::rule(), Skipper> integerVariableExpression; +}; + +} +} +} + +#endif /* INTEGEREXPRESSIONGRAMMAR_H */ + diff --git a/src/parser/PrismParser/PrismGrammar.cpp b/src/parser/PrismParser/PrismGrammar.cpp new file mode 100644 index 000000000..1fb3ff00e --- /dev/null +++ b/src/parser/PrismParser/PrismGrammar.cpp @@ -0,0 +1,258 @@ +/* + * PrismGrammar.cpp + * + * Created on: 11.01.2013 + * Author: chris + */ + +#include "PrismGrammar.h" + +#include "src/utility/OsDetection.h" + +#include "src/parser/PrismParser/Includes.h" +#include "src/parser/PrismParser/BooleanExpressionGrammar.h" +#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" +#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" +#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" +#include "src/parser/PrismParser/IntegerExpressionGrammar.h" +#include "src/parser/PrismParser/IdentifierGrammars.h" +#include "src/parser/PrismParser/VariableState.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/WrongFileFormatException.h" + +// Needed for file IO. +#include +#include +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; + +// Some typedefs and namespace definitions to reduce code size. +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +namespace storm { +namespace parser { +namespace prism { + +void dump(const std::string& s) { + std::cerr << "Dump: " << s << std::endl; +} + +std::shared_ptr PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr value) { + this->state->integerConstants_.add(name, value); + this->state->allConstantNames_.add(name, name); + return value; +} + +void PrismGrammar::addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping) { + this->state->labelNames_.add(name, name); + mapping[name] = value; +} +void PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + //std::cout << "Adding int assignment for " << variable << std::endl; + this->state->assignedLocalIntegerVariables_.add(variable, variable); + mapping[variable] = Assignment(variable, value); +} +void PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + //std::cout << "Adding bool assignment for " << variable << std::endl; + this->state->assignedLocalBooleanVariables_.add(variable, variable); + mapping[variable] = Assignment(variable, value); +} +Module PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map& mapping) { + this->state->moduleNames_.add(name, name); + Module* old = this->state->moduleMap_.find(oldname); + if (old == nullptr) { + LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!"); + throw "Renaming module failed"; + } + Module res(*old, name, mapping, this->state); + this->state->moduleMap_.at(name) = res; + return res; +} +Module PrismGrammar::createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands) { + this->state->moduleNames_.add(name, name); + Module res(name, bools, ints, boolids, intids, commands); + this->state->moduleMap_.at(name) = res; + return res; +} + +void PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids) { + //std::cout << "Creating int " << name << " = " << init << std::endl; + uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper); + vars.emplace_back(id, name, lower, upper, init); + varids[name] = id; + this->state->localIntegerVariables_.add(name, name); +} +void PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids) { + //std::cout << "Creating bool " << name << std::endl; + uint_fast64_t id = this->state->addBooleanVariable(name); + vars.emplace_back(id, name, init); + varids[name] = id; + this->state->localBooleanVariables_.add(name, name); +} + +StateReward createStateReward(std::shared_ptr guard, std::shared_ptr reward) { + return StateReward(guard, reward); +} +TransitionReward createTransitionReward(std::string label, std::shared_ptr guard, std::shared_ptr reward) { + return TransitionReward(label, guard, reward); +} +void createRewardModel(std::string name, std::vector& stateRewards, std::vector& transitionRewards, std::map& mapping) { + mapping[name] = RewardModel(name, stateRewards, transitionRewards); +} +Update createUpdate(std::shared_ptr likelihood, std::map& bools, std::map ints) { + return Update(likelihood, bools, ints); +} +Command createCommand(std::string& label, std::shared_ptr guard, std::vector& updates) { + return Command(label, guard, updates); +} +Program createProgram( + Program::ModelType modelType, + std::map> undefBoolConst, + std::map> undefIntConst, + std::map> undefDoubleConst, + std::vector modules, + std::map rewards, + std::map> labels) { + return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels); +} + +PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) { + + labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";")) + [phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)]; + labelDefinition.name("label declaration"); + labelDefinitionList %= *labelDefinition(qi::_r1); + labelDefinitionList.name("label declaration list"); + + // This block defines all entities that are needed for parsing a reward model. + stateRewardDefinition = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)]; + stateRewardDefinition.name("state reward definition"); + transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)]; + transitionRewardDefinition.name("transition reward definition"); + rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards")) + [phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)]; + rewardDefinition.name("reward definition"); + rewardDefinitionList = *rewardDefinition(qi::_r1); + rewardDefinitionList.name("reward definition list"); + + commandName %= this->state->commandNames_; + commandName.name("command name"); + unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; + unassignedLocalBooleanVariableName.name("unassigned local boolean variable"); + unassignedLocalIntegerVariableName %= this->state->localIntegerVariables_ - this->state->assignedLocalIntegerVariables_; + unassignedLocalIntegerVariableName.name("unassigned local integer variable"); + + // This block defines all entities that are needed for parsing a single command. + assignmentDefinition = + (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntAssignment, this, qi::_1, qi::_2, qi::_r2)] | + (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBoolAssignment, this, qi::_1, qi::_2, qi::_r1)]; + assignmentDefinition.name("assignment"); + assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; + assignmentDefinitionList.name("assignment list"); + updateDefinition = ( + ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; + updateDefinition.name("update"); + updateListDefinition = +updateDefinition % "+"; + updateListDefinition.name("update list"); + commandDefinition = ( + qi::lit("[") > -( + (FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] + ) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";") + )[qi::_val = phoenix::bind(&createCommand, qi::_a, qi::_2, qi::_3)]; + commandDefinition.name("command"); + + // This block defines all entities that are needed for parsing variable definitions. + booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + [ + phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2) + ]; + booleanVariableDefinition.name("boolean variable declaration"); + + integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + [ + phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2) + ]; + integerVariableDefinition.name("integer variable declaration"); + variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); + variableDefinition.name("variable declaration"); + + // This block defines all entities that are needed for parsing a module. + moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::startModule, *this->state)] + >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) + [qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; + + moduleDefinition.name("module"); + moduleRenaming = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") + > this->state->moduleNames_ > qi::lit("[") > *( + (IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] + ) > qi::lit("]") > qi::lit("endmodule")) + [qi::_val = phoenix::bind(&PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)]; + moduleRenaming.name("renamed module"); + moduleDefinitionList %= +(moduleDefinition | moduleRenaming); + moduleDefinitionList.name("module list"); + + // This block defines all entities that are needed for parsing constant definitions. + definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedBooleanConstantDefinition.name("defined boolean constant declaration"); + definedIntegerConstantDefinition = ( + qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> + ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";") + )[ qi::_val = phoenix::bind(&PrismGrammar::addIntegerConstant, this, qi::_1, qi::_2) ]; + definedIntegerConstantDefinition.name("defined integer constant declaration"); + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedDoubleConstantDefinition.name("defined double constant declaration"); + undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; + undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); + undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; + undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); + undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; + undefinedDoubleConstantDefinition.name("undefined double constant declaration"); + definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + definedConstantDefinition.name("defined constant declaration"); + undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); + undefinedConstantDefinition.name("undefined constant declaration"); + constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); + constantDefinitionList.name("constant declaration list"); + + // This block defines all entities that are needed for parsing a program. + modelTypeDefinition = modelType_; + modelTypeDefinition.name("model type"); + start = ( + modelTypeDefinition > + constantDefinitionList(qi::_a, qi::_b, qi::_c) > + moduleDefinitionList > + rewardDefinitionList(qi::_d) > + labelDefinitionList(qi::_e) + )[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; + start.name("probabilistic program declaration"); +} + +void PrismGrammar::prepareForSecondRun() { + LOG4CPLUS_INFO(logger, "Preparing parser for second run."); + this->state->prepareForSecondRun(); + BooleanExpressionGrammar::secondRun(); + ConstBooleanExpressionGrammar::secondRun(); + ConstDoubleExpressionGrammar::secondRun(); + ConstIntegerExpressionGrammar::secondRun(); + IntegerExpressionGrammar::secondRun(); +} + +void PrismGrammar::resetGrammars() { + LOG4CPLUS_INFO(logger, "Resetting grammars."); + BooleanExpressionGrammar::resetInstance(); + ConstBooleanExpressionGrammar::resetInstance(); + ConstDoubleExpressionGrammar::resetInstance(); + ConstIntegerExpressionGrammar::resetInstance(); + IntegerExpressionGrammar::resetInstance(); +} + +} // namespace prism +} // namespace parser +} // namespace storm diff --git a/src/parser/PrismParser/PrismGrammar.h b/src/parser/PrismParser/PrismGrammar.h new file mode 100644 index 000000000..97033f506 --- /dev/null +++ b/src/parser/PrismParser/PrismGrammar.h @@ -0,0 +1,142 @@ +/* + * File: PrismGrammar.h + * Author: nafur + * + * Created on April 30, 2013, 5:20 PM + */ + +#ifndef PRISMGRAMMAR_H +#define PRISMGRAMMAR_H + +// All classes of the intermediate representation are used. +#include "src/ir/IR.h" +#include "src/parser/PrismParser/Includes.h" +#include "src/parser/PrismParser/Tokens.h" +#include "src/parser/PrismParser/IdentifierGrammars.h" +#include "src/parser/PrismParser/VariableState.h" +#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" +#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" +#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" +#include "src/parser/PrismParser/BooleanExpressionGrammar.h" +#include "src/parser/PrismParser/IntegerExpressionGrammar.h" + +// Used for file input. +#include +#include + +namespace storm { +namespace parser { +namespace prism { + +using namespace storm::ir; +using namespace storm::ir::expressions; + +/*! + * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of + * the input that complies with the PRISM syntax. + */ +class PrismGrammar : public qi::grammar< + Iterator, + Program(), + qi::locals< + std::map>, + std::map>, + std::map>, + std::map, + std::map> + >, + Skipper> { +public: + PrismGrammar(); + void prepareForSecondRun(); + void resetGrammars(); + +private: + + std::shared_ptr state; + + // The starting point of the grammar. + qi::rule< + Iterator, + Program(), + qi::locals< + std::map>, + std::map>, + std::map>, + std::map, + std::map> + >, + Skipper> start; + qi::rule modelTypeDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; + qi::rule(), Skipper> moduleDefinitionList; + + // Rules for module definition. + qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; + qi::rule>, Skipper> moduleRenaming; + + // Rules for variable definitions. + qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> booleanVariableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; + + // Rules for command definitions. + qi::rule, Skipper> commandDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule, std::map>, Skipper> updateDefinition; + qi::rule&, std::map&), Skipper> assignmentDefinitionList; + qi::rule&, std::map&), Skipper> assignmentDefinition; + + // Rules for variable/command names. + qi::rule commandName; + qi::rule unassignedLocalBooleanVariableName; + qi::rule unassignedLocalIntegerVariableName; + + // Rules for reward definitions. + qi::rule&), Skipper> rewardDefinitionList; + qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; + + // Rules for label definitions. + qi::rule>&), Skipper> labelDefinitionList; + qi::rule>&), Skipper> labelDefinition; + + // Rules for constant definitions. + qi::rule(), Skipper> constantDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; + qi::rule(), Skipper> definedConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; + qi::rule(), Skipper> definedBooleanConstantDefinition; + qi::rule(), Skipper> definedIntegerConstantDefinition; + qi::rule(), Skipper> definedDoubleConstantDefinition; + + // Rules for variable recognition. + qi::rule(), Skipper> booleanVariableCreatorExpression; + qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; + + storm::parser::prism::keywordsStruct keywords_; + storm::parser::prism::modelTypeStruct modelType_; + storm::parser::prism::relationalOperatorStruct relations_; + + std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value); + void addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping); + void addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + void addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + Module renameModule(const std::string& name, const std::string& oldname, std::map& mapping); + Module createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands); + + void createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids); + void createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids); +}; + + +} // namespace prism +} // namespace parser +} // namespace storm + + +#endif /* PRISMGRAMMAR_H */ + diff --git a/src/parser/PrismParser/Tokens.h b/src/parser/PrismParser/Tokens.h new file mode 100644 index 000000000..bd246d358 --- /dev/null +++ b/src/parser/PrismParser/Tokens.h @@ -0,0 +1,70 @@ +/* + * File: Tokens.h + * Author: nafur + * + * Created on April 19, 2013, 11:17 PM + */ + +#ifndef TOKENS_H +#define TOKENS_H + +namespace storm { +namespace parser { +namespace prism { + + + // A structure mapping the textual representation of a model type to the model type + // representation of the intermediate representation. + struct modelTypeStruct : qi::symbols { + modelTypeStruct() { + add + ("dtmc", Program::ModelType::DTMC) + ("ctmc", Program::ModelType::CTMC) + ("mdp", Program::ModelType::MDP) + ("ctmdp", Program::ModelType::CTMDP) + ; + } + }; + + + // A structure defining the keywords that are not allowed to be chosen as identifiers. + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("dtmc", 1) + ("ctmc", 2) + ("mdp", 3) + ("ctmdp", 4) + ("const", 5) + ("int", 6) + ("bool", 7) + ("module", 8) + ("endmodule", 9) + ("rewards", 10) + ("endrewards", 11) + ("true", 12) + ("false", 13) + ; + } + }; + + // A structure mapping the textual representation of a binary relation to the representation + // of the intermediate representation. + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + ("=", BinaryRelationExpression::EQUAL) + ("!=", BinaryRelationExpression::NOT_EQUAL) + ("<", BinaryRelationExpression::LESS) + ("<=", BinaryRelationExpression::LESS_OR_EQUAL) + (">", BinaryRelationExpression::GREATER) + (">=", BinaryRelationExpression::GREATER_OR_EQUAL) + ; + } + }; +} +} +} + +#endif /* TOKENS_H */ + diff --git a/src/parser/PrismParser/VariableState.cpp b/src/parser/PrismParser/VariableState.cpp new file mode 100644 index 000000000..e9be69435 --- /dev/null +++ b/src/parser/PrismParser/VariableState.cpp @@ -0,0 +1,171 @@ +#include "VariableState.h" + +namespace storm { +namespace parser { +namespace prism { + +using namespace storm::ir; +using namespace storm::ir::expressions; + +template +struct SymbolDump { + SymbolDump(std::ostream& out) : out(out) {} + void operator() (std::basic_string s, T elem) { + this->out << "\t" << s << " -> " << elem << std::endl; + } +private: + std::ostream& out; +}; +template +std::ostream& operator<<(std::ostream& out, qi::symbols& symbols) { + out << "Dumping symbol table" << std::endl; + SymbolDump dump(out); + symbols.for_each(dump); + return out; +} +std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& symbols) { + SymbolDump dump(out); + symbols.for_each(dump); + return out; +} + + +VariableState::VariableState(bool firstRun) + : firstRun(firstRun), keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) { +} + +uint_fast64_t VariableState::addBooleanVariable(const std::string& name) { + if (firstRun) { + std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); + LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextBooleanVariableIndex); + this->booleanVariables_.add(name, varExpr); + this->booleanVariableNames_.add(name, name); + this->nextBooleanVariableIndex++; + return varExpr->getVariableIndex(); + } else { + std::shared_ptr res = this->booleanVariables_.at(name); + if (res != nullptr) { + return res->getVariableIndex(); + } else { + LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " was not created in first run."); + return 0; + } + } +} + +uint_fast64_t VariableState::addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper) { + if (firstRun) { + std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper)); + LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextIntegerVariableIndex); + this->integerVariables_.add(name, varExpr); + this->integerVariableNames_.add(name, name); + this->nextIntegerVariableIndex++; + return varExpr->getVariableIndex(); + } else { + std::shared_ptr res = this->integerVariables_.at(name); + if (res != nullptr) { + return res->getVariableIndex(); + } else { + + LOG4CPLUS_ERROR(logger, "Integer variable " << name << " was not created in first run."); + return 0; + } + } +} + +std::shared_ptr VariableState::getBooleanVariable(const std::string& name) { + std::shared_ptr* res = this->booleanVariables_.find(name); + if (res != nullptr) { + return *res; + } else { + if (firstRun) { + LOG4CPLUS_TRACE(logger, "Getting boolean variable " << name << ", was not yet created."); + return std::shared_ptr(new VariableExpression(BaseExpression::bool_, std::numeric_limits::max(), "bool", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); + } else { + LOG4CPLUS_ERROR(logger, "Getting boolean variable " << name << ", but was not found. This variable does not exist."); + return std::shared_ptr(nullptr); + } + } +} + +std::shared_ptr VariableState::getIntegerVariable(const std::string& name) { + std::shared_ptr* res = this->integerVariables_.find(name); + if (res != nullptr) { + return *res; + } else { + if (firstRun) { + LOG4CPLUS_TRACE(logger, "Getting integer variable " << name << ", was not yet created."); + return std::shared_ptr(new VariableExpression(BaseExpression::int_, std::numeric_limits::max(), "int", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); + } else { + LOG4CPLUS_ERROR(logger, "Getting integer variable " << name << ", but was not found. This variable does not exist."); + return std::shared_ptr(nullptr); + } + } +} +std::shared_ptr VariableState::getVariable(const std::string& name) { + std::shared_ptr* res = this->integerVariables_.find(name); + if (res != nullptr) { + return *res; + } else { + res = this->booleanVariables_.find(name); + if (res != nullptr) { + return *res; + } else { + return std::shared_ptr(nullptr); + } + } +} + +void VariableState::performRenaming(const std::map& renaming) { + for (auto it: renaming) { + std::shared_ptr* original = this->integerVariables_.find(it.first); + if (original != nullptr) { + std::shared_ptr* next = this->integerVariables_.find(it.second); + if (next == nullptr) { + this->addIntegerVariable(it.second, (*original)->getLowerBound(), (*original)->getUpperBound()); + } + } + original = this->booleanVariables_.find(it.first); + if (original != nullptr) { + if (this->booleanVariables_.find(it.second) == nullptr) { + this->addBooleanVariable(it.second); + } + } + std::string* oldCmdName = this->commandNames_.find(it.first); + if (oldCmdName != nullptr) { + LOG4CPLUS_TRACE(logger, "Adding new command name " << it.second << " due to module renaming."); + this->commandNames_.at(it.second) = it.second; + } + } +} + +void VariableState::startModule() { + this->localBooleanVariables_.clear(); + this->localIntegerVariables_.clear(); +} + +bool VariableState::isFreeIdentifier(std::string& s) const { + if (this->integerVariableNames_.find(s) != nullptr) return false; + if (this->allConstantNames_.find(s) != nullptr) return false; + if (this->labelNames_.find(s) != nullptr) return false; + if (this->moduleNames_.find(s) != nullptr) return false; + if (this->keywords.find(s) != nullptr) return false; + return true; +} +bool VariableState::isIdentifier(std::string& s) const { + if (this->allConstantNames_.find(s) != nullptr) return false; + if (this->keywords.find(s) != nullptr) return false; + return true; +} + +void VariableState::prepareForSecondRun() { + integerConstants_.clear(); + booleanConstants_.clear(); + doubleConstants_.clear(); + allConstantNames_.clear(); + this->firstRun = false; +} + +} +} +} diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h new file mode 100644 index 000000000..620c029ff --- /dev/null +++ b/src/parser/PrismParser/VariableState.h @@ -0,0 +1,71 @@ +/* + * File: VariableState.h + * Author: nafur + * + * Created on April 10, 2013, 4:43 PM + */ + +#ifndef VARIABLESTATE_H +#define VARIABLESTATE_H + +#include "src/ir/IR.h" +#include "Includes.h" +#include "Tokens.h" +#include + +namespace storm { +namespace parser { +namespace prism { + +using namespace storm::ir; +using namespace storm::ir::expressions; + +template +std::ostream& operator<<(std::ostream& out, qi::symbols& symbols); + +struct VariableState : public storm::ir::VariableAdder { + +public: + VariableState(bool firstRun = true); + +public: + bool firstRun; + keywordsStruct keywords; + + // Used for indexing the variables. + uint_fast64_t nextBooleanVariableIndex; + uint_fast64_t nextIntegerVariableIndex; + + // Structures mapping variable and constant names to the corresponding expression nodes of + // the intermediate representation. + struct qi::symbols> integerVariables_, booleanVariables_; + struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; + struct qi::symbols moduleMap_; + + // A structure representing the identity function over identifier names. + struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, + localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; +public: + uint_fast64_t addBooleanVariable(const std::string& name); + uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper); + + std::shared_ptr getBooleanVariable(const std::string& name); + std::shared_ptr getIntegerVariable(const std::string& name); + std::shared_ptr getVariable(const std::string& name); + + void performRenaming(const std::map& renaming); + + void startModule(); + + bool isFreeIdentifier(std::string& s) const; + bool isIdentifier(std::string& s) const; + + void prepareForSecondRun(); +}; + +} +} +} + +#endif /* VARIABLESTATE_H */ + diff --git a/src/storm.cpp b/src/storm.cpp index f02783319..d60700018 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -27,6 +27,7 @@ #include "src/modelchecker/GmmxxMdpPrctlModelChecker.h" #include "src/parser/AutoParser.h" #include "src/parser/PrctlParser.h" +#include "src/solver/GraphAnalyzer.h" #include "src/utility/Settings.h" #include "src/utility/ErrorHandling.h" #include "src/formula/Prctl.h" @@ -38,8 +39,26 @@ #include "log4cplus/consoleappender.h" #include "log4cplus/fileappender.h" +#include "src/parser/PrismParser.h" +#include "src/adapters/ExplicitModelAdapter.h" +#include "src/adapters/SymbolicModelAdapter.h" + #include "src/exceptions/InvalidSettingsException.h" +#include +#include +#include +#include + +void printUsage() { + struct rusage ru; + getrusage(RUSAGE_SELF, &ru); + + std::cout << "Memory Usage: " << ru.ru_maxrss << "kB" << std::endl; + std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl; +} + + log4cplus::Logger logger; /*! @@ -118,7 +137,12 @@ bool parseOptions(const int argc, const char* argv[]) { if (s->isSet("debug")) { logger.setLogLevel(log4cplus::DEBUG_LOG_LEVEL); logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::DEBUG_LOG_LEVEL); - LOG4CPLUS_DEBUG(logger, "Enable very verbose mode, log output gets printed to console."); + LOG4CPLUS_INFO(logger, "Enable very verbose mode, log output gets printed to console."); + } + if (s->isSet("trace")) { + logger.setLogLevel(log4cplus::TRACE_LOG_LEVEL); + logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::TRACE_LOG_LEVEL); + LOG4CPLUS_INFO(logger, "Enable trace mode, log output gets printed to console."); } if (s->isSet("logfile")) { setUpFileLogging(); @@ -134,7 +158,7 @@ void setUp() { * Function to perform some cleanup. */ void cleanUp() { - // nothing here + delete storm::utility::cuddUtilityInstance(); } /*! diff --git a/src/utility/CuddUtility.cpp b/src/utility/CuddUtility.cpp new file mode 100644 index 000000000..ab3d85797 --- /dev/null +++ b/src/utility/CuddUtility.cpp @@ -0,0 +1,195 @@ +/* + * CuddUtility.cpp + * + * Created on: 26.01.2013 + * Author: Christian Dehnert + */ + +#include "CuddUtility.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +#include +#include + +namespace storm { + +namespace utility { + +storm::utility::CuddUtility* storm::utility::CuddUtility::instance = nullptr; + +ADD* CuddUtility::getNewAddVariable() { + ADD* result = new ADD(manager.addVar()); + allDecisionDiagramVariables.push_back(result); + return result; +} + +ADD* CuddUtility::getAddVariable(int index) const { + return new ADD(manager.addVar(index)); +} + +ADD* CuddUtility::getOne() const { + return new ADD(manager.addOne()); +} + +ADD* CuddUtility::getZero() const { + return new ADD(manager.addZero()); +} + +ADD* CuddUtility::getConstantEncoding(uint_fast64_t constant, std::vector const& variables) const { + if ((constant >> variables.size()) != 0) { + LOG4CPLUS_ERROR(logger, "Cannot create encoding for constant " << constant << " with " + << variables.size() << " variables."); + throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" + << " for constant " << constant << " with " << variables.size() + << " variables."; + } + + // Determine whether the new ADD will be rooted by the first variable or its complement. + ADD initialNode; + if ((constant & (1 << (variables.size() - 1))) != 0) { + initialNode = *variables[0]; + } else { + initialNode = ~(*variables[0]); + } + ADD* result = new ADD(initialNode); + + // Add (i.e. multiply) the other variables as well according to whether their bit is set or not. + for (uint_fast64_t i = 1; i < variables.size(); ++i) { + if ((constant & (1 << (variables.size() - i - 1))) != 0) { + *result *= *variables[i]; + } else { + *result *= ~(*variables[i]); + } + } + + return result; +} + +void CuddUtility::setValueAtIndex(ADD* add, uint_fast64_t index, std::vector const& variables, double value) const { + if ((index >> variables.size()) != 0) { + LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << index << " with " + << variables.size() << " variables."); + throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" + << " for index " << index << " with " << variables.size() + << " variables."; + } + + // Determine whether the new ADD will be rooted by the first variable or its complement. + ADD initialNode; + if ((index & (1 << (variables.size() - 1))) != 0) { + initialNode = *variables[0]; + } else { + initialNode = ~(*variables[0]); + } + ADD* encoding = new ADD(initialNode); + + // Add (i.e. multiply) the other variables as well according to whether their bit is set or not. + for (uint_fast64_t i = 1; i < variables.size(); ++i) { + if ((index & (1 << (variables.size() - i - 1))) != 0) { + *encoding *= *variables[i]; + } else { + *encoding *= ~(*variables[i]); + } + } + + *add = encoding->Ite(manager.constant(value), *add); +} + +void CuddUtility::setValueAtIndices(ADD* add, uint_fast64_t rowIndex, uint_fast64_t columnIndex, std::vector const& rowVariables, std::vector const& columnVariables, double value) const { + if ((rowIndex >> rowVariables.size()) != 0) { + LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << rowIndex << " with " + << rowVariables.size() << " variables."); + throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" + << " for index " << rowIndex << " with " << rowVariables.size() + << " variables."; + } + if ((columnIndex >> columnVariables.size()) != 0) { + LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << columnIndex << " with " + << columnVariables.size() << " variables."); + throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" + << " for index " << columnIndex << " with " << columnVariables.size() + << " variables."; + } + if (rowVariables.size() != columnVariables.size()) { + LOG4CPLUS_ERROR(logger, "Number of variables for indices encodings does not match."); + throw storm::exceptions::InvalidArgumentException() + << "Number of variables for indices encodings does not match."; + } + + ADD initialNode; + if ((rowIndex & (1 << (rowVariables.size() - 1))) != 0) { + initialNode = *rowVariables[0]; + } else { + initialNode = ~(*rowVariables[0]); + } + ADD* encoding = new ADD(initialNode); + if ((columnIndex & (1 << (rowVariables.size() - 1))) != 0) { + *encoding *= *columnVariables[0]; + } else { + *encoding *= ~(*columnVariables[0]); + } + + for (uint_fast64_t i = 1; i < rowVariables.size(); ++i) { + if ((rowIndex & (1 << (rowVariables.size() - i - 1))) != 0) { + *encoding *= *rowVariables[i]; + } else { + *encoding *= ~(*rowVariables[i]); + } + if ((columnIndex & (1 << (columnVariables.size() - i - 1))) != 0) { + *encoding *= *columnVariables[i]; + } else { + *encoding *= ~(*columnVariables[i]); + } + } + + *add = encoding->Ite(manager.constant(value), *add); +} + + +ADD* CuddUtility::getConstant(double value) const { + return new ADD(manager.constant(value)); +} + +ADD* CuddUtility::permuteVariables(ADD* add, std::vector fromVariables, std::vector toVariables, uint_fast64_t totalNumberOfVariables) const { + std::vector permutation; + permutation.resize(totalNumberOfVariables); + for (uint_fast64_t i = 0; i < totalNumberOfVariables; ++i) { + permutation[i] = i; + } + for (uint_fast64_t i = 0; i < fromVariables.size(); ++i) { + permutation[fromVariables[i]->NodeReadIndex()] = toVariables[i]->NodeReadIndex(); + } + return new ADD(add->Permute(&permutation[0])); +} + +void CuddUtility::dumpDotToFile(ADD* add, std::string filename) const { + std::vector nodes; + nodes.push_back(*add); + + FILE* filePtr; + filePtr = fopen(filename.c_str(), "w"); + manager.DumpDot(nodes, 0, 0, filePtr); + fclose(filePtr); +} + +Cudd const& CuddUtility::getManager() const { + return manager; +} + +CuddUtility* cuddUtilityInstance() { + if (CuddUtility::instance == nullptr) { + CuddUtility::instance = new CuddUtility(); + } + return CuddUtility::instance; +} + +} // namespace utility + +} // namespace storm + + diff --git a/src/utility/CuddUtility.h b/src/utility/CuddUtility.h new file mode 100644 index 000000000..8102eb012 --- /dev/null +++ b/src/utility/CuddUtility.h @@ -0,0 +1,63 @@ +/* + * CuddUtility.h + * + * Created on: 26.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_UTILITY_CUDDUTILITY_H_ +#define STORM_UTILITY_CUDDUTILITY_H_ + +#include "cuddObj.hh" + +namespace storm { + +namespace utility { + +class CuddUtility { +public: + ~CuddUtility() { + for (auto element : allDecisionDiagramVariables) { + delete element; + } + } + + ADD* getNewAddVariable(); + ADD* getAddVariable(int index) const; + + ADD* getOne() const; + ADD* getZero() const; + + ADD* getConstantEncoding(uint_fast64_t constant, std::vector const& variables) const; + + void setValueAtIndex(ADD* add, uint_fast64_t index, std::vector const& variables, double value) const; + void setValueAtIndices(ADD* add, uint_fast64_t rowIndex, uint_fast64_t columnIndex, std::vector const& rowVariables, std::vector const& columnVariables, double value) const; + + ADD* getConstant(double value) const; + + ADD* permuteVariables(ADD* add, std::vector fromVariables, std::vector toVariables, uint_fast64_t totalNumberOfVariables) const; + + void dumpDotToFile(ADD* add, std::string filename) const; + + Cudd const& getManager() const; + + friend CuddUtility* cuddUtilityInstance(); + +private: + CuddUtility() : manager(), allDecisionDiagramVariables() { + + } + + Cudd manager; + std::vector allDecisionDiagramVariables; + + static CuddUtility* instance; +}; + +CuddUtility* cuddUtilityInstance(); + +} // namespace utility + +} // namespace storm + +#endif /* STORM_UTILITY_CUDDUTILITY_H_ */ diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 9c2688f58..ae0db6f4b 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -132,6 +132,7 @@ void Settings::initDescriptions() { ("help,h", "produce help message") ("verbose,v", "be verbose") ("debug", "be very verbose, intended for debugging") + ("trace", "be extremely verbose, expect lots of output") ("logfile,l", bpo::value(), "name of the log file") ("configfile,c", bpo::value(), "name of config file") ("trafile", bpo::value()->required(), "name of the .tra file") diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp index b19335fdd..55da2ae32 100644 --- a/test/parser/ParseMdpTest.cpp +++ b/test/parser/ParseMdpTest.cpp @@ -21,7 +21,7 @@ TEST(ParseMdpTest, parseAndOutput) { ASSERT_EQ(mdp->getNumberOfStates(), (uint_fast64_t)3); ASSERT_EQ(mdp->getNumberOfTransitions(), (uint_fast64_t)11); - ASSERT_EQ(matrix->getRowCount(), (uint_fast64_t)2 * 3); + ASSERT_EQ(matrix->getRowCount(), (uint_fast64_t)(2 * 3)); ASSERT_EQ(matrix->getColumnCount(), (uint_fast64_t)3); diff --git a/test/parser/ParsePrismTest.cpp b/test/parser/ParsePrismTest.cpp new file mode 100644 index 000000000..b4155edfd --- /dev/null +++ b/test/parser/ParsePrismTest.cpp @@ -0,0 +1,32 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/PrismParser.h" +#include "src/utility/IoUtility.h" +#include "src/ir/Program.h" +#include "src/adapters/ExplicitModelAdapter.h" +#include "src/models/Mdp.h" + +TEST(ParsePrismTest, parseCrowds5_5) { + storm::parser::PrismParser parser; + storm::ir::Program program; + ASSERT_NO_THROW(program = parser.parseFile("examples/dtmc/crowds/crowds5_5.pm")); + storm::adapters::ExplicitModelAdapter adapter(program); + + std::shared_ptr> model = adapter.getModel()->as>(); + + ASSERT_EQ(model->getNumberOfStates(), (uint_fast64_t)8607); + ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)15113); +} + +TEST(ParsePrismTest, parseTwoDice) { + storm::parser::PrismParser parser; + storm::ir::Program program; + ASSERT_NO_THROW(program = parser.parseFile("examples/mdp/two_dice/two_dice.nm")); + storm::adapters::ExplicitModelAdapter adapter(program); + + std::shared_ptr> model = adapter.getModel()->as>(); + + ASSERT_EQ(model->getNumberOfStates(), (uint_fast64_t)169); + ASSERT_EQ(model->getNumberOfChoices(), (uint_fast64_t)254); + ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)436); +}