From 7660a6c9f8ef637bc759499961f835cc7d738a7a Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 27 Jan 2018 14:33:00 +0100 Subject: [PATCH 01/29] dont check != 0 in templated code --- src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 10311c2a2..dce686091 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -1244,7 +1244,7 @@ namespace storm { // Now insert all (cumulative) probability values that target an MEC. for (uint_fast64_t mecIndex = 0; mecIndex < auxiliaryStateToProbabilityMap.size(); ++mecIndex) { - if (auxiliaryStateToProbabilityMap[mecIndex] != 0) { + if (!storm::utility::isZero(auxiliaryStateToProbabilityMap[mecIndex])) { sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + mecIndex, auxiliaryStateToProbabilityMap[mecIndex]); } } @@ -1279,7 +1279,7 @@ namespace storm { // Now insert all (cumulative) probability values that target an MEC. for (uint_fast64_t targetMecIndex = 0; targetMecIndex < auxiliaryStateToProbabilityMap.size(); ++targetMecIndex) { - if (auxiliaryStateToProbabilityMap[targetMecIndex] != 0) { + if (!storm::utility::isZero(auxiliaryStateToProbabilityMap[targetMecIndex])) { sspMatrixBuilder.addNextValue(currentChoice, firstAuxiliaryStateIndex + targetMecIndex, auxiliaryStateToProbabilityMap[targetMecIndex]); } } @@ -1659,7 +1659,6 @@ namespace storm { template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponent(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponentVI(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponentLP(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); - #endif } } From 1e4b81812cc40aedd022a2ce5a37afbb3af8dc07 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 29 May 2018 16:47:39 +0200 Subject: [PATCH 02/29] Environment does no longer require that unused setting modules still have to be registered. --- src/storm/environment/SubEnvironment.cpp | 19 ++++++++++++++++--- src/storm/environment/SubEnvironment.h | 4 ++-- 2 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp index 920a06049..5226fdca4 100644 --- a/src/storm/environment/SubEnvironment.cpp +++ b/src/storm/environment/SubEnvironment.cpp @@ -16,31 +16,44 @@ namespace storm { template - SubEnvironment::SubEnvironment() : subEnv(std::make_unique()) { + SubEnvironment::SubEnvironment() : subEnv(nullptr) { // Intentionally left empty } template - SubEnvironment::SubEnvironment(SubEnvironment const& other) : subEnv(new EnvironmentType(*other.subEnv)) { + SubEnvironment::SubEnvironment(SubEnvironment const& other) : subEnv(other.subEnv ? new EnvironmentType(*other.subEnv) : nullptr) { // Intentionally left empty } template SubEnvironment& SubEnvironment::operator=(SubEnvironment const& other) { - subEnv = std::make_unique(*other.subEnv); + if (other.subEnv) { + subEnv = std::make_unique(*other.subEnv); + } else { + subEnv.reset(); + } return *this; } template EnvironmentType const& SubEnvironment::get() const { + assertInitialized(); return *subEnv; } template EnvironmentType& SubEnvironment::get() { + assertInitialized(); return *subEnv; } + template + void SubEnvironment::assertInitialized() const { + if (!subEnv) { + subEnv = std::make_unique(); + } + } + template class SubEnvironment; template class SubEnvironment; diff --git a/src/storm/environment/SubEnvironment.h b/src/storm/environment/SubEnvironment.h index 2b6ecbf87..b1858936d 100644 --- a/src/storm/environment/SubEnvironment.h +++ b/src/storm/environment/SubEnvironment.h @@ -16,8 +16,8 @@ namespace storm { EnvironmentType& get(); private: - std::unique_ptr subEnv; + void assertInitialized() const; + mutable std::unique_ptr subEnv; }; } - From 99e561995208116cfa7c7f65216b8b14932a68dd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 28 May 2018 17:33:05 +0200 Subject: [PATCH 03/29] Export storm targets --- CMakeLists.txt | 2 ++ src/storm-cli-utilities/CMakeLists.txt | 2 +- src/storm-dft-cli/CMakeLists.txt | 2 +- src/storm-dft/CMakeLists.txt | 2 +- src/storm-gspn-cli/CMakeLists.txt | 2 +- src/storm-gspn/CMakeLists.txt | 2 +- src/storm-pars-cli/CMakeLists.txt | 2 +- src/storm-pars/CMakeLists.txt | 2 +- src/storm-pgcl-cli/CMakeLists.txt | 2 +- src/storm-pgcl/CMakeLists.txt | 2 +- src/storm/CMakeLists.txt | 4 ++-- 11 files changed, 13 insertions(+), 11 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index d4c789dd7..43ddbd8e9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -500,4 +500,6 @@ add_subdirectory(src) include(export) +install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${CMAKE_INSTALL_DIR}) + include(StormCPackConfig.cmake) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt index 64c2848c7..84819b72b 100644 --- a/src/storm-cli-utilities/CMakeLists.txt +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -36,5 +36,5 @@ add_custom_target(copy_storm_cli_util_headers DEPENDS ${STORM_CLI_UTIL_OUTPUT_HE add_dependencies(storm-cli-utilities copy_storm_pars_headers) # installation -install(TARGETS storm-cli-utilities RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-cli-utilities EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt index 4780eef4d..5886ac0a0 100644 --- a/src/storm-dft-cli/CMakeLists.txt +++ b/src/storm-dft-cli/CMakeLists.txt @@ -6,4 +6,4 @@ set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft") add_dependencies(binaries storm-dft-cli) # installation -install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-dft-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index 9ec70aed2..f191e537f 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -36,5 +36,5 @@ add_custom_target(copy_storm_dft_headers DEPENDS ${STORM_DFT_OUTPUT_HEADERS} ${S add_dependencies(storm-dft copy_storm_dft_headers) # installation -install(TARGETS storm-dft RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-dft EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt index 39d656a4c..f06ff4a53 100644 --- a/src/storm-gspn-cli/CMakeLists.txt +++ b/src/storm-gspn-cli/CMakeLists.txt @@ -5,4 +5,4 @@ set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn") add_dependencies(binaries storm-gspn-cli) # installation -install(TARGETS storm-gspn-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-gspn-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt index cf80ff6aa..9312af543 100644 --- a/src/storm-gspn/CMakeLists.txt +++ b/src/storm-gspn/CMakeLists.txt @@ -15,4 +15,4 @@ set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES}) # installation -install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-gspn EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pars-cli/CMakeLists.txt b/src/storm-pars-cli/CMakeLists.txt index 9e2f6f315..955ee93c8 100644 --- a/src/storm-pars-cli/CMakeLists.txt +++ b/src/storm-pars-cli/CMakeLists.txt @@ -6,4 +6,4 @@ set_target_properties(storm-pars-cli PROPERTIES OUTPUT_NAME "storm-pars") add_dependencies(binaries storm-pars-cli) # installation -install(TARGETS storm-pars-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-pars-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pars/CMakeLists.txt b/src/storm-pars/CMakeLists.txt index 4e2ec1e0f..b91292be4 100644 --- a/src/storm-pars/CMakeLists.txt +++ b/src/storm-pars/CMakeLists.txt @@ -36,5 +36,5 @@ add_custom_target(copy_storm_pars_headers DEPENDS ${STORM_PARS_OUTPUT_HEADERS} $ add_dependencies(storm-pars copy_storm_pars_headers) # installation -install(TARGETS storm-pars RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm-pars EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pgcl-cli/CMakeLists.txt b/src/storm-pgcl-cli/CMakeLists.txt index 4f2799d4d..506772fd9 100644 --- a/src/storm-pgcl-cli/CMakeLists.txt +++ b/src/storm-pgcl-cli/CMakeLists.txt @@ -5,4 +5,4 @@ set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl") add_dependencies(binaries storm-pgcl-cli) # installation -install(TARGETS storm-pgcl-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-pgcl-cli EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm-pgcl/CMakeLists.txt b/src/storm-pgcl/CMakeLists.txt index e20a99483..059bff395 100644 --- a/src/storm-pgcl/CMakeLists.txt +++ b/src/storm-pgcl/CMakeLists.txt @@ -13,4 +13,4 @@ add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS}) target_link_libraries(storm-pgcl storm) # installation -install(TARGETS storm-pgcl RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) \ No newline at end of file +install(TARGETS storm-pgcl EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 0cf8d3183..6a8cda64e 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -72,7 +72,7 @@ add_dependencies(storm copy_resources_headers) add_dependencies(binaries storm-main) # installation -install(TARGETS storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib) -install(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) +install(TARGETS storm EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib) +install(TARGETS storm-main EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) install(DIRECTORY ${CMAKE_BINARY_DIR}/include/ DESTINATION include/storm FILES_MATCHING PATTERN "*.h") From c5e356bc40956c22c2e2c3b41d2bd1a0e1a055d9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 May 2018 16:50:30 +0200 Subject: [PATCH 04/29] Proper installation of Storm --- CMakeLists.txt | 10 ++++++++++ resources/cmake/macros/export.cmake | 20 ++++++++++++++++++-- resources/cmake/stormConfigVersion.cmake.in | 11 +++++++++++ 3 files changed, 39 insertions(+), 2 deletions(-) create mode 100644 resources/cmake/stormConfigVersion.cmake.in diff --git a/CMakeLists.txt b/CMakeLists.txt index 43ddbd8e9..8ca3b9b7e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -78,6 +78,14 @@ set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables") set(DEF_INSTALL_CMAKE_DIR "lib/CMake/storm") set(CMAKE_INSTALL_DIR ${DEF_INSTALL_CMAKE_DIR} CACHE PATH "Installation directory for CMake files") +# Add CMake install prefix +foreach(p LIB BIN INCLUDE CMAKE) + set(var ${p}_INSTALL_DIR) + if(NOT IS_ABSOLUTE "${${var}}") + set(${var} "${CMAKE_INSTALL_PREFIX}/${${var}}") + endif() +endforeach() + message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}") # If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version. @@ -500,6 +508,8 @@ add_subdirectory(src) include(export) +install(FILES ${CMAKE_BINARY_DIR}/stormConfig.install.cmake DESTINATION ${CMAKE_INSTALL_DIR} RENAME stormConfig.cmake) +install(FILES ${CMAKE_BINARY_DIR}/stormConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_DIR}) install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${CMAKE_INSTALL_DIR}) include(StormCPackConfig.cmake) diff --git a/resources/cmake/macros/export.cmake b/resources/cmake/macros/export.cmake index eb2e8fa84..606bde62f 100644 --- a/resources/cmake/macros/export.cmake +++ b/resources/cmake/macros/export.cmake @@ -8,7 +8,7 @@ message(STATUS "Registered with cmake") export(PACKAGE storm) set(DEP_TARGETS "") -foreach(dt ${STORM_DEP_TARGETS}) +foreach(dt ${STORM_DEP_TARGETS}) export_target(DEP_TARGETS ${dt}) endforeach() @@ -19,10 +19,26 @@ endforeach() include(CMakePackageConfigHelpers) +write_basic_package_version_file(${CMAKE_CURRENT_BINARY_DIR}/stormConfigVersion.cmake + VERSION 0.1.0 + COMPATIBILITY SameMajorVersion ) + +# For the build tree set(CONF_INCLUDE_DIRS "${CMAKE_BINARY_DIR}/include/") configure_package_config_file( resources/cmake/stormConfig.cmake.in ${PROJECT_BINARY_DIR}/stormConfig.cmake INSTALL_DESTINATION ${CMAKE_INSTALL_DIR} - PATH_VARS INCLUDE_INSTALL_DIR #SYSCONFIG_INSTALL_DIR + PATH_VARS INCLUDE_INSTALL_DIR +) + + # For the install tree +file(RELATIVE_PATH REL_INCLUDE_DIR "${CMAKE_INSTALL_DIR}" "${INCLUDE_INSTALL_DIR}") +set(CONF_INCLUDE_DIRS "\${storm_CMAKE_DIR}/${REL_INCLUDE_DIR}/storm") + +configure_package_config_file( + resources/cmake/stormConfig.cmake.in + ${PROJECT_BINARY_DIR}/stormConfig.install.cmake + INSTALL_DESTINATION ${CMAKE_INSTALL_DIR} + PATH_VARS INCLUDE_INSTALL_DIR ) diff --git a/resources/cmake/stormConfigVersion.cmake.in b/resources/cmake/stormConfigVersion.cmake.in new file mode 100644 index 000000000..d248393ad --- /dev/null +++ b/resources/cmake/stormConfigVersion.cmake.in @@ -0,0 +1,11 @@ +set(PACKAGE_VERSION "@storm_VERSION@") + +# Check whether the requested PACKAGE_FIND_VERSION is compatible +if("${PACKAGE_VERSION}" VERSION_LESS "${PACKAGE_FIND_VERSION}") + set(PACKAGE_VERSION_COMPATIBLE FALSE) +else() + set(PACKAGE_VERSION_COMPATIBLE TRUE) + if ("${PACKAGE_VERSION}" VERSION_EQUAL "${PACKAGE_FIND_VERSION}") + set(PACKAGE_VERSION_EXACT TRUE) + endif() +endif() From a2c990ea58707995aed1d331825302b46ef49df0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 6 Jun 2018 16:50:44 +0200 Subject: [PATCH 05/29] Travis: changed mail address for notifications --- .travis.yml | 2 +- travis/generate_travis.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index d6e942eec..1074ba368 100644 --- a/.travis.yml +++ b/.travis.yml @@ -25,7 +25,7 @@ notifications: on_failure: always on_success: change recipients: - secure: "Q9CW/PtyWkZwExDrfFFb9n1STGYsRfI6awv1bZHcGwfrDvhpXoMCuF8CwviIfilm7fFJJEoKizTtdRpY0HrOnY/8KY111xrtcFYosxdndv7xbESodIxQOUoIEFCO0mCNHwWYisoi3dAA7H3Yn661EsxluwHjzX5vY0xSbw0n229hlsFz092HwGLSU33zHl7eXpQk+BOFmBTRGlOq9obtDZ17zbHz1oXFZntHK/JDUIYP0b0uq8NvE2jM6CIVdcuSwmIkOhZJoO2L3Py3rBbPci+L2PSK4Smv2UjCPF8KusnOaFIyDB3LcNM9Jqq5ssJMrK/KaO6BiuYrOZXYWZ7KEg3Y/naC8HjOH1dzty+P7oW46sb9F03pTsufqD4R7wcK+9wROTztO6aJPDG/IPH7EWgrBTxqlOkVRwi2eYuQouZpZUW6EMClKbMHMIxCH2S8aOk/r1w2cNwmPEcunnP0nl413x/ByHr4fTPFykPj8pQxIsllYjpdWBRQfDOauKWGzk6LcrFW0qpWP+/aJ2vYu/IoZQMG5lMHbp6Y1Lg09pYm7Q983v3b7D+JvXhOXMyGq91HyPahA2wwKoG1GA4uoZ2I95/IFYNiKkelDd3WTBoFLNF9YFoEJNdCywm1fO2WY4WkyEFBuQcgDA+YpFMJJMxjTbivYk9jvHk2gji//2w=" + secure: "BoMQTBWnkh4ZLIHEaKu0tAKDohhVmOQ2pz/fjc+ScKG8mtvXqtpx0TiyePOUV1MuYNZiAP7x4mwABcoid55SwZ4+LPjd8uxXNfOji9B9GW5YqbqRvAeh7Es7dx48MyLYPIezjoryHH9R3Q2zZ9gmxgtw5eirjURcLNTXpKAwq/oOsKvh+vhOx4Qierw98wEXjMV7ipBzE4cfkgUbbX7oxGh1nsAsCew+rRmNLijfmE9tctYdH5W0wE+zC9ik+12Xyk3FwsDIABirPHfeCcEl+b9I0h1a2vZSZIA+sCDkIGKTiv9pCnsthn5LJc9pMLX7B/Wf6xLGMzpSiw3P1ZzjXpOE026WuyhTMVXqZYvbl7cJoNZiLCfTYg3MQVq5NHkq0h0jInIH7QlZYd0hZPOGONwdy17O1QmnX2Weq6G+Ps9siLVKFba37+y5PfRYkiUatJvDf2f7Jdxye6TWrUmlxQkAvs65ioyr8doad7IT1/yaGr/rBpXeQqZp6zNoMYr/cCRAYX6nOrnSszgiIWEc8QMMx+G31v77Uvd++9VG4MG9gbdpexpfYRNzKAxDarSaYEOuaWm2Z6R87bpNcjA+tW0hnBHBzRx0NFYYqXyW0tpVO9+035A9CHrLDLz77r4jJttcRvrP2rTbTBiwuhpmiufRyk3BuWlgzU3yaSuQV3M=" # # Configurations diff --git a/travis/generate_travis.py b/travis/generate_travis.py index ade78cbca..ac4e89417 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -61,7 +61,7 @@ if __name__ == "__main__": s += " on_failure: always\n" s += " on_success: change\n" s += " recipients:\n" - s += ' secure: "Q9CW/PtyWkZwExDrfFFb9n1STGYsRfI6awv1bZHcGwfrDvhpXoMCuF8CwviIfilm7fFJJEoKizTtdRpY0HrOnY/8KY111xrtcFYosxdndv7xbESodIxQOUoIEFCO0mCNHwWYisoi3dAA7H3Yn661EsxluwHjzX5vY0xSbw0n229hlsFz092HwGLSU33zHl7eXpQk+BOFmBTRGlOq9obtDZ17zbHz1oXFZntHK/JDUIYP0b0uq8NvE2jM6CIVdcuSwmIkOhZJoO2L3Py3rBbPci+L2PSK4Smv2UjCPF8KusnOaFIyDB3LcNM9Jqq5ssJMrK/KaO6BiuYrOZXYWZ7KEg3Y/naC8HjOH1dzty+P7oW46sb9F03pTsufqD4R7wcK+9wROTztO6aJPDG/IPH7EWgrBTxqlOkVRwi2eYuQouZpZUW6EMClKbMHMIxCH2S8aOk/r1w2cNwmPEcunnP0nl413x/ByHr4fTPFykPj8pQxIsllYjpdWBRQfDOauKWGzk6LcrFW0qpWP+/aJ2vYu/IoZQMG5lMHbp6Y1Lg09pYm7Q983v3b7D+JvXhOXMyGq91HyPahA2wwKoG1GA4uoZ2I95/IFYNiKkelDd3WTBoFLNF9YFoEJNdCywm1fO2WY4WkyEFBuQcgDA+YpFMJJMxjTbivYk9jvHk2gji//2w="\n' + s += ' secure: "BoMQTBWnkh4ZLIHEaKu0tAKDohhVmOQ2pz/fjc+ScKG8mtvXqtpx0TiyePOUV1MuYNZiAP7x4mwABcoid55SwZ4+LPjd8uxXNfOji9B9GW5YqbqRvAeh7Es7dx48MyLYPIezjoryHH9R3Q2zZ9gmxgtw5eirjURcLNTXpKAwq/oOsKvh+vhOx4Qierw98wEXjMV7ipBzE4cfkgUbbX7oxGh1nsAsCew+rRmNLijfmE9tctYdH5W0wE+zC9ik+12Xyk3FwsDIABirPHfeCcEl+b9I0h1a2vZSZIA+sCDkIGKTiv9pCnsthn5LJc9pMLX7B/Wf6xLGMzpSiw3P1ZzjXpOE026WuyhTMVXqZYvbl7cJoNZiLCfTYg3MQVq5NHkq0h0jInIH7QlZYd0hZPOGONwdy17O1QmnX2Weq6G+Ps9siLVKFba37+y5PfRYkiUatJvDf2f7Jdxye6TWrUmlxQkAvs65ioyr8doad7IT1/yaGr/rBpXeQqZp6zNoMYr/cCRAYX6nOrnSszgiIWEc8QMMx+G31v77Uvd++9VG4MG9gbdpexpfYRNzKAxDarSaYEOuaWm2Z6R87bpNcjA+tW0hnBHBzRx0NFYYqXyW0tpVO9+035A9CHrLDLz77r4jJttcRvrP2rTbTBiwuhpmiufRyk3BuWlgzU3yaSuQV3M="\n' s += "\n" s += "#\n" s += "# Configurations\n" From 30a95ef9d6dafe7577119bdd650aa6a720bd3fc2 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 8 Jun 2018 11:28:38 +0200 Subject: [PATCH 06/29] Simplify check whether argument of --prop is a file/property Before, the argument to `--prop` was only treated as a file if (a) it exits and (b) contains a dot. We remove the requirement for a dot and always treat the argument as a file if it exists. --- src/storm/api/properties.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index f6a2d00e3..5b5d53bcb 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -24,10 +24,9 @@ namespace storm { } std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter) { - // If the given property looks like a file (containing a dot and there exists a file with that name), - // we try to parse it as a file, otherwise we assume it's a property. + // If the given property is a file, we parse it as a file, otherwise we assume it's a property. std::vector properties; - if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) { + if (std::ifstream(inputString).good()) { properties = formulaParser.parseFromFile(inputString); } else { properties = formulaParser.parseFromString(inputString); From 04a1bbedfcf72dbab46f65368b079a2cf622dcd1 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 8 Jun 2018 12:34:43 +0200 Subject: [PATCH 07/29] properties.cpp: Log filename of properties file in --verbose mode --- src/storm/api/properties.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index 5b5d53bcb..71fab4d79 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -27,6 +27,7 @@ namespace storm { // If the given property is a file, we parse it as a file, otherwise we assume it's a property. std::vector properties; if (std::ifstream(inputString).good()) { + STORM_LOG_INFO("Loading properties from file: " << inputString << std::endl); properties = formulaParser.parseFromFile(inputString); } else { properties = formulaParser.parseFromString(inputString); From 2948611f3f61afccf8cf402e32d430e5b1609f9b Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 8 Jun 2018 16:54:20 +0200 Subject: [PATCH 08/29] cli.cpp: Quote arguments in "Command line arguments" status line It's nice to be able to copy-paste the arguments from a log file to a shell, so we'd like to have proper quoting. We thus use single quotes if an argument contains non-safe characters in the log output. --- src/storm-cli-utilities/cli.cpp | 27 ++++++++++++++++++++++++--- src/storm-cli-utilities/cli.h | 7 +++++++ 2 files changed, 31 insertions(+), 3 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index dfc3065b8..4d44454c8 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -11,6 +11,7 @@ #include #include +#include #include "storm-cli-utilities/model-handling.h" @@ -63,7 +64,27 @@ namespace storm { storm::utility::cleanUp(); return 0; } - + + std::string shellQuoteSingleIfNecessary(const std::string& arg) { + // quote empty argument + if (arg.empty()) { + return "''"; + } + + if (arg.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789-_./=") != std::string::npos) { + // contains potentially unsafe character, needs quoting + if (arg.find('\'') != std::string::npos) { + // contains ', we have to replace all ' with '\'' + std::string escaped(arg); + boost::replace_all(escaped, "'", "'\\''"); + return "'" + escaped + "'"; + } else { + return "'" + arg + "'"; + } + } + + return arg; + } void printHeader(std::string const& name, const int argc, const char** argv) { STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl); @@ -71,7 +92,7 @@ namespace storm { // "Compute" the command line argument string with which storm was invoked. std::stringstream commandStream; for (int i = 1; i < argc; ++i) { - commandStream << argv[i] << " "; + commandStream << " " << shellQuoteSingleIfNecessary(argv[i]); } std::string command = commandStream.str(); @@ -79,7 +100,7 @@ namespace storm { if (!command.empty()) { std::time_t result = std::time(nullptr); STORM_PRINT("Date: " << std::ctime(&result)); - STORM_PRINT("Command line arguments: " << commandStream.str() << std::endl); + STORM_PRINT("Command line arguments:" << commandStream.str() << std::endl); STORM_PRINT("Current working directory: " << storm::utility::cli::getCurrentWorkingDirectory() << std::endl << std::endl); } } diff --git a/src/storm-cli-utilities/cli.h b/src/storm-cli-utilities/cli.h index e8d8601e9..66c51bad6 100644 --- a/src/storm-cli-utilities/cli.h +++ b/src/storm-cli-utilities/cli.h @@ -11,6 +11,13 @@ namespace storm { */ int64_t process(const int argc, const char** argv); + /*! + * For a command-line argument, returns a quoted version + * with single quotes if it contains unsafe characters. + * Otherwise, just returns the unquoted argument. + */ + std::string shellQuoteSingleIfNecessary(const std::string& arg); + void printHeader(std::string const& name, const int argc, const char** argv); void printVersion(std::string const& name); From b6d67e7995ae69cf14bd4f320ba4effe06a6b3b8 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 8 Jun 2018 16:59:03 +0200 Subject: [PATCH 09/29] properties.cpp: Output warning if we filter away all properties --- src/storm/api/properties.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index 71fab4d79..163679013 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -78,6 +78,11 @@ namespace storm { std::set const& propertyNameSet = propertyFilter.get(); std::vector result; std::set reducedPropertyNames; + + if (propertyNameSet.empty()) { + STORM_LOG_WARN("Filtering all properties."); + } + for (auto const& property : properties) { if (propertyNameSet.find(property.getName()) != propertyNameSet.end()) { result.push_back(property); From e29e6c7cd28f30222ac0edfbd7a977d731a1105c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 10 Jun 2018 12:20:40 +0200 Subject: [PATCH 10/29] high level counterexamples extended with more options, and improved performance when minimizing over a subset --- .../SMTMinimalLabelSetGenerator.h | 122 ++++++++++++++---- 1 file changed, 96 insertions(+), 26 deletions(-) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 6b4c440c1..000d830ad 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -49,14 +49,20 @@ namespace storm { // The set of labels that matter in terms of minimality. boost::container::flat_set minimalityLabels; - + // A set of labels that is definitely known to be taken in the final solution. boost::container::flat_set knownLabels; + + boost::container::flat_set dontCareLabels; // A list of relevant choices for each relevant state. std::map> relevantChoicesForRelevantStates; }; - + + struct GeneratorStats { + + }; + struct VariableInformation { // The manager responsible for the constraints we are building. std::shared_ptr manager; @@ -154,10 +160,12 @@ namespace storm { std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); relevancyInformation.relevantLabels = remainingLabels; } - + + relevancyInformation.dontCareLabels = dontCareLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), dontCareLabels.begin(), dontCareLabels.end(), std::inserter(relevancyInformation.minimalityLabels, relevancyInformation.minimalityLabels.begin())); STORM_LOG_DEBUG("Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels."); + STORM_LOG_DEBUG("Found " << relevancyInformation.minimalityLabels.size() << " labels to minize over."); return relevancyInformation; } @@ -649,10 +657,11 @@ namespace storm { // Popping the disjunction of negated guards from the solver stack. localSolver->pop(); + STORM_LOG_ERROR_COND(backwardImplicationAdded, "Error in adding cuts for counterexample generation (backward implication misses a label set)."); } else { STORM_LOG_DEBUG("Selection is enabled in initial state."); } - STORM_LOG_ERROR_COND(backwardImplicationAdded, "Error in adding cuts for counterexample generation (backward implication misses a label set)."); + } } else if (symbolicModel.isJaniModel()) { STORM_LOG_WARN("Model uses assignment levels, did not assert backward implications."); @@ -1316,7 +1325,7 @@ namespace storm { * in order to satisfy the constraint system. * @return The smallest set of labels such that the constraint system of the solver is satisfiable. */ - static boost::container::flat_set findSmallestCommandSet(storm::solver::SmtSolver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { + static boost::optional> findSmallestCommandSet(storm::solver::SmtSolver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { // Check if we can find a solution with the current bound. storm::expressions::Expression assumption = !variableInformation.auxiliaryVariables.back(); @@ -1331,6 +1340,10 @@ namespace storm { solver.add(variableInformation.auxiliaryVariables.back()); variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound)); assumption = !variableInformation.auxiliaryVariables.back(); + if (currentBound > (1 << variableInformation.minimalityLabelVariables.size())) { + STORM_LOG_DEBUG("Constraint system fully explored: Bound exceeds maximum of " << (1 << variableInformation.minimalityLabelVariables.size())); + return boost::none; + } } // At this point we know that the constraint system was satisfiable, so compute the induced label @@ -1342,12 +1355,17 @@ namespace storm { std::vector formulae; boost::container::flat_set unknownLabels; - std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); + std::set_intersection(labelSet.begin(), labelSet.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); + + //std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); for (auto const& label : unknownLabels) { formulae.emplace_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } + boost::container::flat_set remainingLabels; - std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), labelSet.begin(), labelSet.end(), std::inserter(remainingLabels, remainingLabels.end())); + //std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), labelSet.begin(), labelSet.end(), std::inserter(remainingLabels, remainingLabels.end())); + std::set_difference(relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), labelSet.begin(), labelSet.end(), std::inserter(remainingLabels, remainingLabels.end())); + for (auto const& label : remainingLabels) { formulae.emplace_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } @@ -1355,6 +1373,22 @@ namespace storm { STORM_LOG_DEBUG("Ruling out single solution."); assertDisjunction(solver, formulae, *variableInformation.manager); } + + static void ruleOutBiggerSolutions(storm::solver::SmtSolver& solver, boost::container::flat_set const& labelSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + std::vector formulae; + + boost::container::flat_set unknownLabels; + std::set_intersection(labelSet.begin(), labelSet.end(), relevancyInformation.minimalityLabels.begin(), relevancyInformation.minimalityLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); + + //std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); + for (auto const& label : unknownLabels) { + formulae.emplace_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); + } + + + STORM_LOG_DEBUG("Ruling out set of solutions."); + assertDisjunction(solver, formulae, *variableInformation.manager); + } /*! * Analyzes the given sub-model that has a maximal reachability of zero (i.e. no psi states are reachable) and tries to construct assertions that aim to make at least one psi state reachable. @@ -1664,6 +1698,9 @@ namespace storm { bool encodeReachability; bool useDynamicConstraints; bool silent = false; + uint64_t continueAfterFirstCounterexampleUntil = 0; + uint64_t maximumCounterexamples = 1; + uint64_t multipleCounterexampleSizeCap = 100000000; }; /*! @@ -1677,8 +1714,9 @@ namespace storm { * @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false). * @param options A set of options for customization. */ - static boost::container::flat_set getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { + static std::vector> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { #ifdef STORM_HAVE_Z3 + std::vector> result; // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); auto timeOfLastMessage = std::chrono::high_resolution_clock::now(); @@ -1762,10 +1800,10 @@ namespace storm { // If there are no relevant labels, return directly. if (relevancyInformation.relevantLabels.empty()) { - return commandSet; + return {commandSet}; } else if (relevancyInformation.minimalityLabels.empty()) { commandSet.insert(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end()); - return commandSet; + return {commandSet}; } // Set up some variables for the iterations. @@ -1775,17 +1813,31 @@ namespace storm { uint_fast64_t currentBound = 0; maximalReachabilityProbability = 0; uint_fast64_t zeroProbabilityCount = 0; + uint64_t smallestCounterexampleSize = model.getNumberOfChoices(); // Definitive u uint64_t progressDelay = storm::settings::getModule().getShowProgressDelay(); do { STORM_LOG_DEBUG("Computing minimal command set."); solverClock = std::chrono::high_resolution_clock::now(); - commandSet = findSmallestCommandSet(*solver, variableInformation, currentBound); + boost::optional> smallest = findSmallestCommandSet(*solver, variableInformation, currentBound); totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock; - STORM_LOG_DEBUG("Computed minimal command set of size " << commandSet.size() + relevancyInformation.knownLabels.size() << " (" << commandSet.size() << " + " << relevancyInformation.knownLabels.size() << ") "); + if(smallest == boost::none) { + STORM_LOG_DEBUG("No further counterexamples."); + break; + } else { + commandSet = smallest.get(); + } + STORM_LOG_DEBUG("Computed minimal command with bound " << currentBound << " and set of size " << commandSet.size() + relevancyInformation.knownLabels.size() << " (" << commandSet.size() << " + " << relevancyInformation.knownLabels.size() << ") "); // Restrict the given model to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); + commandSet.insert(relevancyInformation.dontCareLabels.begin(), relevancyInformation.dontCareLabels.end()); + if (commandSet.size() > smallestCounterexampleSize + options.continueAfterFirstCounterexampleUntil || (result.size() > 1 && commandSet.size() > options.multipleCounterexampleSizeCap) ) { + STORM_LOG_DEBUG("No further counterexamples of similar size."); + break; + } + + auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet); std::shared_ptr> const& subModel = subChoiceOrigins.first; std::vector> const& subLabelSets = subChoiceOrigins.second; @@ -1818,7 +1870,17 @@ namespace storm { ruleOutSingleSolution(*solver, commandSet, variableInformation, relevancyInformation); } } else { - done = true; + STORM_LOG_DEBUG("Found a counterexample."); + result.push_back(commandSet); + if (options.maximumCounterexamples > result.size()) { + STORM_LOG_DEBUG("Exclude counterexample for future."); + ruleOutBiggerSolutions(*solver, commandSet, variableInformation, relevancyInformation); + + } else { + STORM_LOG_DEBUG("Stop searching for further counterexamples."); + done = true; + } + } totalAnalysisTime += (std::chrono::high_resolution_clock::now() - analysisClock); ++iterations; @@ -1828,10 +1890,10 @@ namespace storm { if (static_cast(durationSinceLastMessage) >= progressDelay || lastSize < commandSet.size()) { auto milliseconds = std::chrono::duration_cast(now - totalClock).count(); if (lastSize < commandSet.size()) { - std::cout << "Improved lower bound to " << commandSet.size() << " after " << milliseconds << "ms." << std::endl; + std::cout << "Improved lower bound to " << currentBound << " after " << milliseconds << "ms." << std::endl; lastSize = commandSet.size(); } else { - std::cout << "Lower bound on label set size is " << commandSet.size() << " after " << milliseconds << "ms (checked " << iterations << " models, " << zeroProbabilityCount << " could not reach the target set)." << std::endl; + std::cout << "Lower bound on label set size is " << currentBound << " after " << milliseconds << "ms (checked " << iterations << " models, " << zeroProbabilityCount << " could not reach the target set)." << std::endl; timeOfLastMessage = std::chrono::high_resolution_clock::now(); } } @@ -1863,7 +1925,7 @@ namespace storm { std::cout << " * number of models that could not reach a target state: " << zeroProbabilityCount << " (" << 100 * static_cast(zeroProbabilityCount)/iterations << "%)" << std::endl << std::endl; } - return commandSet; + return result; #else throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3."; #endif @@ -1953,7 +2015,7 @@ namespace storm { } - static boost::container::flat_set computeCounterexampleLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::shared_ptr const& formula, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options(true)) { + static std::vector> computeCounterexampleLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::shared_ptr const& formula, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options(true)) { STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models."); if (!options.silent) { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; @@ -2025,28 +2087,36 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, dontCareLabels, options); + auto labelSets = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, dontCareLabels, options); auto endTime = std::chrono::high_resolution_clock::now(); if (!options.silent) { - std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + for (auto const& labelSet : labelSets) { + std::cout << std::endl << "Computed minimal label set of size " << labelSet.size(); + + } + std::cout << std::endl << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + } // Extend the command set properly. - if (lowerBoundedFormula) { - extendLabelSetLowerBound(model, labelSet, phiStates, psiStates, options.silent); + for (auto& labelSet : labelSets) { + if (lowerBoundedFormula) { + extendLabelSetLowerBound(model, labelSet, phiStates, psiStates, options.silent); + } } - return labelSet; + return labelSets; } static std::shared_ptr computeCounterexample(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 - auto labelSet = computeCounterexampleLabelSet(env, symbolicModel, model, formula); - + auto labelSets = computeCounterexampleLabelSet(env, symbolicModel, model, formula); + + if (symbolicModel.isPrismProgram()) { - return std::make_shared(symbolicModel.asPrismProgram().restrictCommands(labelSet)); + return std::make_shared(symbolicModel.asPrismProgram().restrictCommands(labelSets[0])); } else { STORM_LOG_ASSERT(symbolicModel.isJaniModel(), "Unknown symbolic model description type."); - return std::make_shared(symbolicModel.asJaniModel().restrictEdges(labelSet)); + return std::make_shared(symbolicModel.asJaniModel().restrictEdges(labelSets[0])); } #else throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3."; From d1ab2600688c2e645971c13329114b7b74ad8c0b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 10 Jun 2018 12:22:34 +0200 Subject: [PATCH 11/29] remove outdated parts in highlevel counterexamplse --- .../SMTMinimalLabelSetGenerator.h | 106 ------------------ 1 file changed, 106 deletions(-) diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 000d830ad..0313fe655 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1162,112 +1162,6 @@ namespace storm { return relaxingVariable; } - /*! - * Asserts that the input vector encodes a decimal smaller or equal to one. - * - * @param context The Z3 context in which to build the expressions. - * @param solver The solver to use for the satisfiability evaluation. - * @param input The binary encoded input number. - */ - static void assertLessOrEqualOne(z3::context& context, z3::solver& solver, std::vector input) { - std::transform(input.begin(), input.end(), input.begin(), [](z3::expr e) -> z3::expr { return !e; }); - assertConjunction(context, solver, input); - } - - /*! - * Asserts that at most one of given literals may be true at any time. - * - * @param context The Z3 context in which to build the expressions. - * @param solver The solver to use for the satisfiability evaluation. - * @param blockingVariables A vector of variables out of which only one may be true. - */ - static void assertAtMostOne(z3::context& context, z3::solver& solver, std::vector const& literals) { - std::vector counter = createCounterCircuit(context, literals); - assertLessOrEqualOne(context, solver, counter); - } - - /*! - * Performs one Fu-Malik-Maxsat step. - * - * @param context The Z3 context in which to build the expressions. - * @param solver The solver to use for the satisfiability evaluation. - * @param variableInformation A structure with information about the variables for the labels. - * @return True iff the constraint system was satisfiable. - */ - static bool fuMalikMaxsatStep(z3::context& context, z3::solver& solver, std::vector& auxiliaryVariables, std::vector& softConstraints, uint_fast64_t& nextFreeVariableIndex) { - z3::expr_vector assumptions(context); - for (auto const& auxiliaryVariable : auxiliaryVariables) { - assumptions.push_back(!auxiliaryVariable); - } - - // Check whether the assumptions are satisfiable. - STORM_LOG_DEBUG("Invoking satisfiability checking."); - z3::check_result result = solver.check(assumptions); - STORM_LOG_DEBUG("Done invoking satisfiability checking."); - - if (result == z3::sat) { - return true; - } else { - STORM_LOG_DEBUG("Computing unsat core."); - z3::expr_vector unsatCore = solver.unsat_core(); - STORM_LOG_DEBUG("Computed unsat core."); - - std::vector blockingVariables; - blockingVariables.reserve(unsatCore.size()); - - // Create stringstream to build expression names. - std::stringstream variableName; - - for (uint_fast64_t softConstraintIndex = 0; softConstraintIndex < softConstraints.size(); ++softConstraintIndex) { - for (uint_fast64_t coreIndex = 0; coreIndex < unsatCore.size(); ++coreIndex) { - bool isContainedInCore = false; - if (softConstraints[softConstraintIndex] == unsatCore[coreIndex]) { - isContainedInCore = true; - } - - if (isContainedInCore) { - variableName.clear(); - variableName.str(""); - variableName << "b" << nextFreeVariableIndex; - blockingVariables.push_back(context.bool_const(variableName.str().c_str())); - - variableName.clear(); - variableName.str(""); - variableName << "a" << nextFreeVariableIndex; - ++nextFreeVariableIndex; - auxiliaryVariables[softConstraintIndex] = context.bool_const(variableName.str().c_str()); - - softConstraints[softConstraintIndex] = softConstraints[softConstraintIndex] || blockingVariables.back(); - - solver.add(softConstraints[softConstraintIndex] || auxiliaryVariables[softConstraintIndex]); - } - } - } - - assertAtMostOne(context, solver, blockingVariables); - } - - return false; - } - - /*! - * Rules out the given command set for the given solver. - * - * @param context The Z3 context in which to build the expressions. - * @param solver The solver to use for the satisfiability evaluation. - * @param commandSet The command set to rule out as a solution. - * @param variableInformation A structure with information about the variables for the labels. - */ - static void ruleOutSolution(z3::context& context, z3::solver& solver, boost::container::flat_set const& commandSet, VariableInformation const& variableInformation) { - z3::expr blockSolutionExpression = context.bool_val(false); - for (auto labelIndexPair : variableInformation.labelToIndexMap) { - if (commandSet.find(labelIndexPair.first) != commandSet.end()) { - blockSolutionExpression = blockSolutionExpression || variableInformation.labelVariables[labelIndexPair.second]; - } - } - - solver.add(blockSolutionExpression); - } /*! * Determines the set of labels that was chosen by the given model. From 6dfce6a405fdd52e3f24f422893a29a77a3043da Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 10 Jun 2018 18:50:56 +0200 Subject: [PATCH 12/29] extended counterexamples towards expected rewards, and moved counterexamples to a seperate lib (still in main cli) to slightly accelarate building times --- src/CMakeLists.txt | 1 + src/storm-cli-utilities/CMakeLists.txt | 2 +- src/storm-cli-utilities/cli.cpp | 2 + src/storm-cli-utilities/model-handling.h | 2 + src/storm-counterexamples/CMakeLists.txt | 40 ++++++++ .../api/counterexamples.cpp | 2 +- .../api/counterexamples.h | 4 +- .../counterexamples/Counterexample.cpp | 2 +- .../counterexamples/Counterexample.h | 0 .../HighLevelCounterexample.cpp | 2 +- .../counterexamples/HighLevelCounterexample.h | 2 +- .../MILPMinimalLabelSetGenerator.h | 4 +- .../SMTMinimalLabelSetGenerator.h | 91 +++++++++++++------ .../CounterexampleGeneratorSettings.cpp | 2 +- .../modules/CounterexampleGeneratorSettings.h | 0 src/storm-pars/settings/ParsSettings.cpp | 2 - src/storm/api/storm.h | 1 - src/storm/settings/SettingsManager.cpp | 2 - .../utility/ModelInstantiatorTest.cpp | 1 + 19 files changed, 118 insertions(+), 44 deletions(-) create mode 100644 src/storm-counterexamples/CMakeLists.txt rename src/{storm => storm-counterexamples}/api/counterexamples.cpp (95%) rename src/{storm => storm-counterexamples}/api/counterexamples.h (80%) rename src/{storm => storm-counterexamples}/counterexamples/Counterexample.cpp (79%) rename src/{storm => storm-counterexamples}/counterexamples/Counterexample.h (100%) rename src/{storm => storm-counterexamples}/counterexamples/HighLevelCounterexample.cpp (92%) rename src/{storm => storm-counterexamples}/counterexamples/HighLevelCounterexample.h (93%) rename src/{storm => storm-counterexamples}/counterexamples/MILPMinimalLabelSetGenerator.h (99%) rename src/{storm => storm-counterexamples}/counterexamples/SMTMinimalLabelSetGenerator.h (95%) rename src/{storm => storm-counterexamples}/settings/modules/CounterexampleGeneratorSettings.cpp (98%) rename src/{storm => storm-counterexamples}/settings/modules/CounterexampleGeneratorSettings.h (100%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index acf819119..0f277386d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -5,6 +5,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) add_custom_target(binaries) add_subdirectory(storm) +add_subdirectory(storm-counterexamples) add_subdirectory(storm-cli-utilities) add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl-cli) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt index 84819b72b..5e37b5db4 100644 --- a/src/storm-cli-utilities/CMakeLists.txt +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -17,7 +17,7 @@ set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-cli-utilities) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-cli-utilities PUBLIC storm) +target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples) # Install storm headers to include directory. foreach(HEADER ${STORM_CLI_UTIL_HEADERS}) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 4d44454c8..e79971cbc 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -49,6 +49,8 @@ namespace storm { storm::cli::printHeader("Storm", argc, argv); storm::settings::initializeAll("Storm", "storm"); + storm::settings::addModule(); + storm::utility::Stopwatch totalTimer(true); if (!storm::cli::parseOptions(argc, argv)) { return -1; diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index d03cfe630..b57818c08 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -2,6 +2,8 @@ #include "storm/api/storm.h" +#include "storm-counterexamples/api/counterexamples.h" + #include "storm/utility/resources.h" #include "storm/utility/file.h" #include "storm/utility/storm-version.h" diff --git a/src/storm-counterexamples/CMakeLists.txt b/src/storm-counterexamples/CMakeLists.txt new file mode 100644 index 000000000..d01c4ceb7 --- /dev/null +++ b/src/storm-counterexamples/CMakeLists.txt @@ -0,0 +1,40 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-counterexamples) + + + +file(GLOB_RECURSE STORM_CEX_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.cpp) +file(GLOB_RECURSE STORM_CEX_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h) + + +# Create storm-dft. +add_library(storm-counterexamples SHARED ${STORM_CEX_SOURCES} ${STORM_CEX_HEADERS}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-counterexamples PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-counterexamples) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-counterexamples PUBLIC storm) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_DFT_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_CEX_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_cex_headers DEPENDS ${STORM_CEX_OUTPUT_HEADERS} ${STORM_CEX_HEADERS}) +add_dependencies(storm-counterexamples copy_storm_cex_headers) + +# installation +install(TARGETS storm-counterexamples EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm/api/counterexamples.cpp b/src/storm-counterexamples/api/counterexamples.cpp similarity index 95% rename from src/storm/api/counterexamples.cpp rename to src/storm-counterexamples/api/counterexamples.cpp index c57724ad5..5652beba6 100644 --- a/src/storm/api/counterexamples.cpp +++ b/src/storm-counterexamples/api/counterexamples.cpp @@ -1,4 +1,4 @@ -#include "storm/api/counterexamples.h" +#include "storm-counterexamples/api/counterexamples.h" #include "storm/environment/Environment.h" diff --git a/src/storm/api/counterexamples.h b/src/storm-counterexamples/api/counterexamples.h similarity index 80% rename from src/storm/api/counterexamples.h rename to src/storm-counterexamples/api/counterexamples.h index 672ddc4df..6a5984991 100644 --- a/src/storm/api/counterexamples.h +++ b/src/storm-counterexamples/api/counterexamples.h @@ -1,7 +1,7 @@ #pragma once -#include "storm/counterexamples/MILPMinimalLabelSetGenerator.h" -#include "storm/counterexamples/SMTMinimalLabelSetGenerator.h" +#include "storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h" +#include "storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h" namespace storm { namespace api { diff --git a/src/storm/counterexamples/Counterexample.cpp b/src/storm-counterexamples/counterexamples/Counterexample.cpp similarity index 79% rename from src/storm/counterexamples/Counterexample.cpp rename to src/storm-counterexamples/counterexamples/Counterexample.cpp index 4aba71b9c..9975f54ba 100644 --- a/src/storm/counterexamples/Counterexample.cpp +++ b/src/storm-counterexamples/counterexamples/Counterexample.cpp @@ -1,4 +1,4 @@ -#include "storm/counterexamples/Counterexample.h" +#include "storm-counterexamples/counterexamples/Counterexample.h" namespace storm { namespace counterexamples { diff --git a/src/storm/counterexamples/Counterexample.h b/src/storm-counterexamples/counterexamples/Counterexample.h similarity index 100% rename from src/storm/counterexamples/Counterexample.h rename to src/storm-counterexamples/counterexamples/Counterexample.h diff --git a/src/storm/counterexamples/HighLevelCounterexample.cpp b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.cpp similarity index 92% rename from src/storm/counterexamples/HighLevelCounterexample.cpp rename to src/storm-counterexamples/counterexamples/HighLevelCounterexample.cpp index 707ed6d39..11279a220 100644 --- a/src/storm/counterexamples/HighLevelCounterexample.cpp +++ b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.cpp @@ -1,4 +1,4 @@ -#include "storm/counterexamples/HighLevelCounterexample.h" +#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" namespace storm { namespace counterexamples { diff --git a/src/storm/counterexamples/HighLevelCounterexample.h b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h similarity index 93% rename from src/storm/counterexamples/HighLevelCounterexample.h rename to src/storm-counterexamples/counterexamples/HighLevelCounterexample.h index 92310a5ba..27fe981c0 100644 --- a/src/storm/counterexamples/HighLevelCounterexample.h +++ b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/counterexamples/Counterexample.h" +#include "Counterexample.h" #include "storm/storage/SymbolicModelDescription.h" diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h similarity index 99% rename from src/storm/counterexamples/MILPMinimalLabelSetGenerator.h rename to src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h index 861f86f83..52ed50778 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h @@ -17,7 +17,7 @@ #include "storm/solver/MinMaxLinearEquationSolver.h" -#include "storm/counterexamples/HighLevelCounterexample.h" +#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" #include "storm/utility/graph.h" #include "storm/utility/counterexamples.h" @@ -29,7 +29,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm/settings/modules/CounterexampleGeneratorSettings.h" +#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" namespace storm { diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h similarity index 95% rename from src/storm/counterexamples/SMTMinimalLabelSetGenerator.h rename to src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 0313fe655..4de23e767 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -5,7 +5,7 @@ #include "storm/solver/Z3SmtSolver.h" -#include "storm/counterexamples/HighLevelCounterexample.h" +#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" @@ -1510,7 +1510,7 @@ namespace storm { * Returns the sub-model obtained from removing all choices that do not originate from the specified filterLabelSet. * Also returns the Labelsets of the sub-model. */ - static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet) { + static std::pair>, std::vector>> restrictModelToLabelSet(storm::models::sparse::Model const& model, boost::container::flat_set const& filterLabelSet, boost::optional absorbState = boost::none) { bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp); @@ -1544,7 +1544,8 @@ namespace storm { if (customRowGrouping) { transitionMatrixBuilder.newRowGroup(currentRow); } - transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::one()); + uint64_t targetState = absorbState == boost::none ? state : absorbState.get(); + transitionMatrixBuilder.addNextValue(currentRow, targetState, storm::utility::one()); // Insert an empty label set for this choice resultLabelSet.emplace_back(); ++currentRow; @@ -1561,17 +1562,25 @@ namespace storm { return std::make_pair(resultModel, std::move(resultLabelSet)); } - static T computeMaximalReachabilityProbability(Environment const& env, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static T computeMaximalReachabilityProbability(Environment const& env, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional const& rewardName) { T result = storm::utility::zero(); std::vector allStatesResult; STORM_LOG_DEBUG("Invoking model checker."); if (model.isOfType(storm::models::ModelType::Dtmc)) { - allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false); + if (rewardName == boost::none) { + allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false); + } else { + allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), model.getRewardModel(rewardName.get()), psiStates, false); + } } else { - storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; - allStatesResult = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false, false).values); + if (rewardName == boost::none) { + storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; + allStatesResult = std::move(modelCheckerHelper.computeUntilProbabilities(env, false, model.getTransitionMatrix(),model.getBackwardTransitions(), phiStates,psiStates, false, false).values); + } else { + STORM_LOG_THROW(rewardName != boost::none, storm::exceptions::NotSupportedException, "Reward property counterexample generation is currently only supported for DTMCs."); + } } for (auto state : model.getInitialStates()) { result = std::max(result, allStatesResult[state]); @@ -1604,11 +1613,12 @@ namespace storm { * @param model The sparse model in which to find the minimal command set. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiStates A bit vector characterizing all psi states in the model. - * @param probabilityThreshold The threshold that is to be achieved or exceeded. + * @param propertyThreshold The threshold that is to be achieved or exceeded. + * @param rewardName The name of the reward structure to use, or boost::none if probabilities are considerd. * @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false). * @param options A set of options for customization. */ - static std::vector> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { + static std::vector> getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double propertyThreshold, boost::optional const& rewardName, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { #ifdef STORM_HAVE_Z3 std::vector> result; // Set up all clocks used for time measurement. @@ -1650,10 +1660,10 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (options.checkThresholdFeasible) { - maximalReachabilityProbability = computeMaximalReachabilityProbability(env, model, phiStates, psiStates); + maximalReachabilityProbability = computeMaximalReachabilityProbability(env, model, phiStates, psiStates, rewardName); - STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); - std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; + STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= propertyThreshold) || (!strictBound && maximalReachabilityProbability > propertyThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << propertyThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); + std::cout << std::endl << "Maximal property value in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; } // (2) Identify all states and commands that are relevant, because only these need to be considered later. @@ -1705,7 +1715,7 @@ namespace storm { uint_fast64_t lastSize = 0; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; - maximalReachabilityProbability = 0; + double maximalPropertyValue = 0; uint_fast64_t zeroProbabilityCount = 0; uint64_t smallestCounterexampleSize = model.getNumberOfChoices(); // Definitive u uint64_t progressDelay = storm::settings::getModule().getShowProgressDelay(); @@ -1732,18 +1742,18 @@ namespace storm { } - auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet); + auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0)); std::shared_ptr> const& subModel = subChoiceOrigins.first; std::vector> const& subLabelSets = subChoiceOrigins.second; // Now determine the maximal reachability probability in the sub-model. - maximalReachabilityProbability = computeMaximalReachabilityProbability(env, *subModel, phiStates, psiStates); + maximalPropertyValue = computeMaximalReachabilityProbability(env, *subModel, phiStates, psiStates, rewardName); totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock; // Depending on whether the threshold was successfully achieved or not, we proceed by either analyzing the bad solution or stopping the iteration process. analysisClock = std::chrono::high_resolution_clock::now(); - if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { - if (maximalReachabilityProbability == storm::utility::zero()) { + if ((strictBound && maximalPropertyValue < propertyThreshold) || (!strictBound && maximalPropertyValue <= propertyThreshold)) { + if (maximalPropertyValue == storm::utility::zero()) { ++zeroProbabilityCount; } @@ -1759,6 +1769,10 @@ namespace storm { // the given threshold, we analyze the solution and try to guide the solver into the right direction. analyzeInsufficientProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } + + if (relevancyInformation.dontCareLabels.size() > 0) { + ruleOutSingleSolution(*solver, commandSet, variableInformation, relevancyInformation); + } } else { // Do not guide solver, just rule out current solution. ruleOutSingleSolution(*solver, commandSet, variableInformation, relevancyInformation); @@ -1915,22 +1929,41 @@ namespace storm { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; } - STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); - storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); - STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); - STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); + storm::logic::ComparisonType comparisonType; + double threshold; + boost::optional rewardName = boost::none; + + STORM_LOG_THROW(formula->isProbabilityOperatorFormula() || formula->isRewardOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); + if (formula->isProbabilityOperatorFormula()) { + storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); + STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); + STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation."); + + comparisonType = probabilityOperator.getComparisonType(); + threshold = probabilityOperator.getThresholdAs(); + } else { + assert(formula->isRewardOperatorFormula()); + storm::logic::RewardOperatorFormula const& rewardOperator = formula->asRewardOperatorFormula(); + STORM_LOG_THROW(rewardOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas."); + STORM_LOG_THROW( rewardOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'F phi' for counterexample generation."); + + comparisonType = rewardOperator.getComparisonType(); + threshold = rewardOperator.getThresholdAs(); + rewardName = rewardOperator.getRewardModelName(); - storm::logic::ComparisonType comparisonType = probabilityOperator.getComparisonType(); - bool strictBound = comparisonType == storm::logic::ComparisonType::Less; - double threshold = probabilityOperator.getThresholdAs(); + STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for probability formulas."); + } + bool strictBound = comparisonType == storm::logic::ComparisonType::Less; + storm::logic::Formula const& subformula = formula->asOperatorFormula().getSubformula(); + storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; storm::modelchecker::SparsePropositionalModelChecker> modelchecker(model); - if (probabilityOperator.getSubformula().isUntilFormula()) { + if (subformula.isUntilFormula()) { STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType), storm::exceptions::NotSupportedException, "Lower bounds in counterexamples are only supported for eventually formulas."); - storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); + storm::logic::UntilFormula const& untilFormula = subformula.asUntilFormula(); std::unique_ptr leftResult = modelchecker.check(env, untilFormula.getLeftSubformula()); std::unique_ptr rightResult = modelchecker.check(env, untilFormula.getRightSubformula()); @@ -1940,8 +1973,8 @@ namespace storm { phiStates = leftQualitativeResult.getTruthValuesVector(); psiStates = rightQualitativeResult.getTruthValuesVector(); - } else if (probabilityOperator.getSubformula().isEventuallyFormula()) { - storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula(); + } else if (subformula.isEventuallyFormula()) { + storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula(); std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); @@ -1981,7 +2014,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSets = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, dontCareLabels, options); + auto labelSets = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, rewardName, strictBound, dontCareLabels, options); auto endTime = std::chrono::high_resolution_clock::now(); if (!options.silent) { for (auto const& labelSet : labelSets) { diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp similarity index 98% rename from src/storm/settings/modules/CounterexampleGeneratorSettings.cpp rename to src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp index 0eaf656bb..9fe9d3d36 100644 --- a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp @@ -1,4 +1,4 @@ -#include "storm/settings/modules/CounterexampleGeneratorSettings.h" +#include "CounterexampleGeneratorSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/exceptions/InvalidSettingsException.h" diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.h b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h similarity index 100% rename from src/storm/settings/modules/CounterexampleGeneratorSettings.h rename to src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp index a0e9d8073..bf6065d62 100644 --- a/src/storm-pars/settings/ParsSettings.cpp +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -1,4 +1,3 @@ -#include #include "storm-pars/settings/ParsSettings.h" #include "storm-pars/settings/modules/ParametricSettings.h" @@ -38,7 +37,6 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm/api/storm.h b/src/storm/api/storm.h index ffc4c75a6..d8f6aed82 100644 --- a/src/storm/api/storm.h +++ b/src/storm/api/storm.h @@ -6,5 +6,4 @@ #include "storm/api/bisimulation.h" #include "storm/api/transformation.h" #include "storm/api/verification.h" -#include "storm/api/counterexamples.h" #include "storm/api/export.h" diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index fc2b80b35..f18f76bb1 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -17,7 +17,6 @@ #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/settings/modules/DebugSettings.h" -#include "storm/settings/modules/CounterexampleGeneratorSettings.h" #include "storm/settings/modules/CuddSettings.h" #include "storm/settings/modules/BuildSettings.h" #include "storm/settings/modules/SylvanSettings.h" @@ -531,7 +530,6 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp index e66a912d5..1873a4436 100644 --- a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp +++ b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp @@ -16,6 +16,7 @@ #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" TEST(ModelInstantiatorTest, BrpProb) { carl::VariablePool::getInstance().clear(); From 3a704ae5327b01c298e44ffa318c7a636c9c7cb0 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 10 Jun 2018 18:51:25 +0200 Subject: [PATCH 13/29] fix storm-dft missing includes --- src/storm-dft-cli/storm-dft.cpp | 1 + src/storm-dft/modelchecker/dft/DFTModelChecker.cpp | 3 +++ 2 files changed, 4 insertions(+) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 9923330d0..ce31be5b8 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -5,6 +5,7 @@ #include "storm-dft/settings/modules/FaultTreeSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/ResourceSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 8d277d60d..24e39a0f5 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -1,9 +1,12 @@ #include "DFTModelChecker.h" #include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/builder/ParallelCompositionBuilder.h" #include "storm/utility/bitoperations.h" #include "storm/utility/DirectEncodingExporter.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" From 79bb6734ed94b6e5897ada83e1349bfb6e8502ff Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 10 Jun 2018 20:20:39 +0200 Subject: [PATCH 14/29] compile and link parsers in seperate binary --- src/CMakeLists.txt | 1 + src/storm-cli-utilities/CMakeLists.txt | 2 +- src/storm-cli-utilities/model-handling.h | 1 + src/storm-dft-cli/storm-dft.cpp | 2 + src/storm-dft/parser/DFTGalileoParser.h | 4 +- src/storm-dft/parser/DFTJsonParser.h | 2 +- src/storm-gspn-cli/storm-gspn.cpp | 2 +- .../builder/ExplicitGspnModelBuilder.cpp | 2 +- src/storm-parsers/CMakeLists.txt | 42 +++++++++++ .../api/model_descriptions.cpp | 6 +- .../api/model_descriptions.h | 0 src/storm-parsers/api/properties.cpp | 71 +++++++++++++++++++ src/storm-parsers/api/properties.h | 43 +++++++++++ src/storm-parsers/api/storm-parsers.h | 4 ++ .../AtomicPropositionLabelingParser.cpp | 4 +- .../parser/AtomicPropositionLabelingParser.h | 0 .../parser/AutoParser.cpp | 10 +-- .../parser/AutoParser.h | 0 .../parser/DeterministicModelParser.cpp | 8 +-- .../parser/DeterministicModelParser.h | 0 .../DeterministicSparseTransitionParser.cpp | 4 +- .../DeterministicSparseTransitionParser.h | 0 .../parser/DirectEncodingParser.cpp | 2 +- .../parser/DirectEncodingParser.h | 2 +- .../parser/ExpressionCreator.cpp | 0 .../parser/ExpressionCreator.h | 2 +- .../parser/ExpressionParser.cpp | 4 +- .../parser/ExpressionParser.h | 4 +- .../parser/FormulaParser.cpp | 4 +- .../parser/FormulaParser.h | 4 +- .../parser/FormulaParserGrammar.cpp | 0 .../parser/FormulaParserGrammar.h | 4 +- .../parser/ImcaMarkovAutomatonParser.cpp | 2 +- .../parser/ImcaMarkovAutomatonParser.h | 2 +- .../parser/JaniParser.cpp | 0 .../parser/JaniParser.h | 0 .../parser/KeyValueParser.cpp | 0 .../parser/KeyValueParser.h | 0 .../parser/MappedFile.cpp | 2 +- .../parser/MappedFile.h | 0 .../parser/MarkovAutomatonParser.cpp | 0 .../parser/MarkovAutomatonParser.h | 2 +- .../MarkovAutomatonSparseTransitionParser.cpp | 2 +- .../MarkovAutomatonSparseTransitionParser.h | 0 .../parser/NondeterministicModelParser.cpp | 8 +-- .../parser/NondeterministicModelParser.h | 0 ...NondeterministicSparseTransitionParser.cpp | 4 +- .../NondeterministicSparseTransitionParser.h | 0 .../parser/PrismParser.cpp | 4 +- .../parser/PrismParser.h | 4 +- .../parser/ReadValues.h | 0 .../parser/SparseChoiceLabelingParser.cpp | 4 +- .../parser/SparseChoiceLabelingParser.h | 0 .../parser/SparseItemLabelingParser.cpp | 4 +- .../parser/SparseItemLabelingParser.h | 2 +- .../parser/SparseStateRewardParser.cpp | 4 +- .../parser/SparseStateRewardParser.h | 0 .../parser/SpiritErrorHandler.h | 2 +- .../parser/SpiritParserDefinitions.h | 0 .../parser/ValueParser.cpp | 2 +- .../parser/ValueParser.h | 2 +- src/storm-pgcl/parser/PgclParser.h | 6 +- src/storm/CMakeLists.txt | 2 - src/storm/api/builder.h | 6 +- src/storm/api/properties.cpp | 51 ------------- src/storm/api/properties.h | 12 +--- src/storm/api/storm.h | 1 - src/test/storm-pars/CMakeLists.txt | 2 +- .../ParametricDtmcPrctlModelCheckerTest.cpp | 6 +- .../SparseDtmcParameterLiftingTest.cpp | 2 + .../SparseMdpParameterLiftingTest.cpp | 2 + ...licParametricDtmcPrctlModelCheckerTest.cpp | 4 +- .../utility/ModelInstantiatorTest.cpp | 1 + src/test/storm/CMakeLists.txt | 2 +- .../storm/abstraction/PrismMenuGameTest.cpp | 2 +- .../storm/builder/DdJaniModelBuilderTest.cpp | 2 +- .../storm/builder/DdPrismModelBuilderTest.cpp | 2 +- .../builder/ExplicitJaniModelBuilderTest.cpp | 2 +- .../ExplicitJitJaniModelBuilderTest.cpp | 2 +- .../builder/ExplicitPrismModelBuilderTest.cpp | 2 +- src/test/storm/logic/FragmentCheckerTest.cpp | 2 +- .../ConditionalDtmcPrctlModelCheckerTest.cpp | 4 +- .../modelchecker/CtmcCslModelCheckerTest.cpp | 7 +- .../DtmcPrctlModelCheckerTest.cpp | 7 +- .../ExplicitDtmcPrctlModelCheckerTest.cpp | 6 +- .../ExplicitMdpPrctlModelCheckerTest.cpp | 6 +- .../GameBasedDtmcModelCheckerTest.cpp | 4 +- .../GameBasedMdpModelCheckerTest.cpp | 4 +- .../LraDtmcPrctlModelCheckerTest.cpp | 4 +- .../LraMdpPrctlModelCheckerTest.cpp | 4 +- .../modelchecker/MdpPrctlModelCheckerTest.cpp | 3 +- ...ulerGenerationMdpPrctlModelCheckerTest.cpp | 6 +- .../SparseDtmcEliminationModelCheckerTest.cpp | 4 +- ...tmcMultiDimensionalRewardUnfoldingTest.cpp | 1 + .../SparseExplorationModelCheckerTest.cpp | 4 +- ...arseMaCbMultiObjectiveModelCheckerTest.cpp | 1 + ...seMaPcaaMultiObjectiveModelCheckerTest.cpp | 1 + ...rseMdpCbMultiObjectiveModelCheckerTest.cpp | 1 + ...MdpMultiDimensionalRewardUnfoldingTest.cpp | 1 + ...eMdpPcaaMultiObjectiveModelCheckerTest.cpp | 1 + src/test/storm/parser/AutoParserTest.cpp | 2 +- .../parser/DeterministicModelParserTest.cpp | 2 +- ...eterministicSparseTransitionParserTest.cpp | 2 +- .../storm/parser/DirectEncodingParserTest.cpp | 2 +- src/test/storm/parser/FormulaParserTest.cpp | 2 +- src/test/storm/parser/MappedFileTest.cpp | 2 +- .../parser/MarkovAutomatonParserTest.cpp | 2 +- ...kovAutomatonSparseTransitionParserTest.cpp | 4 +- .../NondeterministicModelParserTest.cpp | 2 +- ...eterministicSparseTransitionParserTest.cpp | 2 +- src/test/storm/parser/PrismParserTest.cpp | 2 +- .../parser/SparseItemLabelingParserTest.cpp | 2 +- .../parser/SparseStateRewardParserTest.cpp | 2 +- .../MilpPermissiveSchedulerTest.cpp | 4 +- .../SmtPermissiveSchedulerTest.cpp | 4 +- ...sticModelBisimulationDecompositionTest.cpp | 4 +- src/test/storm/storage/JaniModelTest.cpp | 2 +- .../MaximalEndComponentDecompositionTest.cpp | 4 +- ...sticModelBisimulationDecompositionTest.cpp | 4 +- src/test/storm/storage/PrismProgramTest.cpp | 2 +- ...glyConnectedComponentDecompositionTest.cpp | 2 +- .../SymbolicBisimulationDecompositionTest.cpp | 6 +- src/test/storm/utility/GraphTest.cpp | 2 +- src/test/storm/utility/KSPTest.cpp | 2 +- 124 files changed, 322 insertions(+), 206 deletions(-) create mode 100644 src/storm-parsers/CMakeLists.txt rename src/{storm => storm-parsers}/api/model_descriptions.cpp (88%) rename src/{storm => storm-parsers}/api/model_descriptions.h (100%) create mode 100644 src/storm-parsers/api/properties.cpp create mode 100644 src/storm-parsers/api/properties.h create mode 100644 src/storm-parsers/api/storm-parsers.h rename src/{storm => storm-parsers}/parser/AtomicPropositionLabelingParser.cpp (98%) rename src/{storm => storm-parsers}/parser/AtomicPropositionLabelingParser.h (100%) rename src/{storm => storm-parsers}/parser/AutoParser.cpp (95%) rename src/{storm => storm-parsers}/parser/AutoParser.h (100%) rename src/{storm => storm-parsers}/parser/DeterministicModelParser.cpp (95%) rename src/{storm => storm-parsers}/parser/DeterministicModelParser.h (100%) rename src/{storm => storm-parsers}/parser/DeterministicSparseTransitionParser.cpp (99%) rename src/{storm => storm-parsers}/parser/DeterministicSparseTransitionParser.h (100%) rename src/{storm => storm-parsers}/parser/DirectEncodingParser.cpp (99%) rename src/{storm => storm-parsers}/parser/DirectEncodingParser.h (97%) rename src/{storm => storm-parsers}/parser/ExpressionCreator.cpp (100%) rename src/{storm => storm-parsers}/parser/ExpressionCreator.h (98%) rename src/{storm => storm-parsers}/parser/ExpressionParser.cpp (99%) rename src/{storm => storm-parsers}/parser/ExpressionParser.h (99%) rename src/{storm => storm-parsers}/parser/FormulaParser.cpp (98%) rename src/{storm => storm-parsers}/parser/FormulaParser.h (96%) rename src/{storm => storm-parsers}/parser/FormulaParserGrammar.cpp (100%) rename src/{storm => storm-parsers}/parser/FormulaParserGrammar.h (99%) rename src/{storm => storm-parsers}/parser/ImcaMarkovAutomatonParser.cpp (99%) rename src/{storm => storm-parsers}/parser/ImcaMarkovAutomatonParser.h (98%) rename src/{storm => storm-parsers}/parser/JaniParser.cpp (100%) rename src/{storm => storm-parsers}/parser/JaniParser.h (100%) rename src/{storm => storm-parsers}/parser/KeyValueParser.cpp (100%) rename src/{storm => storm-parsers}/parser/KeyValueParser.h (100%) rename src/{storm => storm-parsers}/parser/MappedFile.cpp (98%) rename src/{storm => storm-parsers}/parser/MappedFile.h (100%) rename src/{storm => storm-parsers}/parser/MarkovAutomatonParser.cpp (100%) rename src/{storm => storm-parsers}/parser/MarkovAutomatonParser.h (96%) rename src/{storm => storm-parsers}/parser/MarkovAutomatonSparseTransitionParser.cpp (99%) rename src/{storm => storm-parsers}/parser/MarkovAutomatonSparseTransitionParser.h (100%) rename src/{storm => storm-parsers}/parser/NondeterministicModelParser.cpp (93%) rename src/{storm => storm-parsers}/parser/NondeterministicModelParser.h (100%) rename src/{storm => storm-parsers}/parser/NondeterministicSparseTransitionParser.cpp (99%) rename src/{storm => storm-parsers}/parser/NondeterministicSparseTransitionParser.h (100%) rename src/{storm => storm-parsers}/parser/PrismParser.cpp (99%) rename src/{storm => storm-parsers}/parser/PrismParser.h (99%) rename src/{storm => storm-parsers}/parser/ReadValues.h (100%) rename src/{storm => storm-parsers}/parser/SparseChoiceLabelingParser.cpp (97%) rename src/{storm => storm-parsers}/parser/SparseChoiceLabelingParser.h (100%) rename src/{storm => storm-parsers}/parser/SparseItemLabelingParser.cpp (99%) rename src/{storm => storm-parsers}/parser/SparseItemLabelingParser.h (98%) rename src/{storm => storm-parsers}/parser/SparseStateRewardParser.cpp (96%) rename src/{storm => storm-parsers}/parser/SparseStateRewardParser.h (100%) rename src/{storm => storm-parsers}/parser/SpiritErrorHandler.h (95%) rename src/{storm => storm-parsers}/parser/SpiritParserDefinitions.h (100%) rename src/{storm => storm-parsers}/parser/ValueParser.cpp (96%) rename src/{storm => storm-parsers}/parser/ValueParser.h (97%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0f277386d..7239a9676 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -6,6 +6,7 @@ add_custom_target(binaries) add_subdirectory(storm) add_subdirectory(storm-counterexamples) +add_subdirectory(storm-parsers) add_subdirectory(storm-cli-utilities) add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl-cli) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt index 5e37b5db4..de4c0fde1 100644 --- a/src/storm-cli-utilities/CMakeLists.txt +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -17,7 +17,7 @@ set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-cli-utilities) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples) +target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-parsers) # Install storm headers to include directory. foreach(HEADER ${STORM_CLI_UTIL_HEADERS}) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index b57818c08..41faf8732 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -3,6 +3,7 @@ #include "storm/api/storm.h" #include "storm-counterexamples/api/counterexamples.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/utility/resources.h" #include "storm/utility/file.h" diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index ce31be5b8..395985f7e 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -7,6 +7,8 @@ #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/GeneralSettings.h" + +#include "storm-parsers/api/storm-parsers.h" #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index c56540edd..f956d8cb9 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -3,12 +3,12 @@ #include #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/builder/DFTBuilder.h" -#include "storm/parser/ValueParser.h" +#include "storm-parsers/parser/ValueParser.h" namespace storm { diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index 5517d85e1..3b6812a76 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -3,7 +3,7 @@ #include #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm-dft/storage/dft/DFT.h" diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 602b353a0..99d60b0d7 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -14,7 +14,7 @@ #include "api/storm.h" #include "storm-cli-utilities/cli.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/jani/Model.h" diff --git a/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp b/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp index 1960a623a..23ba78594 100644 --- a/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp +++ b/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp @@ -5,7 +5,7 @@ //#include "storm/utility/macros.h" //#include "storm/exceptions/NotImplementedException.h" //#include "storm/storage/expressions/ExpressionManager.h" -//#include "storm/parser/FormulaParser.h" +//#include "storm-parsers/parser/FormulaParser.h" //#include "storm/storage/expressions/ExpressionEvaluator.h" // //namespace storm { diff --git a/src/storm-parsers/CMakeLists.txt b/src/storm-parsers/CMakeLists.txt new file mode 100644 index 000000000..d459345e4 --- /dev/null +++ b/src/storm-parsers/CMakeLists.txt @@ -0,0 +1,42 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.h ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-parsers) + + + +file(GLOB_RECURSE STORM_PARSER_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.cpp) +file(GLOB_RECURSE STORM_PARSER_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.h) + + +# Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation +SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm-parsers/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0) +# Create storm-dft. +add_library(storm-parsers SHARED ${STORM_PARSER_SOURCES} ${STORM_PARSER_HEADERS}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-parsers PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-parsers) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-parsers PUBLIC storm) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_PARSER_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_PARSER_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_parser_headers DEPENDS ${STORM_PARSER_OUTPUT_HEADERS} ${STORM_PARSER_HEADERS}) +add_dependencies(storm-parsers copy_storm_parser_headers) + +# installation +install(TARGETS storm-parsers EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp similarity index 88% rename from src/storm/api/model_descriptions.cpp rename to src/storm-parsers/api/model_descriptions.cpp index 76ce24116..a440dffef 100644 --- a/src/storm/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -1,7 +1,7 @@ -#include "storm/api/model_descriptions.h" +#include "model_descriptions.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/JaniParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/JaniParser.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" diff --git a/src/storm/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h similarity index 100% rename from src/storm/api/model_descriptions.h rename to src/storm-parsers/api/model_descriptions.h diff --git a/src/storm-parsers/api/properties.cpp b/src/storm-parsers/api/properties.cpp new file mode 100644 index 000000000..d5349544d --- /dev/null +++ b/src/storm-parsers/api/properties.cpp @@ -0,0 +1,71 @@ + + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/api/properties.h" + + +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/prism/Program.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" + +#include "storm/logic/Formula.h" + +#include "storm/utility/cli.h" + + +namespace storm { + namespace api { + + boost::optional > parsePropertyFilter(std::string const &propertyFilter) { + if (propertyFilter == "all") { + return boost::none; + } + std::vector propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter); + std::set propertyNameSet(propertyNames.begin(), propertyNames.end()); + return propertyNameSet; + } + + std::vector parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional > const &propertyFilter) { + // If the given property is a file, we parse it as a file, otherwise we assume it's a property. + std::vector properties; + if (std::ifstream(inputString).good()) { + STORM_LOG_INFO("Loading properties from file: " << inputString << std::endl); + properties = formulaParser.parseFromFile(inputString); + } else { + properties = formulaParser.parseFromString(inputString); + } + + return filterProperties(properties, propertyFilter); + } + + std::vector parseProperties(std::string const &inputString, boost::optional > const &propertyFilter) { + auto exprManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(exprManager); + return parseProperties(formulaParser, inputString, propertyFilter); + } + + std::vector parsePropertiesForJaniModel(std::string const &inputString, storm::jani::Model const &model, boost::optional > const &propertyFilter) { + storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer()); + auto formulas = parseProperties(formulaParser, inputString, propertyFilter); + return substituteConstantsInProperties(formulas, model.getConstantsSubstitution()); + } + + std::vector parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional > const &propertyFilter) { + storm::parser::FormulaParser formulaParser(program); + auto formulas = parseProperties(formulaParser, inputString, propertyFilter); + return substituteConstantsInProperties(formulas, program.getConstantsSubstitution()); + } + + std::vector parsePropertiesForSymbolicModelDescription(std::string const &inputString, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional > const &propertyFilter) { + std::vector result; + if (modelDescription.isPrismProgram()) { + result = storm::api::parsePropertiesForPrismProgram(inputString, modelDescription.asPrismProgram(), propertyFilter); + } else { + STORM_LOG_ASSERT(modelDescription.isJaniModel(), "Unknown model description type."); + result = storm::api::parsePropertiesForJaniModel(inputString, modelDescription.asJaniModel(), propertyFilter); + } + return result; + } + } +} \ No newline at end of file diff --git a/src/storm-parsers/api/properties.h b/src/storm-parsers/api/properties.h new file mode 100644 index 000000000..81d37d965 --- /dev/null +++ b/src/storm-parsers/api/properties.h @@ -0,0 +1,43 @@ +#pragma once + +#include +#include +#include +#include +#include +#include + +namespace storm { + namespace parser { + class FormulaParser; + } + namespace jani { + class Property; + class Model; + } + namespace expressions { + class Variable; + class Expression; + } + namespace prism { + class Program; + } + namespace storage { + class SymbolicModelDescription; + } + namespace logic { + class Formula; + } + + namespace api { + boost::optional> parsePropertyFilter(std::string const& propertyFilter); + + // Parsing properties. + std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter = boost::none); + std::vector parseProperties(std::string const& inputString, boost::optional> const& propertyFilter = boost::none); + std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter = boost::none); + std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter = boost::none); + std::vector parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& propertyFilter = boost::none); + + } +} diff --git a/src/storm-parsers/api/storm-parsers.h b/src/storm-parsers/api/storm-parsers.h new file mode 100644 index 000000000..b88188976 --- /dev/null +++ b/src/storm-parsers/api/storm-parsers.h @@ -0,0 +1,4 @@ +#pragma once + +#include "storm-parsers/api/model_descriptions.h" +#include "storm-parsers/api/properties.h" \ No newline at end of file diff --git a/src/storm/parser/AtomicPropositionLabelingParser.cpp b/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp similarity index 98% rename from src/storm/parser/AtomicPropositionLabelingParser.cpp rename to src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp index 4d55b4fe8..a8afc93d7 100644 --- a/src/storm/parser/AtomicPropositionLabelingParser.cpp +++ b/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp @@ -5,14 +5,14 @@ * Author: Gereon Kremer */ -#include "storm/parser/AtomicPropositionLabelingParser.h" +#include "storm-parsers/parser/AtomicPropositionLabelingParser.h" #include #include #include #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/storm/parser/AtomicPropositionLabelingParser.h b/src/storm-parsers/parser/AtomicPropositionLabelingParser.h similarity index 100% rename from src/storm/parser/AtomicPropositionLabelingParser.h rename to src/storm-parsers/parser/AtomicPropositionLabelingParser.h diff --git a/src/storm/parser/AutoParser.cpp b/src/storm-parsers/parser/AutoParser.cpp similarity index 95% rename from src/storm/parser/AutoParser.cpp rename to src/storm-parsers/parser/AutoParser.cpp index 896c4215e..9e96af5e6 100644 --- a/src/storm/parser/AutoParser.cpp +++ b/src/storm-parsers/parser/AutoParser.cpp @@ -1,12 +1,12 @@ -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" -#include "storm/parser/DeterministicModelParser.h" -#include "storm/parser/NondeterministicModelParser.h" -#include "storm/parser/MarkovAutomatonParser.h" +#include "storm-parsers/parser/DeterministicModelParser.h" +#include "storm-parsers/parser/NondeterministicModelParser.h" +#include "storm-parsers/parser/MarkovAutomatonParser.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm/parser/AutoParser.h b/src/storm-parsers/parser/AutoParser.h similarity index 100% rename from src/storm/parser/AutoParser.h rename to src/storm-parsers/parser/AutoParser.h diff --git a/src/storm/parser/DeterministicModelParser.cpp b/src/storm-parsers/parser/DeterministicModelParser.cpp similarity index 95% rename from src/storm/parser/DeterministicModelParser.cpp rename to src/storm-parsers/parser/DeterministicModelParser.cpp index cfe5a16df..6b81c0630 100644 --- a/src/storm/parser/DeterministicModelParser.cpp +++ b/src/storm-parsers/parser/DeterministicModelParser.cpp @@ -1,13 +1,13 @@ -#include "storm/parser/DeterministicModelParser.h" +#include "storm-parsers/parser/DeterministicModelParser.h" #include #include #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/DeterministicSparseTransitionParser.h" -#include "storm/parser/SparseItemLabelingParser.h" -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/DeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm/parser/DeterministicModelParser.h b/src/storm-parsers/parser/DeterministicModelParser.h similarity index 100% rename from src/storm/parser/DeterministicModelParser.h rename to src/storm-parsers/parser/DeterministicModelParser.h diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp similarity index 99% rename from src/storm/parser/DeterministicSparseTransitionParser.cpp rename to src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp index 540371f74..229cc3c2e 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/DeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/DeterministicSparseTransitionParser.h" #include #include @@ -9,7 +9,7 @@ #include "storm/utility/constants.h" #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" diff --git a/src/storm/parser/DeterministicSparseTransitionParser.h b/src/storm-parsers/parser/DeterministicSparseTransitionParser.h similarity index 100% rename from src/storm/parser/DeterministicSparseTransitionParser.h rename to src/storm-parsers/parser/DeterministicSparseTransitionParser.h diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp similarity index 99% rename from src/storm/parser/DirectEncodingParser.cpp rename to src/storm-parsers/parser/DirectEncodingParser.cpp index 93d8a60f2..da4cd5228 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/DirectEncodingParser.h" +#include "storm-parsers/parser/DirectEncodingParser.h" #include #include diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm-parsers/parser/DirectEncodingParser.h similarity index 97% rename from src/storm/parser/DirectEncodingParser.h rename to src/storm-parsers/parser/DirectEncodingParser.h index 456445e1c..f025b8dfc 100644 --- a/src/storm/parser/DirectEncodingParser.h +++ b/src/storm-parsers/parser/DirectEncodingParser.h @@ -1,7 +1,7 @@ #ifndef STORM_PARSER_DIRECTENCODINGPARSER_H_ #define STORM_PARSER_DIRECTENCODINGPARSER_H_ -#include "storm/parser/ValueParser.h" +#include "storm-parsers/parser/ValueParser.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/storage/sparse/ModelComponents.h" diff --git a/src/storm/parser/ExpressionCreator.cpp b/src/storm-parsers/parser/ExpressionCreator.cpp similarity index 100% rename from src/storm/parser/ExpressionCreator.cpp rename to src/storm-parsers/parser/ExpressionCreator.cpp diff --git a/src/storm/parser/ExpressionCreator.h b/src/storm-parsers/parser/ExpressionCreator.h similarity index 98% rename from src/storm/parser/ExpressionCreator.h rename to src/storm-parsers/parser/ExpressionCreator.h index 20bcc5854..814dc964a 100644 --- a/src/storm/parser/ExpressionCreator.h +++ b/src/storm-parsers/parser/ExpressionCreator.h @@ -1,7 +1,7 @@ #pragma once #include // Very ugly, but currently we would like to have the symbol table here. -#include "storm/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" #include #include "storm/adapters/RationalNumberAdapter.h" diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm-parsers/parser/ExpressionParser.cpp similarity index 99% rename from src/storm/parser/ExpressionParser.cpp rename to src/storm-parsers/parser/ExpressionParser.cpp index 64e185b54..d1d6dcaf0 100644 --- a/src/storm/parser/ExpressionParser.cpp +++ b/src/storm-parsers/parser/ExpressionParser.cpp @@ -1,10 +1,10 @@ -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/constants.h" -#include "storm/parser/ExpressionCreator.h" +#include "storm-parsers/parser/ExpressionCreator.h" #include "storm/storage/expressions/Expression.h" diff --git a/src/storm/parser/ExpressionParser.h b/src/storm-parsers/parser/ExpressionParser.h similarity index 99% rename from src/storm/parser/ExpressionParser.h rename to src/storm-parsers/parser/ExpressionParser.h index cb415c53e..4fa075adc 100644 --- a/src/storm/parser/ExpressionParser.h +++ b/src/storm-parsers/parser/ExpressionParser.h @@ -2,8 +2,8 @@ #include -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/storage/expressions/OperatorType.h" #include "storm/adapters/RationalNumberAdapter.h" diff --git a/src/storm/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp similarity index 98% rename from src/storm/parser/FormulaParser.cpp rename to src/storm-parsers/parser/FormulaParser.cpp index d8b9c2df2..0f44d469b 100644 --- a/src/storm/parser/FormulaParser.cpp +++ b/src/storm-parsers/parser/FormulaParser.cpp @@ -1,8 +1,8 @@ -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/storage/prism/Program.h" diff --git a/src/storm/parser/FormulaParser.h b/src/storm-parsers/parser/FormulaParser.h similarity index 96% rename from src/storm/parser/FormulaParser.h rename to src/storm-parsers/parser/FormulaParser.h index d9c06fa92..49c78a720 100644 --- a/src/storm/parser/FormulaParser.h +++ b/src/storm-parsers/parser/FormulaParser.h @@ -3,8 +3,8 @@ #include -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/jani/Property.h" #include "storm/storage/expressions/Expression.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp similarity index 100% rename from src/storm/parser/FormulaParserGrammar.cpp rename to src/storm-parsers/parser/FormulaParserGrammar.cpp diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h similarity index 99% rename from src/storm/parser/FormulaParserGrammar.h rename to src/storm-parsers/parser/FormulaParserGrammar.h index dd9a3a06f..c9d5ae020 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -3,11 +3,11 @@ #include #include -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/jani/Property.h" #include "storm/logic/Formulas.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/modelchecker/results/FilterType.h" diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.cpp b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp similarity index 99% rename from src/storm/parser/ImcaMarkovAutomatonParser.cpp rename to src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp index f55d09219..0cbf917f1 100644 --- a/src/storm/parser/ImcaMarkovAutomatonParser.cpp +++ b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/ImcaMarkovAutomatonParser.h" +#include "storm-parsers/parser/ImcaMarkovAutomatonParser.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BuildSettings.h" diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.h b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.h similarity index 98% rename from src/storm/parser/ImcaMarkovAutomatonParser.h rename to src/storm-parsers/parser/ImcaMarkovAutomatonParser.h index f2820242e..b5c7beded 100644 --- a/src/storm/parser/ImcaMarkovAutomatonParser.h +++ b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.h @@ -7,7 +7,7 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/generator/StateBehavior.h" -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" namespace storm { namespace parser { diff --git a/src/storm/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp similarity index 100% rename from src/storm/parser/JaniParser.cpp rename to src/storm-parsers/parser/JaniParser.cpp diff --git a/src/storm/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h similarity index 100% rename from src/storm/parser/JaniParser.h rename to src/storm-parsers/parser/JaniParser.h diff --git a/src/storm/parser/KeyValueParser.cpp b/src/storm-parsers/parser/KeyValueParser.cpp similarity index 100% rename from src/storm/parser/KeyValueParser.cpp rename to src/storm-parsers/parser/KeyValueParser.cpp diff --git a/src/storm/parser/KeyValueParser.h b/src/storm-parsers/parser/KeyValueParser.h similarity index 100% rename from src/storm/parser/KeyValueParser.h rename to src/storm-parsers/parser/KeyValueParser.h diff --git a/src/storm/parser/MappedFile.cpp b/src/storm-parsers/parser/MappedFile.cpp similarity index 98% rename from src/storm/parser/MappedFile.cpp rename to src/storm-parsers/parser/MappedFile.cpp index 5b9f02714..d28e8e927 100644 --- a/src/storm/parser/MappedFile.cpp +++ b/src/storm-parsers/parser/MappedFile.cpp @@ -5,7 +5,7 @@ * Author: Manuel Sascha Weiand */ -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include #include diff --git a/src/storm/parser/MappedFile.h b/src/storm-parsers/parser/MappedFile.h similarity index 100% rename from src/storm/parser/MappedFile.h rename to src/storm-parsers/parser/MappedFile.h diff --git a/src/storm/parser/MarkovAutomatonParser.cpp b/src/storm-parsers/parser/MarkovAutomatonParser.cpp similarity index 100% rename from src/storm/parser/MarkovAutomatonParser.cpp rename to src/storm-parsers/parser/MarkovAutomatonParser.cpp diff --git a/src/storm/parser/MarkovAutomatonParser.h b/src/storm-parsers/parser/MarkovAutomatonParser.h similarity index 96% rename from src/storm/parser/MarkovAutomatonParser.h rename to src/storm-parsers/parser/MarkovAutomatonParser.h index 763ece141..1f2087674 100644 --- a/src/storm/parser/MarkovAutomatonParser.h +++ b/src/storm-parsers/parser/MarkovAutomatonParser.h @@ -2,7 +2,7 @@ #define STORM_PARSER_MARKOVAUTOMATONPARSER_H_ #include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/parser/MarkovAutomatonSparseTransitionParser.h" +#include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h" namespace storm { namespace parser { diff --git a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp similarity index 99% rename from src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp rename to src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp index 25b62a2e2..9acd151b0 100644 --- a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -4,7 +4,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/cstring.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/MarkovAutomatonSparseTransitionParser.h b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h similarity index 100% rename from src/storm/parser/MarkovAutomatonSparseTransitionParser.h rename to src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h diff --git a/src/storm/parser/NondeterministicModelParser.cpp b/src/storm-parsers/parser/NondeterministicModelParser.cpp similarity index 93% rename from src/storm/parser/NondeterministicModelParser.cpp rename to src/storm-parsers/parser/NondeterministicModelParser.cpp index c107803eb..b26626fb0 100644 --- a/src/storm/parser/NondeterministicModelParser.cpp +++ b/src/storm-parsers/parser/NondeterministicModelParser.cpp @@ -1,13 +1,13 @@ -#include "storm/parser/NondeterministicModelParser.h" +#include "storm-parsers/parser/NondeterministicModelParser.h" #include #include #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/NondeterministicSparseTransitionParser.h" -#include "storm/parser/SparseItemLabelingParser.h" -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/NondeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/NondeterministicModelParser.h b/src/storm-parsers/parser/NondeterministicModelParser.h similarity index 100% rename from src/storm/parser/NondeterministicModelParser.h rename to src/storm-parsers/parser/NondeterministicModelParser.h diff --git a/src/storm/parser/NondeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp similarity index 99% rename from src/storm/parser/NondeterministicSparseTransitionParser.cpp rename to src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp index cb941aec5..56b00070c 100644 --- a/src/storm/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp @@ -1,8 +1,8 @@ -#include "storm/parser/NondeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/NondeterministicSparseTransitionParser.h" #include -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/storm/parser/NondeterministicSparseTransitionParser.h b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.h similarity index 100% rename from src/storm/parser/NondeterministicSparseTransitionParser.h rename to src/storm-parsers/parser/NondeterministicSparseTransitionParser.h diff --git a/src/storm/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp similarity index 99% rename from src/storm/parser/PrismParser.cpp rename to src/storm-parsers/parser/PrismParser.cpp index ca59981cb..5d76736f7 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/prism/Compositions.h" @@ -11,7 +11,7 @@ #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" namespace storm { namespace parser { diff --git a/src/storm/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h similarity index 99% rename from src/storm/parser/PrismParser.h rename to src/storm-parsers/parser/PrismParser.h index fe7f0bc83..38a112e9d 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -6,8 +6,8 @@ #include #include -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" diff --git a/src/storm/parser/ReadValues.h b/src/storm-parsers/parser/ReadValues.h similarity index 100% rename from src/storm/parser/ReadValues.h rename to src/storm-parsers/parser/ReadValues.h diff --git a/src/storm/parser/SparseChoiceLabelingParser.cpp b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp similarity index 97% rename from src/storm/parser/SparseChoiceLabelingParser.cpp rename to src/storm-parsers/parser/SparseChoiceLabelingParser.cpp index b51e8b97c..452045319 100644 --- a/src/storm/parser/SparseChoiceLabelingParser.cpp +++ b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp @@ -1,10 +1,10 @@ -#include "storm/parser/SparseChoiceLabelingParser.h" +#include "storm-parsers/parser/SparseChoiceLabelingParser.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/FileIoException.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/cstring.h" namespace storm { diff --git a/src/storm/parser/SparseChoiceLabelingParser.h b/src/storm-parsers/parser/SparseChoiceLabelingParser.h similarity index 100% rename from src/storm/parser/SparseChoiceLabelingParser.h rename to src/storm-parsers/parser/SparseChoiceLabelingParser.h diff --git a/src/storm/parser/SparseItemLabelingParser.cpp b/src/storm-parsers/parser/SparseItemLabelingParser.cpp similarity index 99% rename from src/storm/parser/SparseItemLabelingParser.cpp rename to src/storm-parsers/parser/SparseItemLabelingParser.cpp index 2e98e4673..9e5e7b154 100644 --- a/src/storm/parser/SparseItemLabelingParser.cpp +++ b/src/storm-parsers/parser/SparseItemLabelingParser.cpp @@ -1,11 +1,11 @@ -#include "storm/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" #include #include #include #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm/parser/SparseItemLabelingParser.h b/src/storm-parsers/parser/SparseItemLabelingParser.h similarity index 98% rename from src/storm/parser/SparseItemLabelingParser.h rename to src/storm-parsers/parser/SparseItemLabelingParser.h index 4b901ab82..97c30cc25 100644 --- a/src/storm/parser/SparseItemLabelingParser.h +++ b/src/storm-parsers/parser/SparseItemLabelingParser.h @@ -4,7 +4,7 @@ #include #include -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/ChoiceLabeling.h" diff --git a/src/storm/parser/SparseStateRewardParser.cpp b/src/storm-parsers/parser/SparseStateRewardParser.cpp similarity index 96% rename from src/storm/parser/SparseStateRewardParser.cpp rename to src/storm-parsers/parser/SparseStateRewardParser.cpp index f42b4cbe8..acb67e9fb 100644 --- a/src/storm/parser/SparseStateRewardParser.cpp +++ b/src/storm-parsers/parser/SparseStateRewardParser.cpp @@ -1,11 +1,11 @@ #include -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/FileIoException.h" #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/SparseStateRewardParser.h b/src/storm-parsers/parser/SparseStateRewardParser.h similarity index 100% rename from src/storm/parser/SparseStateRewardParser.h rename to src/storm-parsers/parser/SparseStateRewardParser.h diff --git a/src/storm/parser/SpiritErrorHandler.h b/src/storm-parsers/parser/SpiritErrorHandler.h similarity index 95% rename from src/storm/parser/SpiritErrorHandler.h rename to src/storm-parsers/parser/SpiritErrorHandler.h index 34280e422..ab64008bc 100644 --- a/src/storm/parser/SpiritErrorHandler.h +++ b/src/storm-parsers/parser/SpiritErrorHandler.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm/parser/SpiritParserDefinitions.h b/src/storm-parsers/parser/SpiritParserDefinitions.h similarity index 100% rename from src/storm/parser/SpiritParserDefinitions.h rename to src/storm-parsers/parser/SpiritParserDefinitions.h diff --git a/src/storm/parser/ValueParser.cpp b/src/storm-parsers/parser/ValueParser.cpp similarity index 96% rename from src/storm/parser/ValueParser.cpp rename to src/storm-parsers/parser/ValueParser.cpp index 17495b0d9..61cd5c0ac 100644 --- a/src/storm/parser/ValueParser.cpp +++ b/src/storm-parsers/parser/ValueParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/ValueParser.h" +#include "storm-parsers/parser/ValueParser.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm/parser/ValueParser.h b/src/storm-parsers/parser/ValueParser.h similarity index 97% rename from src/storm/parser/ValueParser.h rename to src/storm-parsers/parser/ValueParser.h index db948b75e..626857a3e 100644 --- a/src/storm/parser/ValueParser.h +++ b/src/storm-parsers/parser/ValueParser.h @@ -2,7 +2,7 @@ #define STORM_PARSER_VALUEPARSER_H_ #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm-pgcl/parser/PgclParser.h b/src/storm-pgcl/parser/PgclParser.h index dfd75a810..0e31094b9 100755 --- a/src/storm-pgcl/parser/PgclParser.h +++ b/src/storm-pgcl/parser/PgclParser.h @@ -5,9 +5,9 @@ #include #include // Includes files for building and parsing the PGCL program -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/SpiritErrorHandler.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/Expression.h" #include "storm-pgcl/storage/pgcl/PgclProgram.h" diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 6a8cda64e..dcd1bb9f9 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -28,8 +28,6 @@ if (ADDITIONAL_LINK_DIRS) link_directories(${ADDITIONAL_LINK_DIRS}) endif(ADDITIONAL_LINK_DIRS) -# Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation -SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0) ############################################################################### ## diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 715e6e1ac..8aa2e2e17 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -1,8 +1,8 @@ #pragma once -#include "storm/parser/AutoParser.h" -#include "storm/parser/DirectEncodingParser.h" -#include "storm/parser/ImcaMarkovAutomatonParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/DirectEncodingParser.h" +#include "storm-parsers/parser/ImcaMarkovAutomatonParser.h" #include "storm/storage/SymbolicModelDescription.h" diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index 163679013..e5010d8b9 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -1,6 +1,5 @@ #include "storm/api/properties.h" -#include "storm/parser/FormulaParser.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/prism/Program.h" @@ -13,57 +12,7 @@ namespace storm { namespace api { - - boost::optional> parsePropertyFilter(std::string const& propertyFilter) { - if (propertyFilter == "all") { - return boost::none; - } - std::vector propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter); - std::set propertyNameSet(propertyNames.begin(), propertyNames.end()); - return propertyNameSet; - } - std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter) { - // If the given property is a file, we parse it as a file, otherwise we assume it's a property. - std::vector properties; - if (std::ifstream(inputString).good()) { - STORM_LOG_INFO("Loading properties from file: " << inputString << std::endl); - properties = formulaParser.parseFromFile(inputString); - } else { - properties = formulaParser.parseFromString(inputString); - } - - return filterProperties(properties, propertyFilter); - } - - std::vector parseProperties(std::string const& inputString, boost::optional> const& propertyFilter) { - auto exprManager = std::make_shared(); - storm::parser::FormulaParser formulaParser(exprManager); - return parseProperties(formulaParser, inputString, propertyFilter); - } - - std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter) { - storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer()); - auto formulas = parseProperties(formulaParser, inputString, propertyFilter); - return substituteConstantsInProperties(formulas, model.getConstantsSubstitution()); - } - - std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter) { - storm::parser::FormulaParser formulaParser(program); - auto formulas = parseProperties(formulaParser, inputString, propertyFilter); - return substituteConstantsInProperties(formulas, program.getConstantsSubstitution()); - } - - std::vector parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& propertyFilter) { - std::vector result; - if (modelDescription.isPrismProgram()) { - result = storm::api::parsePropertiesForPrismProgram(inputString, modelDescription.asPrismProgram(), propertyFilter); - } else { - STORM_LOG_ASSERT(modelDescription.isJaniModel(), "Unknown model description type."); - result = storm::api::parsePropertiesForJaniModel(inputString, modelDescription.asJaniModel(), propertyFilter); - } - return result; - } std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution) { std::vector preprocessedProperties; diff --git a/src/storm/api/properties.h b/src/storm/api/properties.h index c52073105..c0c878f48 100644 --- a/src/storm/api/properties.h +++ b/src/storm/api/properties.h @@ -8,9 +8,7 @@ #include namespace storm { - namespace parser { - class FormulaParser; - } + namespace jani { class Property; class Model; @@ -30,14 +28,6 @@ namespace storm { } namespace api { - boost::optional> parsePropertyFilter(std::string const& propertyFilter); - - // Parsing properties. - std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter = boost::none); - std::vector parseProperties(std::string const& inputString, boost::optional> const& propertyFilter = boost::none); - std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter = boost::none); - std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter = boost::none); - std::vector parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& propertyFilter = boost::none); // Process properties. std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution); diff --git a/src/storm/api/storm.h b/src/storm/api/storm.h index d8f6aed82..0048bc315 100644 --- a/src/storm/api/storm.h +++ b/src/storm/api/storm.h @@ -1,6 +1,5 @@ #pragma once -#include "storm/api/model_descriptions.h" #include "storm/api/properties.h" #include "storm/api/builder.h" #include "storm/api/bisimulation.h" diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt index 0f2793553..28c5a391d 100644 --- a/src/test/storm-pars/CMakeLists.txt +++ b/src/test/storm-pars/CMakeLists.txt @@ -13,7 +13,7 @@ foreach (testsuite modelchecker utility) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-pars-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) - target_link_libraries(test-pars-${testsuite} storm-pars) + target_link_libraries(test-pars-${testsuite} storm-pars storm-parsers) target_link_libraries(test-pars-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) add_dependencies(test-pars-${testsuite} test-resources) diff --git a/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp index cf30285c5..91e08d2cf 100644 --- a/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp @@ -2,13 +2,13 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/api/builder.h" diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index dd6d59cf8..94bedf559 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -8,6 +8,8 @@ #include "storm-pars/api/storm-pars.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" + #include "storm/environment/solver/MinMaxSolverEnvironment.h" namespace { diff --git a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp index 3d3c97caa..48e71fd0b 100644 --- a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -8,6 +8,8 @@ #include "storm-pars/api/storm-pars.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" + #include "storm/environment/solver/MinMaxSolverEnvironment.h" namespace { diff --git a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp index de5e6f849..f23a23e4a 100644 --- a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/utility/solver.h" #include "storm/storage/SymbolicModelDescription.h" @@ -9,7 +9,7 @@ #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "storm/solver/SymbolicEliminationLinearEquationSolver.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/Dtmc.h" diff --git a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp index 1873a4436..fa7bb16eb 100644 --- a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp +++ b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp @@ -13,6 +13,7 @@ #include "storm-pars/utility/ModelInstantiator.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index 0ae2fc509..c745943b4 100644 --- a/src/test/storm/CMakeLists.txt +++ b/src/test/storm/CMakeLists.txt @@ -13,7 +13,7 @@ foreach (testsuite abstraction adapter builder logic modelchecker parser permiss file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) - target_link_libraries(test-${testsuite} storm) + target_link_libraries(test-${testsuite} storm storm-parsers) target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) add_dependencies(test-${testsuite} test-resources) diff --git a/src/test/storm/abstraction/PrismMenuGameTest.cpp b/src/test/storm/abstraction/PrismMenuGameTest.cpp index a200c1d68..96c484d99 100644 --- a/src/test/storm/abstraction/PrismMenuGameTest.cpp +++ b/src/test/storm/abstraction/PrismMenuGameTest.cpp @@ -3,7 +3,7 @@ #ifdef STORM_HAVE_MSAT -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/abstraction/MenuGameRefiner.h" #include "storm/abstraction/prism/PrismMenuGameAbstractor.h" diff --git a/src/test/storm/builder/DdJaniModelBuilderTest.cpp b/src/test/storm/builder/DdJaniModelBuilderTest.cpp index fa657a96f..1515b83e3 100644 --- a/src/test/storm/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/DdJaniModelBuilderTest.cpp @@ -10,7 +10,7 @@ #include "storm/storage/jani/Compositions.h" #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdJaniModelBuilder.h" #include "storm/settings/SettingMemento.h" diff --git a/src/test/storm/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp index 1ff4a79fe..a56aa1e12 100644 --- a/src/test/storm/builder/DdPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/DdPrismModelBuilderTest.cpp @@ -8,7 +8,7 @@ #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { diff --git a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp index 4f21c3a64..95b690e96 100644 --- a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp @@ -3,7 +3,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/generator/JaniNextStateGenerator.h" #include "storm/storage/jani/Model.h" diff --git a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp index 334735b02..c5c0eec05 100644 --- a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp @@ -3,7 +3,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/jit/ExplicitJitJaniModelBuilder.h" #include "storm/storage/jani/Model.h" diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index 8e5929618..65e1dff1d 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index c846f7f68..5adf50028 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/FragmentChecker.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp index c0972c474..fd124f456 100644 --- a/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp @@ -2,12 +2,12 @@ #include "test/storm_gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/api/builder.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index f2a790b9b..1b83be1c6 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -3,9 +3,10 @@ #include "storm-config.h" #include "storm/api/builder.h" -#include "storm/api/model_descriptions.h" +#include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/api/properties.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/EigenLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -18,7 +19,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/environment/solver/NativeSolverEnvironment.h" diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index ad6654ff4..f7f3b72a1 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -3,9 +3,10 @@ #include "storm-config.h" #include "storm/api/builder.h" -#include "storm/api/model_descriptions.h" +#include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/api/properties.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/EigenLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -19,7 +20,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/environment/solver/NativeSolverEnvironment.h" diff --git a/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp index 06b90270b..025bc8c45 100644 --- a/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" @@ -9,8 +9,8 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp index 91db98302..b295c397b 100644 --- a/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -10,8 +10,8 @@ #include "storm/environment/solver/MinMaxSolverEnvironment.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { diff --git a/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp index 2a4f64c4d..3511aabec 100644 --- a/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp @@ -1,13 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/utility/solver.h" #include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/Dtmc.h" diff --git a/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp index 960cc56bc..225bf81b4 100644 --- a/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/sparse/Model.h" @@ -13,6 +13,8 @@ #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" + #if defined STORM_HAVE_MSAT TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) { #else diff --git a/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp index 59c589cb1..c964628b9 100644 --- a/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/settings/SettingMemento.h" #include "storm/logic/Formulas.h" #include "storm/solver/NativeLinearEquationSolver.h" @@ -17,7 +17,7 @@ #include "storm/environment/solver/EigenSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/builder/ExplicitModelBuilder.h" namespace { diff --git a/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp index ed3abb16b..b05ebfb76 100644 --- a/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -12,7 +12,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::storage::SparseMatrixBuilder matrixBuilder; diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index e0741fa30..feb90d438 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -4,8 +4,9 @@ #include "test/storm_gtest.h" #include "storm/api/builder.h" -#include "storm/api/model_descriptions.h" +#include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/symbolic/Mdp.h" diff --git a/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 751a28ed2..6f82d6a47 100644 --- a/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -12,8 +12,8 @@ #include "storm/environment/solver/MinMaxSolverEnvironment.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" namespace { diff --git a/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 00c8b88e5..ed182bf2c 100644 --- a/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" @@ -10,7 +10,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" TEST(SparseDtmcEliminationModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew"); diff --git a/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp index 36ca41ff0..3a20c997b 100644 --- a/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp @@ -7,6 +7,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/constants.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) { diff --git a/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp index a1645e2a0..dc7d7a55a 100644 --- a/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp @@ -4,8 +4,8 @@ #include "storm/logic/Formulas.h" #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/ExplorationSettings.h" diff --git a/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp index e5843b4e1..4970fff9d 100644 --- a/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp @@ -9,6 +9,7 @@ #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" diff --git a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index d2c116358..58c8e7494 100644 --- a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -14,6 +14,7 @@ #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" diff --git a/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp index 7b2479ec3..f353092af 100644 --- a/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 3f73da77e..4880564b0 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -10,6 +10,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/constants.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" diff --git a/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 947cbde55..8e4cb084c 100644 --- a/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -10,6 +10,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { diff --git a/src/test/storm/parser/AutoParserTest.cpp b/src/test/storm/parser/AutoParserTest.cpp index 0ddd14894..96aa9cc60 100644 --- a/src/test/storm/parser/AutoParserTest.cpp +++ b/src/test/storm/parser/AutoParserTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/test/storm/parser/DeterministicModelParserTest.cpp b/src/test/storm/parser/DeterministicModelParserTest.cpp index b2f7ac9c2..bd5b0bf69 100644 --- a/src/test/storm/parser/DeterministicModelParserTest.cpp +++ b/src/test/storm/parser/DeterministicModelParserTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/DeterministicModelParser.h" +#include "storm-parsers/parser/DeterministicModelParser.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp index bd8e9e2f2..737d8ff04 100644 --- a/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/DeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/DeterministicSparseTransitionParser.h" #include "storm/storage/SparseMatrix.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/test/storm/parser/DirectEncodingParserTest.cpp b/src/test/storm/parser/DirectEncodingParserTest.cpp index 93bd34e04..c5716195b 100644 --- a/src/test/storm/parser/DirectEncodingParserTest.cpp +++ b/src/test/storm/parser/DirectEncodingParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/DirectEncodingParser.h" +#include "storm-parsers/parser/DirectEncodingParser.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" diff --git a/src/test/storm/parser/FormulaParserTest.cpp b/src/test/storm/parser/FormulaParserTest.cpp index 6269a082c..fd1206947 100644 --- a/src/test/storm/parser/FormulaParserTest.cpp +++ b/src/test/storm/parser/FormulaParserTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/FragmentSpecification.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/parser/MappedFileTest.cpp b/src/test/storm/parser/MappedFileTest.cpp index f33ee3aa2..362cbc899 100644 --- a/src/test/storm/parser/MappedFileTest.cpp +++ b/src/test/storm/parser/MappedFileTest.cpp @@ -9,7 +9,7 @@ #include "storm-config.h" #include -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/cstring.h" #include "storm/utility/file.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/MarkovAutomatonParserTest.cpp b/src/test/storm/parser/MarkovAutomatonParserTest.cpp index c31787087..3eb2dc3f7 100644 --- a/src/test/storm/parser/MarkovAutomatonParserTest.cpp +++ b/src/test/storm/parser/MarkovAutomatonParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/MarkovAutomatonParser.h" +#include "storm-parsers/parser/MarkovAutomatonParser.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/OutOfRangeException.h" diff --git a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp index 461b28a95..f29a5689d 100644 --- a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -12,9 +12,9 @@ #include -#include "storm/parser/MarkovAutomatonSparseTransitionParser.h" +#include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h" #include "storm/utility/cstring.h" -#include "storm/parser/MarkovAutomatonParser.h" +#include "storm-parsers/parser/MarkovAutomatonParser.h" #include "storm/settings/SettingMemento.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/NondeterministicModelParserTest.cpp b/src/test/storm/parser/NondeterministicModelParserTest.cpp index b700c56f4..8ed57b2b7 100644 --- a/src/test/storm/parser/NondeterministicModelParserTest.cpp +++ b/src/test/storm/parser/NondeterministicModelParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/NondeterministicModelParser.h" +#include "storm-parsers/parser/NondeterministicModelParser.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp index 77344834a..9c740144f 100644 --- a/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/NondeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/NondeterministicSparseTransitionParser.h" #include "storm/storage/SparseMatrix.h" #include "storm/settings/SettingMemento.h" diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index c86d90f63..4fe5735f5 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" TEST(PrismParser, StandardModelTest) { storm::prism::Program result; diff --git a/src/test/storm/parser/SparseItemLabelingParserTest.cpp b/src/test/storm/parser/SparseItemLabelingParserTest.cpp index 695b6837b..2f5cf3c0b 100644 --- a/src/test/storm/parser/SparseItemLabelingParserTest.cpp +++ b/src/test/storm/parser/SparseItemLabelingParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "storm/models/sparse/StateLabeling.h" -#include "storm/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" diff --git a/src/test/storm/parser/SparseStateRewardParserTest.cpp b/src/test/storm/parser/SparseStateRewardParserTest.cpp index d92203210..53524b3cd 100644 --- a/src/test/storm/parser/SparseStateRewardParserTest.cpp +++ b/src/test/storm/parser/SparseStateRewardParserTest.cpp @@ -10,7 +10,7 @@ #include -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" diff --git a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index 20707d33e..a6b0a34fd 100644 --- a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -1,8 +1,8 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/logic/Formulas.h" #include "storm/permissivesched/PermissiveSchedulers.h" diff --git a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index b19f82618..1b873a935 100644 --- a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -1,8 +1,8 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/permissivesched/PermissiveSchedulers.h" #include "storm/builder/ExplicitModelBuilder.h" diff --git a/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp index 3ebeca7a5..3341b1fe7 100644 --- a/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/test/storm/storage/JaniModelTest.cpp b/src/test/storm/storage/JaniModelTest.cpp index 7c7f393b3..c7a6b5c11 100644 --- a/src/test/storm/storage/JaniModelTest.cpp +++ b/src/test/storm/storage/JaniModelTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/utility/solver.h" diff --git a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp index 6e9718e6b..b30b5259b 100644 --- a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp +++ b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp @@ -1,13 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" TEST(MaximalEndComponentDecomposition, FullSystem1) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", ""); diff --git a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp index 596938852..d77fa8d64 100644 --- a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -1,8 +1,8 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/builder/ExplicitModelBuilder.h" diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp index 8525f03e2..e860fa997 100644 --- a/src/test/storm/storage/PrismProgramTest.cpp +++ b/src/test/storm/storage/PrismProgramTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/utility/solver.h" diff --git a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp index e447d2ec0..821b721a7 100644 --- a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp index d339bd027..64d2906d1 100644 --- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -1,8 +1,8 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/builder/DdPrismModelBuilder.h" @@ -19,7 +19,7 @@ #include "storm/solver/SymbolicMinMaxLinearEquationSolver.h" #include "storm/logic/Formulas.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/test/storm/utility/GraphTest.cpp b/src/test/storm/utility/GraphTest.cpp index ac646d99a..3098297c0 100644 --- a/src/test/storm/utility/GraphTest.cpp +++ b/src/test/storm/utility/GraphTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" diff --git a/src/test/storm/utility/KSPTest.cpp b/src/test/storm/utility/KSPTest.cpp index 5ac954314..dfe14e817 100644 --- a/src/test/storm/utility/KSPTest.cpp +++ b/src/test/storm/utility/KSPTest.cpp @@ -3,7 +3,7 @@ #include "storm/builder/ExplicitModelBuilder.h" #include "storm/models/sparse/Dtmc.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/graph.h" #include "storm/utility/shortestPaths.h" From 39698d6ecbe5d33c026259643f9b3566fc60c9c1 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 10 Jun 2018 21:01:14 +0200 Subject: [PATCH 15/29] fix install of storm-counterexamples --- src/storm-counterexamples/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storm-counterexamples/CMakeLists.txt b/src/storm-counterexamples/CMakeLists.txt index d01c4ceb7..2052930c6 100644 --- a/src/storm-counterexamples/CMakeLists.txt +++ b/src/storm-counterexamples/CMakeLists.txt @@ -20,7 +20,7 @@ set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) target_link_libraries(storm-counterexamples PUBLIC storm) # Install storm headers to include directory. -foreach(HEADER ${STORM_DFT_HEADERS}) +foreach(HEADER ${STORM_CEX_HEADERS}) string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) From 53238f43f753aa2a6a6786dd49215b9f39abc98c Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 10 Jun 2018 21:01:38 +0200 Subject: [PATCH 16/29] fixed some missing includes due to updated API --- src/storm-gspn-cli/storm-gspn.cpp | 3 +++ src/test/storm-dft/CMakeLists.txt | 2 +- src/test/storm-dft/api/DftModelCheckerTest.cpp | 1 + 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 99d60b0d7..46da4fea5 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -12,6 +12,8 @@ #include "storm/utility/initialize.h" #include "api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" #include "storm-cli-utilities/cli.h" #include "storm-parsers/parser/FormulaParser.h" @@ -27,6 +29,7 @@ #include "storm/exceptions/FileIoException.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/IOSettings.h" #include "storm-gspn/settings/modules/GSPNSettings.h" #include "storm-gspn/settings/modules/GSPNExportSettings.h" diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt index d461c2f9d..a0e96ee36 100644 --- a/src/test/storm-dft/CMakeLists.txt +++ b/src/test/storm-dft/CMakeLists.txt @@ -13,7 +13,7 @@ foreach (testsuite api) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) - target_link_libraries(test-dft-${testsuite} storm-dft) + target_link_libraries(test-dft-${testsuite} storm-dft storm-parsers) target_link_libraries(test-dft-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) add_dependencies(test-dft-${testsuite} test-resources) diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 5db58d60d..b4e9534f9 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "storm-dft/api/storm-dft.h" +#include "storm-parsers/api/storm-parsers.h" namespace { From 9e398ffaab09fec2bb4593d27982c4644371fdb4 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Jun 2018 15:07:42 +0200 Subject: [PATCH 17/29] Minor improvements for some CMake output --- CMakeLists.txt | 14 +++++++------- resources/3rdparty/CMakeLists.txt | 14 +++++++------- resources/3rdparty/carl/CMakeLists.txt | 4 ++-- 3 files changed, 16 insertions(+), 16 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ca3b9b7e..ee6c1117c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -86,7 +86,7 @@ foreach(p LIB BIN INCLUDE CMAKE) endif() endforeach() -message("CMAKE_INSTALL_DIR: ${CMAKE_INSTALL_DIR}") +message(STATUS "Storm - CMake install dir: ${CMAKE_INSTALL_DIR}") # If the STORM_DEVELOPER option was turned on, by default we target a debug version, otherwise a release version. if (STORM_DEVELOPER) @@ -153,15 +153,15 @@ elseif (WIN32) set(STATIC_EXT ".lib") set(LIB_PREFIX "") endif() -message(STATUS "Assuming extension for shared libraries: ${DYNAMIC_EXT}") -message(STATUS "Assuming extension for static libraries: ${STATIC_EXT}") +message(STATUS "Storm - Assuming extension for shared libraries: ${DYNAMIC_EXT}") +message(STATUS "Storm - Assuming extension for static libraries: ${STATIC_EXT}") if(BUILD_SHARED_LIBS) set(LIB_EXT ${DYNAMIC_EXT}) - message(STATUS "Build dynamic libraries.") + message(STATUS "Storm - Build dynamic libraries.") else() set(LIB_EXT ${STATIC_EXT}) - message(STATUS "Build static libraries.") + message(STATUS "Storm - Build static libraries.") endif() ############################################################# @@ -443,7 +443,7 @@ if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND") set(STORM_VERSION_SOURCE "VersionSource::Static") set(STORM_VERSION_COMMITS_AHEAD "boost::none") include(version.cmake) - message(WARNING "Storm - git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") + message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.") endif() # check whether there is a label ('alpha', 'pre', etc.) @@ -473,7 +473,7 @@ endif() set(STORM_VERSION "${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_DEV_PATCH}") set(STORM_VERSION_STRING "${STORM_VERSION}${STORM_VERSION_LABEL_STRING}${STORM_VERSION_DEV_STRING}") -message(STATUS "Storm - version is ${STORM_VERSION_STRING} (version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}${STORM_VERSION_LABEL_STRING} + ${STORM_VERSION_COMMITS_AHEAD} commits), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).") +message(STATUS "Storm - Version is ${STORM_VERSION_STRING} (version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}${STORM_VERSION_LABEL_STRING} + ${STORM_VERSION_COMMITS_AHEAD} commits), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).") # Configure a header file to pass some of the CMake settings to the source code diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 5957f3b51..caaa2a0f1 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -239,16 +239,16 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) else() set(STORM_SHIPPED_CARL ON) # The first external project will be built at *configure stage* - message("START CARL CONFIG PROCESS") - file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) + message(STATUS "Carl - Start of config process") + file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) execute_process( COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download OUTPUT_VARIABLE carlconfig_out RESULT_VARIABLE carlconfig_result) - + if(NOT carlconfig_result) - message("${carlconfig_out}") + message(STATUS "${carlconfig_out}") endif() execute_process( COMMAND ${CMAKE_COMMAND} --build . --target carl-config @@ -257,10 +257,10 @@ else() RESULT_VARIABLE carlconfig_result ) if(NOT carlconfig_result) - message("${carlconfig_out}") + message(STATUS "${carlconfig_out}") endif() - message("END CARL CONFIG PROCESS") - + message(STATUS "Carl - End of config process") + message(STATUS "Storm - Using shipped version of carl.") ExternalProject_Add( carl diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt index 4b819682d..3bb50d1b1 100644 --- a/resources/3rdparty/carl/CMakeLists.txt +++ b/resources/3rdparty/carl/CMakeLists.txt @@ -4,7 +4,7 @@ include(ExternalProject) option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir") -message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR}) +message(STATUS "Carl - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}") ExternalProject_Add(carl-config GIT_REPOSITORY https://github.com/smtrat/carl @@ -22,4 +22,4 @@ ExternalProject_Add(carl-config add_custom_target(build-carl) add_dependencies(build-carl carl-config) -message("done") +message(STATUS "Carl - Finished configuration.") From afb0be124565e466ed9f5788e88fa34de82cb410 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 12 Jun 2018 15:08:14 +0200 Subject: [PATCH 18/29] Fixed missing dependencies to storm-parsers --- src/storm-dft/CMakeLists.txt | 2 +- src/storm-parsers/CMakeLists.txt | 2 +- src/storm-pgcl/CMakeLists.txt | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt index f191e537f..48a046238 100644 --- a/src/storm-dft/CMakeLists.txt +++ b/src/storm-dft/CMakeLists.txt @@ -17,7 +17,7 @@ set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-dft) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-dft PUBLIC storm storm-gspn ${STORM_DFT_LINK_LIBRARIES}) +target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-parsers ${STORM_DFT_LINK_LIBRARIES}) # Install storm headers to include directory. foreach(HEADER ${STORM_DFT_HEADERS}) diff --git a/src/storm-parsers/CMakeLists.txt b/src/storm-parsers/CMakeLists.txt index d459345e4..24d9532b5 100644 --- a/src/storm-parsers/CMakeLists.txt +++ b/src/storm-parsers/CMakeLists.txt @@ -10,7 +10,7 @@ file(GLOB_RECURSE STORM_PARSER_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-parsers/* # Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm-parsers/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0) -# Create storm-dft. +# Create storm-parsers. add_library(storm-parsers SHARED ${STORM_PARSER_SOURCES} ${STORM_PARSER_HEADERS}) # Remove define symbol for shared libstorm. diff --git a/src/storm-pgcl/CMakeLists.txt b/src/storm-pgcl/CMakeLists.txt index 059bff395..7b86f73c3 100644 --- a/src/storm-pgcl/CMakeLists.txt +++ b/src/storm-pgcl/CMakeLists.txt @@ -10,7 +10,7 @@ file(GLOB_RECURSE STORM_PGCL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pgcl/*/*.h) # Create storm-pgcl. add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS}) -target_link_libraries(storm-pgcl storm) +target_link_libraries(storm-pgcl storm storm-parsers) # installation install(TARGETS storm-pgcl EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) From a6e6d5993f9b3c80db73a25661f3dfce067d158c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 13 Jun 2018 16:37:45 +0200 Subject: [PATCH 19/29] Travis: set unlimited clone depth to allow versioning with git describe --- .travis.yml | 5 ++++- travis/generate_travis.py | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index 1074ba368..8a5dd952d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -9,6 +9,9 @@ sudo: required dist: trusty language: cpp +git: + depth: false + # Enable caching cache: timeout: 1000 @@ -25,7 +28,7 @@ notifications: on_failure: always on_success: change recipients: - secure: "BoMQTBWnkh4ZLIHEaKu0tAKDohhVmOQ2pz/fjc+ScKG8mtvXqtpx0TiyePOUV1MuYNZiAP7x4mwABcoid55SwZ4+LPjd8uxXNfOji9B9GW5YqbqRvAeh7Es7dx48MyLYPIezjoryHH9R3Q2zZ9gmxgtw5eirjURcLNTXpKAwq/oOsKvh+vhOx4Qierw98wEXjMV7ipBzE4cfkgUbbX7oxGh1nsAsCew+rRmNLijfmE9tctYdH5W0wE+zC9ik+12Xyk3FwsDIABirPHfeCcEl+b9I0h1a2vZSZIA+sCDkIGKTiv9pCnsthn5LJc9pMLX7B/Wf6xLGMzpSiw3P1ZzjXpOE026WuyhTMVXqZYvbl7cJoNZiLCfTYg3MQVq5NHkq0h0jInIH7QlZYd0hZPOGONwdy17O1QmnX2Weq6G+Ps9siLVKFba37+y5PfRYkiUatJvDf2f7Jdxye6TWrUmlxQkAvs65ioyr8doad7IT1/yaGr/rBpXeQqZp6zNoMYr/cCRAYX6nOrnSszgiIWEc8QMMx+G31v77Uvd++9VG4MG9gbdpexpfYRNzKAxDarSaYEOuaWm2Z6R87bpNcjA+tW0hnBHBzRx0NFYYqXyW0tpVO9+035A9CHrLDLz77r4jJttcRvrP2rTbTBiwuhpmiufRyk3BuWlgzU3yaSuQV3M=" + - secure: "VWnsiQkt1xjgRo1hfNiNQqvLSr0fshFmLV7jJlUixhCr094mgD0U2bNKdUfebm28Byg9UyDYPbOFDC0sx7KydKiL1q7FKKXkyZH0k04wUu8XiNw+fYkDpmPnQs7G2n8oJ/GFJnr1Wp/1KI3qX5LX3xot4cJfx1I5iFC2O+p+ng6v/oSX+pewlMv4i7KL16ftHHHMo80N694v3g4B2NByn4GU2/bjVQcqlBp/TiVaUa5Nqu9DxZi/n9CJqGEaRHOblWyMO3EyTZsn45BNSWeQ3DtnMwZ73rlIr9CaEgCeuArc6RGghUAVqRI5ao+N5apekIaILwTgL6AJn+Lw/+NRPa8xclgd0rKqUQJMJCDZKjKz2lmIs3bxfELOizxJ3FJQ5R95FAxeAZ6rb/j40YqVVTw2IMBDnEE0J5ZmpUYNUtPti/Adf6GD9Fb2y8sLo0XDJzkI8OxYhfgjSy5KYmRj8O5MXcP2MAE8LQauNO3MaFnL9VMVOTZePJrPozQUgM021uyahf960+QNI06Uqlmg+PwWkSdllQlxHHplOgW7zClFhtSUpnJxcsUBzgg4kVg80gXUwAQkaDi7A9Wh2bs+TvMlmHzBwg+2SaAfWDgjeJIeOaipDkF1uSGzC+EHAiiKYMLd4Aahoi8SuelJUucoyJyLAq00WdUFQIh/izVhM4Y=" # # Configurations diff --git a/travis/generate_travis.py b/travis/generate_travis.py index ac4e89417..49723a13c 100644 --- a/travis/generate_travis.py +++ b/travis/generate_travis.py @@ -44,6 +44,9 @@ if __name__ == "__main__": s += "dist: trusty\n" s += "language: cpp\n" s += "\n" + s += "git:\n" + s += " depth: false\n" + s += "\n" s += "# Enable caching\n" s += "cache:\n" s += " timeout: 1000\n" @@ -61,7 +64,7 @@ if __name__ == "__main__": s += " on_failure: always\n" s += " on_success: change\n" s += " recipients:\n" - s += ' secure: "BoMQTBWnkh4ZLIHEaKu0tAKDohhVmOQ2pz/fjc+ScKG8mtvXqtpx0TiyePOUV1MuYNZiAP7x4mwABcoid55SwZ4+LPjd8uxXNfOji9B9GW5YqbqRvAeh7Es7dx48MyLYPIezjoryHH9R3Q2zZ9gmxgtw5eirjURcLNTXpKAwq/oOsKvh+vhOx4Qierw98wEXjMV7ipBzE4cfkgUbbX7oxGh1nsAsCew+rRmNLijfmE9tctYdH5W0wE+zC9ik+12Xyk3FwsDIABirPHfeCcEl+b9I0h1a2vZSZIA+sCDkIGKTiv9pCnsthn5LJc9pMLX7B/Wf6xLGMzpSiw3P1ZzjXpOE026WuyhTMVXqZYvbl7cJoNZiLCfTYg3MQVq5NHkq0h0jInIH7QlZYd0hZPOGONwdy17O1QmnX2Weq6G+Ps9siLVKFba37+y5PfRYkiUatJvDf2f7Jdxye6TWrUmlxQkAvs65ioyr8doad7IT1/yaGr/rBpXeQqZp6zNoMYr/cCRAYX6nOrnSszgiIWEc8QMMx+G31v77Uvd++9VG4MG9gbdpexpfYRNzKAxDarSaYEOuaWm2Z6R87bpNcjA+tW0hnBHBzRx0NFYYqXyW0tpVO9+035A9CHrLDLz77r4jJttcRvrP2rTbTBiwuhpmiufRyk3BuWlgzU3yaSuQV3M="\n' + s += ' - secure: "VWnsiQkt1xjgRo1hfNiNQqvLSr0fshFmLV7jJlUixhCr094mgD0U2bNKdUfebm28Byg9UyDYPbOFDC0sx7KydKiL1q7FKKXkyZH0k04wUu8XiNw+fYkDpmPnQs7G2n8oJ/GFJnr1Wp/1KI3qX5LX3xot4cJfx1I5iFC2O+p+ng6v/oSX+pewlMv4i7KL16ftHHHMo80N694v3g4B2NByn4GU2/bjVQcqlBp/TiVaUa5Nqu9DxZi/n9CJqGEaRHOblWyMO3EyTZsn45BNSWeQ3DtnMwZ73rlIr9CaEgCeuArc6RGghUAVqRI5ao+N5apekIaILwTgL6AJn+Lw/+NRPa8xclgd0rKqUQJMJCDZKjKz2lmIs3bxfELOizxJ3FJQ5R95FAxeAZ6rb/j40YqVVTw2IMBDnEE0J5ZmpUYNUtPti/Adf6GD9Fb2y8sLo0XDJzkI8OxYhfgjSy5KYmRj8O5MXcP2MAE8LQauNO3MaFnL9VMVOTZePJrPozQUgM021uyahf960+QNI06Uqlmg+PwWkSdllQlxHHplOgW7zClFhtSUpnJxcsUBzgg4kVg80gXUwAQkaDi7A9Wh2bs+TvMlmHzBwg+2SaAfWDgjeJIeOaipDkF1uSGzC+EHAiiKYMLd4Aahoi8SuelJUucoyJyLAq00WdUFQIh/izVhM4Y="\n' s += "\n" s += "#\n" s += "# Configurations\n" From cdfa32846463872bfa51a87c86c09bd14e297879 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Jun 2018 10:57:52 +0200 Subject: [PATCH 20/29] first attempt at adapting to Z3 interface change --- resources/3rdparty/CMakeLists.txt | 9 +++++++++ src/storm/adapters/Z3ExpressionAdapter.cpp | 19 ++++++++++++++----- .../DynamicStatePriorityQueue.h | 2 +- .../MaximalEndComponentDecompositionTest.cpp | 4 ++-- src/test/storm/utility/KSPTest.cpp | 4 ++-- storm-config.h.in | 7 +++++++ 6 files changed, 35 insertions(+), 10 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index caaa2a0f1..18a68a23f 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -168,6 +168,15 @@ else() message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.") endif(Z3_FOUND) +# split Z3 version into its components +string(REPLACE "." ";" Z3_VERSION_LIST ${Z3_VERSION}) +list(GET Z3_VERSION_LIST 0 STORM_Z3_VERSION_MAJOR) +list(GET Z3_VERSION_LIST 1 STORM_Z3_VERSION_MINOR) +list(GET Z3_VERSION_LIST 2 STORM_Z3_VERSION_PATCH) +if (NOT "${Z3_VERSION}" VERSION_LESS "4.7.1") + set(STORM_Z3_API_USES_STANDARD_INTEGERS ON) +endif() + ############################################################# ## ## glpk diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index c7e27756d..fec9068b0 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -12,6 +12,15 @@ namespace storm { namespace adapters { #ifdef STORM_HAVE_Z3 + +#ifdef STORM_Z3_API_USES_STANDARD_INTEGERS + typedef int64_t Z3_SIGNED_INTEGER; + typedef int64_t Z3_UNSIGNED_INTEGER; +#else + typedef long long Z3_SIGNED_INTEGER; + typedef unsigned long long Z3_UNSIGNED_INTEGER; +#endif + Z3ExpressionAdapter::Z3ExpressionAdapter(storm::expressions::ExpressionManager& manager, z3::context& context) : manager(manager), context(context), additionalAssertions(), variableToExpressionMapping() { // Intentionally left empty. } @@ -133,17 +142,17 @@ namespace storm { case Z3_OP_ANUM: // Arithmetic numeral. if (expr.is_int() && expr.is_const()) { - long long value; + Z3_SIGNED_INTEGER value; if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) { return manager.integer(value); } else { STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer."); } } else if (expr.is_real() && expr.is_const()) { - long long num; - long long den; + Z3_SIGNED_INTEGER num; + Z3_SIGNED_INTEGER den; if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) { - return manager.rational(storm::utility::convertNumber((int_fast64_t) num) / storm::utility::convertNumber((int_fast64_t) den)); + return manager.rational(storm::utility::convertNumber(static_cast(num)) / storm::utility::convertNumber(static_cast(den))); } else { return manager.rational(storm::utility::convertNumber(std::string(Z3_get_numeral_string(expr.ctx(), expr)))); } @@ -304,7 +313,7 @@ namespace storm { return cacheIt->second; } - z3::expr result = context.int_val(static_cast(expression.getValue())); + z3::expr result = context.int_val(static_cast(expression.getValue())); expressionCache.emplace(&expression, result); return result; diff --git a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h index 0ac38769d..4065ee265 100644 --- a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h +++ b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.h @@ -17,7 +17,7 @@ namespace storm { namespace stateelimination { struct PriorityComparator { - bool operator()(std::pair const& first, std::pair const& second) { + bool operator()(std::pair const& first, std::pair const& second) const { return (first.second < second.second) || (first.second == second.second && first.first < second.first) ; } }; diff --git a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp index b30b5259b..ced1cd6b0 100644 --- a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp +++ b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp @@ -148,7 +148,7 @@ TEST(MaximalEndComponentDecomposition, Example1) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); - EXPECT_EQ(mecDecomposition.size(), 2); + EXPECT_EQ(2ull, mecDecomposition.size()); ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{3}); @@ -167,7 +167,7 @@ TEST(MaximalEndComponentDecomposition, Example2) { storm::storage::MaximalEndComponentDecomposition mecDecomposition(*mdp); - EXPECT_EQ(mecDecomposition.size(), 2); + EXPECT_EQ(2ull, mecDecomposition.size()); ASSERT_TRUE(mecDecomposition[0].getStateSet() == storm::storage::MaximalEndComponent::set_type{2}); EXPECT_TRUE(mecDecomposition[0].getChoicesForState(2) == storm::storage::MaximalEndComponent::set_type{4}); diff --git a/src/test/storm/utility/KSPTest.cpp b/src/test/storm/utility/KSPTest.cpp index dfe14e817..d584a7660 100644 --- a/src/test/storm/utility/KSPTest.cpp +++ b/src/test/storm/utility/KSPTest.cpp @@ -81,7 +81,7 @@ TEST(KSPTest, kspStateSet) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); auto bv = spg.getStates(7); - EXPECT_EQ(50, bv.getNumberOfSetBits()); + EXPECT_EQ(50ull, bv.getNumberOfSetBits()); // The result may sadly depend on the compiler/system, so checking a particular outcome is not feasible. // storm::storage::BitVector referenceBV(model->getNumberOfStates(), false); @@ -97,7 +97,7 @@ TEST(KSPTest, kspPathAsList) { storm::utility::ksp::ShortestPathsGenerator spg(*model, testState); auto list = spg.getPathAsList(7); - EXPECT_EQ(50, list.size()); + EXPECT_EQ(50ull, list.size()); // TODO: use path that actually has a loop or something to make this more interesting // auto reference = storm::utility::ksp::OrderedStateList{296, 288, 281, 272, 266, 260, 253, 245, 238, 230, 224, 218, 211, 203, 196, 188, 182, 176, 169, 161, 154, 146, 140, 134, 127, 119, 112, 104, 98, 92, 85, 77, 70, 81, 74, 65, 58, 52, 45, 37, 30, 22, 17, 12, 9, 6, 4, 2, 1, 0}; diff --git a/storm-config.h.in b/storm-config.h.in index b0290b751..55d2247d3 100644 --- a/storm-config.h.in +++ b/storm-config.h.in @@ -41,6 +41,13 @@ // Whether the optimization feature of Z3 is available and to be used (define/undef) #cmakedefine STORM_HAVE_Z3_OPTIMIZE +// Version of Z3 used by Storm. +#define STORM_Z3_VERSION_MAJOR @STORM_Z3_VERSION_MAJOR@ +#define STORM_Z3_VERSION_MINOR @STORM_Z3_VERSION_MINOR@ +#define STORM_Z3_VERSION_PATCH @STORM_Z3_VERSION_PATCH@ +#define STORM_Z3_VERSION @Z3_VERSION@ +#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS + // Whether MathSAT is available and to be used (define/undef) #cmakedefine STORM_HAVE_MSAT From dfc0141894c34a1b8c4014adee82677f0595bad5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 22 Jun 2018 13:25:21 +0200 Subject: [PATCH 21/29] minor fix to Z3 API modification --- src/storm/adapters/Z3ExpressionAdapter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index fec9068b0..8a7f55bf5 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -1,5 +1,7 @@ #include "storm/adapters/Z3ExpressionAdapter.h" +#include + #include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/macros.h" @@ -15,7 +17,7 @@ namespace storm { #ifdef STORM_Z3_API_USES_STANDARD_INTEGERS typedef int64_t Z3_SIGNED_INTEGER; - typedef int64_t Z3_UNSIGNED_INTEGER; + typedef uint64_t Z3_UNSIGNED_INTEGER; #else typedef long long Z3_SIGNED_INTEGER; typedef unsigned long long Z3_UNSIGNED_INTEGER; From 87e34d7b324686ae80143a4915aa128c327aec8d Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 22 Jun 2018 15:05:36 +0200 Subject: [PATCH 22/29] Added Support for Total Reward Formulas for DTMCs in the Sparse Engine --- src/storm/logic/FragmentSpecification.cpp | 2 ++ src/storm/modelchecker/AbstractModelChecker.cpp | 7 +++++++ src/storm/modelchecker/AbstractModelChecker.h | 1 + .../modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp | 6 ++++++ .../modelchecker/prctl/SparseDtmcPrctlModelChecker.h | 1 + .../prctl/helper/SparseDtmcPrctlHelper.cpp | 10 ++++++++++ .../modelchecker/prctl/helper/SparseDtmcPrctlHelper.h | 2 ++ src/storm/models/sparse/NondeterministicModel.cpp | 2 +- src/storm/models/sparse/NondeterministicModel.h | 2 +- 9 files changed, 31 insertions(+), 2 deletions(-) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index cdcfc6ecd..ad7678d79 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -59,6 +59,7 @@ namespace storm { prctl.setCumulativeRewardFormulasAllowed(true); prctl.setInstantaneousFormulasAllowed(true); prctl.setReachabilityRewardFormulasAllowed(true); + prctl.setTotalRewardFormulasAllowed(true); prctl.setLongRunAverageOperatorsAllowed(true); prctl.setStepBoundedCumulativeRewardFormulasAllowed(true); prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true); @@ -81,6 +82,7 @@ namespace storm { csrl.setCumulativeRewardFormulasAllowed(true); csrl.setInstantaneousFormulasAllowed(true); csrl.setReachabilityRewardFormulasAllowed(true); + csrl.setTotalRewardFormulasAllowed(true); csrl.setLongRunAverageOperatorsAllowed(true); csrl.setTimeBoundedCumulativeRewardFormulasAllowed(true); diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 2712b6d4a..e6c4f282f 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -105,6 +105,8 @@ namespace storm { return this->computeInstantaneousRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asInstantaneousRewardFormula())); } else if (rewardFormula.isReachabilityRewardFormula()) { return this->computeReachabilityRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asReachabilityRewardFormula())); + } else if (rewardFormula.isTotalRewardFormula()) { + return this->computeTotalRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asTotalRewardFormula())); } else if (rewardFormula.isLongRunAverageRewardFormula()) { return this->computeLongRunAverageRewards(env, rewardMeasureType, checkTask.substituteFormula(rewardFormula.asLongRunAverageRewardFormula())); } else if (rewardFormula.isConditionalRewardFormula()) { @@ -132,6 +134,11 @@ namespace storm { std::unique_ptr AbstractModelChecker::computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); } + + template + std::unique_ptr AbstractModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << checkTask.getFormula() << "."); + } template std::unique_ptr AbstractModelChecker::computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/AbstractModelChecker.h b/src/storm/modelchecker/AbstractModelChecker.h index 0d391f1d9..3251ea1fa 100644 --- a/src/storm/modelchecker/AbstractModelChecker.h +++ b/src/storm/modelchecker/AbstractModelChecker.h @@ -63,6 +63,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); + virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask); // The methods to compute the long-run average probabilities and timing measures. diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 4a746bf07..240657e81 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -123,6 +123,12 @@ namespace storm { std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), checkTask.isQualitativeSet(), checkTask.getHint()); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + + template + std::unique_ptr SparseDtmcPrctlModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + std::vector numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet(), checkTask.getHint()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } template std::unique_ptr SparseDtmcPrctlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h index ebc7d39a3..6500da487 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h @@ -30,6 +30,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeConditionalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp index 03d3fb1a0..2745569ad 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp @@ -383,6 +383,16 @@ namespace storm { return result; } + template + std::vector SparseDtmcPrctlHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, ModelCheckerHint const& hint) { + // Identify the states from which only states with zero reward are reachable. + // We can then compute reachability rewards assuming these states as target set. + storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(transitionMatrix); + storm::storage::BitVector rew0States = storm::utility::graph::performProbGreater0(backwardTransitions, statesWithoutReward, ~statesWithoutReward); + rew0States.complement(); + return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0States, qualitative, hint); + } + template std::vector SparseDtmcPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint) { diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h index a4e2882bc..49fe21deb 100644 --- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h @@ -42,6 +42,8 @@ namespace storm { static std::vector computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepCount); + static std::vector computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); + static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& totalStateRewardVector, storm::storage::BitVector const& targetStates, bool qualitative, ModelCheckerHint const& hint = ModelCheckerHint()); diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 263f67c16..08331c6f5 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -45,7 +45,7 @@ namespace storm { } template - std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { + std::shared_ptr> NondeterministicModel::applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) const { storm::storage::SparseModelMemoryProduct memoryProduct(*this, scheduler); if (!dropUnreachableStates) { memoryProduct.setBuildFullProduct(); diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index ac8603e7f..5280ba962 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -57,7 +57,7 @@ namespace storm { * @param scheduler the considered scheduler. * @param dropUnreachableStates if set, the resulting model only considers the states that are reachable from an initial state */ - std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates = true); + std::shared_ptr> applyScheduler(storm::storage::Scheduler const& scheduler, bool dropUnreachableStates = true) const; virtual void printModelInformationToStream(std::ostream& out) const override; From c2dd57cda57319a548c2ee1de3f50cc718a205fc Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 22 Jun 2018 17:28:01 +0200 Subject: [PATCH 23/29] total rewards for mdps --- .../prctl/helper/SparseMdpPrctlHelper.cpp | 75 +++++++++++++++++++ .../prctl/helper/SparseMdpPrctlHelper.h | 3 + .../transformer/EndComponentEliminator.h | 34 +++++---- 3 files changed, 98 insertions(+), 14 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 8c13c73c4..e2ce02120 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -35,6 +35,8 @@ #include "storm/utility/ProgressMeasurement.h" #include "storm/utility/export.h" +#include "storm/transformer/EndComponentEliminator.h" + #include "storm/environment/solver/MinMaxSolverEnvironment.h" #include "storm/exceptions/InvalidStateException.h" @@ -839,6 +841,79 @@ namespace storm { return result; } + template + template + MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) { + + // Reduce to reachability rewards + if (goal.minimize) { + STORM_LOG_ERROR_COND(!produceScheduler, "Can not produce scheduler for this property (functionality not implemented"); + // Identify the states from which no reward can be collected under some scheduler + storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix); + storm::storage::BitVector statesWithZeroRewardChoice(transitionMatrix.getRowGroupCount(), false); + for (uint64_t state = 0; state < transitionMatrix.getRowGroupCount(); ++state) { + if (choicesWithoutReward.getNextSetIndex(transitionMatrix.getRowGroupIndices()[state])< transitionMatrix.getRowGroupIndices()[state + 1]) { + statesWithZeroRewardChoice.set(state); + } + } + storm::storage::BitVector rew0EStates = storm::utility::graph::performProbGreater0A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, statesWithZeroRewardChoice, ~statesWithZeroRewardChoice, false, 0, choicesWithoutReward); + rew0EStates.complement(); + return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0EStates, qualitative, false, hint); + } else { + // Identify the states from which only states with zero reward are reachable. + storm::storage::BitVector statesWithoutReward = rewardModel.getStatesWithZeroReward(transitionMatrix); + storm::storage::BitVector rew0AStates = storm::utility::graph::performProbGreater0E(backwardTransitions, statesWithoutReward, ~statesWithoutReward); + rew0AStates.complement(); + + // There might be end components that consists only of states/choices with zero rewards. The reachability reward semantics would assign such + // end components reward infinity. To avoid this, we potentially need to eliminate such end components + storm::storage::BitVector trueStates(transitionMatrix.getRowGroupCount(), true); + if (storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, trueStates, rew0AStates).full()) { + return computeReachabilityRewards(env, std::move(goal), transitionMatrix, backwardTransitions, rewardModel, rew0AStates, qualitative, produceScheduler, hint); + } else { + // The transformation of schedulers for the ec-eliminated system back to the original one is not implemented. + STORM_LOG_ERROR_COND(!produceScheduler, "Can not produce scheduler for this property (functionality not implemented"); + storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix); + auto ecElimResult = storm::transformer::EndComponentEliminator::transform(transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), choicesWithoutReward, rew0AStates, true); + storm::storage::BitVector newRew0AStates(ecElimResult.matrix.getRowGroupCount(), false); + for (auto const& oldRew0AState : rew0AStates) { + newRew0AStates.set(ecElimResult.oldToNewStateMapping[oldRew0AState]); + } + + return computeReachabilityRewardsHelper(env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(true), + [&] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { + std::vector result; + std::vector oldChoiceRewards = rewardModel.getTotalRewardVector(rowCount, transitionMatrix); + result.reserve(rowCount); + for (uint64_t newState : maybeStates) { + for (uint64_t newChoice = transitionMatrix.getRowGroupIndices()[newState]; newChoice < transitionMatrix.getRowGroupIndices()[newState + 1]; ++newChoice) { + uint64_t oldChoice = ecElimResult.newToOldRowMapping[newChoice]; + result.push_back(oldChoiceRewards[oldChoice]); + } + } + STORM_LOG_ASSERT(result.size() == rowCount, "Unexpected size of reward vector."); + return result; + }, newRew0AStates, qualitative, false, + [&] () { + storm::storage::BitVector newStatesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false); + for (auto const& oldStateWithoutRew : statesWithoutReward) { + newStatesWithoutReward.set(ecElimResult.oldToNewStateMapping[oldStateWithoutRew]); + } + return newStatesWithoutReward; + }, + [&] () { + storm::storage::BitVector newChoicesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false); + for (uint64_t newChoice = 0; newChoice < ecElimResult.matrix.getRowCount(); ++newChoice) { + if (choicesWithoutReward.get(ecElimResult.newToOldChoiceMapping[newChoice])) { + newChoicesWithoutReward.set(newChoice); + } + } + return newChoicesWithoutReward; + }); + } + } + } + template template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 920bb4d47..b1de7a442 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -55,6 +55,9 @@ namespace storm { template static std::vector computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound); + template + static MDPSparseModelCheckingHelperReturnType computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); + template static MDPSparseModelCheckingHelperReturnType computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint = ModelCheckerHint()); diff --git a/src/storm/transformer/EndComponentEliminator.h b/src/storm/transformer/EndComponentEliminator.h index 635cba7b6..378edc86a 100644 --- a/src/storm/transformer/EndComponentEliminator.h +++ b/src/storm/transformer/EndComponentEliminator.h @@ -18,7 +18,7 @@ namespace storm { // The resulting matrix storm::storage::SparseMatrix matrix; // Index mapping that gives for each row of the resulting matrix the corresponding row in the original matrix. - // For the empty rows added to EC states, an arbitrary row of the original matrix that stays inside the EC is given. + // For the sink rows added to EC states, an arbitrary row of the original matrix that stays inside the EC is given. std::vector newToOldRowMapping; // Gives for each state (=rowGroup) of the original matrix the corresponding state in the resulting matrix. // States of a removed ECs are mapped to the state that substitutes the EC. @@ -38,9 +38,10 @@ namespace storm { * * For each such EC (that is not contained in another EC), we add a new state and redirect all incoming and outgoing * transitions of the EC to (and from) this state. - * If addEmptyRowStates is true for at least one state of an eliminated EC, an empty row is added to the new state (representing the choice to stay at the EC forever). + * If addSinkRowStates is true for at least one state of an eliminated EC, a row is added to the new state (representing the choice to stay at the EC forever). + * If addSelfLoopAtSinkStates is true, such rows get a selfloop (with value 1). Otherwise, the row remains empty. */ - static EndComponentEliminatorReturnType transform(storm::storage::SparseMatrix const& originalMatrix, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& possibleECRows, storm::storage::BitVector const& addEmptyRowStates) { + static EndComponentEliminatorReturnType transform(storm::storage::SparseMatrix const& originalMatrix, storm::storage::BitVector const& subsystemStates, storm::storage::BitVector const& possibleECRows, storm::storage::BitVector const& addSinkRowStates, bool addSelfLoopAtSinkStates = false) { STORM_LOG_DEBUG("Invoked EndComponentEliminator on matrix with " << originalMatrix.getRowGroupCount() << " row groups."); storm::storage::MaximalEndComponentDecomposition ecs = computeECs(originalMatrix, possibleECRows, subsystemStates); @@ -57,7 +58,7 @@ namespace storm { EndComponentEliminatorReturnType result; std::vector newRowGroupIndices; result.oldToNewStateMapping = std::vector(originalMatrix.getRowGroupCount(), std::numeric_limits::max()); - storm::storage::BitVector emptyRows(originalMatrix.getRowCount(), false); // will be resized as soon as the rowCount of the resulting matrix is known + storm::storage::BitVector sinkRows(originalMatrix.getRowCount(), false); // will be resized as soon as the rowCount of the resulting matrix is known for(auto keptState : keptStates) { result.oldToNewStateMapping[keptState] = newRowGroupIndices.size(); // i.e., the current number of processed states @@ -68,7 +69,7 @@ namespace storm { } for (auto const& ec : ecs) { newRowGroupIndices.push_back(result.newToOldRowMapping.size()); - bool ecGetsEmptyRow = false; + bool ecGetsSinkRow = false; for (auto const& stateActionsPair : ec) { result.oldToNewStateMapping[stateActionsPair.first] = newRowGroupIndices.size()-1; for(uint_fast64_t row = originalMatrix.getRowGroupIndices()[stateActionsPair.first]; row < originalMatrix.getRowGroupIndices()[stateActionsPair.first +1]; ++row) { @@ -76,18 +77,18 @@ namespace storm { result.newToOldRowMapping.push_back(row); } } - ecGetsEmptyRow |= addEmptyRowStates.get(stateActionsPair.first); + ecGetsSinkRow |= addSinkRowStates.get(stateActionsPair.first); } - if(ecGetsEmptyRow) { + if(ecGetsSinkRow) { STORM_LOG_ASSERT(result.newToOldRowMapping.size() < originalMatrix.getRowCount(), "Didn't expect to see more rows in the reduced matrix than in the original one."); - emptyRows.set(result.newToOldRowMapping.size(), true); + sinkRows.set(result.newToOldRowMapping.size(), true); result.newToOldRowMapping.push_back(*ec.begin()->second.begin()); } } newRowGroupIndices.push_back(result.newToOldRowMapping.size()); - emptyRows.resize(result.newToOldRowMapping.size()); + sinkRows.resize(result.newToOldRowMapping.size()); - result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, emptyRows); + result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, sinkRows, addSelfLoopAtSinkStates); STORM_LOG_DEBUG("EndComponentEliminator is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups."); return result; } @@ -136,15 +137,20 @@ namespace storm { std::vector const& newRowGroupIndices, std::vector const& newToOldRowMapping, std::vector const& oldToNewStateMapping, - storm::storage::BitVector const& emptyRows) { + storm::storage::BitVector const& sinkRows, + bool addSelfLoopAtSinkStates) { uint_fast64_t numRowGroups = newRowGroupIndices.size()-1; uint_fast64_t newRow = 0; storm::storage::SparseMatrixBuilder builder(newToOldRowMapping.size(), numRowGroups, originalMatrix.getEntryCount(), false, true, numRowGroups); - for(uint_fast64_t newRowGroup = 0; newRowGroup < numRowGroups; ++newRowGroup) { + for (uint_fast64_t newRowGroup = 0; newRowGroup < numRowGroups; ++newRowGroup) { builder.newRowGroup(newRow); - for(; newRow < newRowGroupIndices[newRowGroup+1]; ++newRow) { - if(!emptyRows.get(newRow)) { + for (; newRow < newRowGroupIndices[newRowGroup + 1]; ++newRow) { + if (sinkRows.get(newRow)) { + if (addSelfLoopAtSinkStates) { + builder.addNextValue(newRow, newRowGroup, storm::utility::one()); + } + } else { // Make sure that the entries for this row are inserted in the right order. // Also, transitions to the same EC need to be merged and transitions to states that are erased need to be ignored std::map sortedEntries; From b3edae870762db1a0747cdc7a229e94c77a442b3 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 25 Jun 2018 11:21:31 +0200 Subject: [PATCH 24/29] fixed fragment specification: total reward formulas should not be supported for hybrid/dd right now --- src/storm/logic/FragmentSpecification.cpp | 2 -- .../prctl/SparseDtmcPrctlModelChecker.cpp | 2 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 13 ++++++++++++- 3 files changed, 13 insertions(+), 4 deletions(-) diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index ad7678d79..cdcfc6ecd 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -59,7 +59,6 @@ namespace storm { prctl.setCumulativeRewardFormulasAllowed(true); prctl.setInstantaneousFormulasAllowed(true); prctl.setReachabilityRewardFormulasAllowed(true); - prctl.setTotalRewardFormulasAllowed(true); prctl.setLongRunAverageOperatorsAllowed(true); prctl.setStepBoundedCumulativeRewardFormulasAllowed(true); prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true); @@ -82,7 +81,6 @@ namespace storm { csrl.setCumulativeRewardFormulasAllowed(true); csrl.setInstantaneousFormulasAllowed(true); csrl.setReachabilityRewardFormulasAllowed(true); - csrl.setTotalRewardFormulasAllowed(true); csrl.setLongRunAverageOperatorsAllowed(true); csrl.setTimeBoundedCumulativeRewardFormulasAllowed(true); diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 240657e81..082ddd813 100644 --- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -31,7 +31,7 @@ namespace storm { template bool SparseDtmcPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setConditionalRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true)); } template diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 074a679b6..ba5aac431 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -38,7 +38,7 @@ namespace storm { template bool SparseMdpPrctlModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) { + if (formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula @@ -172,6 +172,17 @@ namespace storm { } return result; } + + template + std::unique_ptr SparseMdpPrctlModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + auto ret = storm::modelchecker::helper::SparseMdpPrctlHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet(), checkTask.isProduceSchedulersSet(), checkTask.getHint()); + std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); + if (checkTask.isProduceSchedulersSet() && ret.scheduler) { + result->asExplicitQuantitativeCheckResult().setScheduler(std::move(ret.scheduler)); + } + return result; + } template std::unique_ptr SparseMdpPrctlModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { From b5566fa861d8b57342101f03403135f68c942880 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 25 Jun 2018 11:22:02 +0200 Subject: [PATCH 25/29] more on total reward formulas for mdps --- src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h | 1 + .../modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp | 8 +++++--- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h index 5ea9a010a..5667549e3 100644 --- a/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h +++ b/src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h @@ -27,6 +27,7 @@ namespace storm { virtual std::unique_ptr computeConditionalProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index e2ce02120..4b29d2324 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -846,7 +846,7 @@ namespace storm { MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, RewardModelType const& rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint) { // Reduce to reachability rewards - if (goal.minimize) { + if (goal.minimize()) { STORM_LOG_ERROR_COND(!produceScheduler, "Can not produce scheduler for this property (functionality not implemented"); // Identify the states from which no reward can be collected under some scheduler storm::storage::BitVector choicesWithoutReward = rewardModel.getChoicesWithZeroReward(transitionMatrix); @@ -883,7 +883,7 @@ namespace storm { return computeReachabilityRewardsHelper(env, std::move(goal), ecElimResult.matrix, ecElimResult.matrix.transpose(true), [&] (uint_fast64_t rowCount, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates) { std::vector result; - std::vector oldChoiceRewards = rewardModel.getTotalRewardVector(rowCount, transitionMatrix); + std::vector oldChoiceRewards = rewardModel.getTotalRewardVector(transitionMatrix); result.reserve(rowCount); for (uint64_t newState : maybeStates) { for (uint64_t newChoice = transitionMatrix.getRowGroupIndices()[newState]; newChoice < transitionMatrix.getRowGroupIndices()[newState + 1]; ++newChoice) { @@ -904,7 +904,7 @@ namespace storm { [&] () { storm::storage::BitVector newChoicesWithoutReward(ecElimResult.matrix.getRowGroupCount(), false); for (uint64_t newChoice = 0; newChoice < ecElimResult.matrix.getRowCount(); ++newChoice) { - if (choicesWithoutReward.get(ecElimResult.newToOldChoiceMapping[newChoice])) { + if (choicesWithoutReward.get(ecElimResult.newToOldRowMapping[newChoice])) { newChoicesWithoutReward.set(newChoice); } } @@ -1761,6 +1761,7 @@ namespace storm { template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound); template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint); + template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint); template std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel); template double SparseMdpPrctlHelper::computeLraForMaximalEndComponent(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); template double SparseMdpPrctlHelper::computeLraForMaximalEndComponentVI(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); @@ -1771,6 +1772,7 @@ namespace storm { template std::vector SparseMdpPrctlHelper::computeInstantaneousRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepCount); template std::vector SparseMdpPrctlHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, uint_fast64_t stepBound); template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint); + template MDPSparseModelCheckingHelperReturnType SparseMdpPrctlHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative, bool produceScheduler, ModelCheckerHint const& hint); template std::vector SparseMdpPrctlHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::models::sparse::StandardRewardModel const& rewardModel); template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponent(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); template storm::RationalNumber SparseMdpPrctlHelper::computeLraForMaximalEndComponentVI(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::MaximalEndComponent const& mec); From 8df9b461cb8319ceccaf2ce6cc47fcda41f5f993 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 25 Jun 2018 11:22:31 +0200 Subject: [PATCH 26/29] total reward formulas for ctmcs and markov automata --- .../csl/SparseCtmcCslModelChecker.cpp | 10 ++++- .../csl/SparseCtmcCslModelChecker.h | 1 + .../SparseMarkovAutomatonCslModelChecker.cpp | 11 +++++- .../SparseMarkovAutomatonCslModelChecker.h | 1 + .../csl/helper/SparseCtmcCslHelper.cpp | 37 +++++++++++++++++++ .../csl/helper/SparseCtmcCslHelper.h | 3 ++ .../helper/SparseMarkovAutomatonCslHelper.cpp | 18 +++++++++ .../helper/SparseMarkovAutomatonCslHelper.h | 3 ++ 8 files changed, 81 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 52d49815e..3cedc1fab 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -37,14 +37,14 @@ namespace storm { template::SupportsExponential, int>::type> bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); + return formula.isInFragment(storm::logic::csrl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true)); } template template::SupportsExponential, int>::type> bool SparseCtmcCslModelChecker::canHandleImplementation(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true)); + return formula.isInFragment(storm::logic::prctl().setGloballyFormulasAllowed(false).setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setTimeAllowed(true).setTotalRewardFormulasAllowed(true)); } template @@ -117,6 +117,12 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); } + template + std::unique_ptr SparseCtmcCslModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + std::vector numericResult = storm::modelchecker::helper::SparseCtmcCslHelper::computeTotalRewards(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRateVector(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), checkTask.isQualitativeSet()); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(numericResult))); + } + template std::unique_ptr SparseCtmcCslModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h index 9bf94fe93..5bf4735d0 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -33,6 +33,7 @@ namespace storm { virtual std::unique_ptr computeCumulativeRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeInstantaneousRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; private: template::SupportsExponential, int>::type = 0> diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 74c976fd6..d72503cae 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -89,7 +89,16 @@ namespace storm { return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } - + + template + std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType, CheckTask const& checkTask) { + STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(this->getModel().isClosed(), storm::exceptions::InvalidPropertyException, "Unable to compute reachability rewards in non-closed Markov automaton."); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTotalRewards(env, checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel("")); + + return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); + } + template std::unique_ptr SparseMarkovAutomatonCslModelChecker::computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::StateFormula const& stateFormula = checkTask.getFormula(); diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 60cf49d37..3bd557dd4 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -24,6 +24,7 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeUntilProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; + virtual std::unique_ptr computeTotalRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageProbabilities(Environment const& env, CheckTask const& checkTask) override; virtual std::unique_ptr computeLongRunAverageRewards(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; virtual std::unique_ptr computeReachabilityTimes(Environment const& env, storm::logic::RewardMeasureType rewardMeasureType, CheckTask const& checkTask) override; diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 99bad8ce1..f888ed1b6 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -329,6 +329,38 @@ namespace storm { return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(env, std::move(goal), probabilityMatrix, backwardTransitions, totalRewardVector, targetStates, qualitative); } + template + std::vector SparseCtmcCslHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, bool qualitative) { + STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); + + storm::storage::SparseMatrix probabilityMatrix = computeProbabilityMatrix(rateMatrix, exitRateVector); + + std::vector totalRewardVector; + if (rewardModel.hasStateRewards()) { + totalRewardVector = rewardModel.getStateRewardVector(); + typename std::vector::const_iterator it2 = exitRateVector.begin(); + for (typename std::vector::iterator it1 = totalRewardVector.begin(), ite1 = totalRewardVector.end(); it1 != ite1; ++it1, ++it2) { + *it1 /= *it2; + } + if (rewardModel.hasStateActionRewards()) { + storm::utility::vector::addVectors(totalRewardVector, rewardModel.getStateActionRewardVector(), totalRewardVector); + } + if (rewardModel.hasTransitionRewards()) { + storm::utility::vector::addVectors(totalRewardVector, probabilityMatrix.getPointwiseProductRowSumVector(rewardModel.getTransitionRewardMatrix()), totalRewardVector); + } + } else if (rewardModel.hasTransitionRewards()) { + totalRewardVector = probabilityMatrix.getPointwiseProductRowSumVector(rewardModel.getTransitionRewardMatrix()); + if (rewardModel.hasStateActionRewards()) { + storm::utility::vector::addVectors(totalRewardVector, rewardModel.getStateActionRewardVector(), totalRewardVector); + } + } else { + totalRewardVector = rewardModel.getStateActionRewardVector(); + } + + RewardModelType dtmcRewardModel(std::move(totalRewardVector)); + return storm::modelchecker::helper::SparseDtmcPrctlHelper::computeTotalRewards(env, std::move(goal), probabilityMatrix, backwardTransitions, dtmcRewardModel, qualitative); + } + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector) { @@ -743,6 +775,8 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StandardRewardModel const& rewardModel, std::vector const* exitRateVector); template std::vector SparseCtmcCslHelper::computeLongRunAverageRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, std::vector const& stateRewardVector, std::vector const* exitRateVector); @@ -772,6 +806,9 @@ namespace storm { template std::vector SparseCtmcCslHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative); template std::vector SparseCtmcCslHelper::computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative); + template std::vector SparseCtmcCslHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative); + template std::vector SparseCtmcCslHelper::computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::models::sparse::StandardRewardModel const& rewardModel, bool qualitative); + template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); template std::vector SparseCtmcCslHelper::computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h index 28125c7c9..b6e7b508c 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.h @@ -44,6 +44,9 @@ namespace storm { template static std::vector computeReachabilityRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative); + + template + static std::vector computeTotalRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, RewardModelType const& rewardModel, bool qualitative); template static std::vector computeLongRunAverageProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector const* exitRateVector); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 8eb688d55..6e6a39acf 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -583,6 +583,20 @@ namespace storm { return std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(env, dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, false).values); } + template + std::vector SparseMarkovAutomatonCslHelper::computeTotalRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel) { + + // Get a reward model where the state rewards are scaled accordingly + std::vector stateRewardWeights(transitionMatrix.getRowGroupCount(), storm::utility::zero()); + for (auto const markovianState : markovianStates) { + stateRewardWeights[markovianState] = storm::utility::one() / exitRateVector[markovianState]; + } + std::vector totalRewardVector = rewardModel.getTotalActionRewardVector(transitionMatrix, stateRewardWeights); + RewardModelType scaledRewardModel(boost::none, std::move(totalRewardVector)); + + return SparseMdpPrctlHelper::computeTotalRewards(env, dir, transitionMatrix, backwardTransitions, scaledRewardModel, false, false).values; + } + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates) { @@ -1020,6 +1034,8 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates); + template std::vector SparseMarkovAutomatonCslHelper::computeTotalRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates); template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel); @@ -1038,6 +1054,8 @@ namespace storm { template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates); + template std::vector SparseMarkovAutomatonCslHelper::computeTotalRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel); + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates); template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index fbfeaa7dd..6b6a94a50 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -26,6 +26,9 @@ namespace storm { template static std::vector computeUntilProbabilities(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative); + template + static std::vector computeTotalRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel); + template static std::vector computeReachabilityRewards(Environment const& env, OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates); From 1f4c0325be6b9d9103cd98a87e68c2fa161bf34b Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 25 Jun 2018 11:22:52 +0200 Subject: [PATCH 27/29] test cases for ctmcs and markov automata --- resources/examples/testfiles/ctmc/simple2.sm | 28 ++ resources/examples/testfiles/ma/simple2.ma | 40 +++ .../modelchecker/CtmcCslModelCheckerTest.cpp | 23 ++ .../MarkovAutomatonCslModelCheckerTest.cpp | 264 ++++++++++++++++++ 4 files changed, 355 insertions(+) create mode 100644 resources/examples/testfiles/ctmc/simple2.sm create mode 100644 resources/examples/testfiles/ma/simple2.ma create mode 100644 src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp diff --git a/resources/examples/testfiles/ctmc/simple2.sm b/resources/examples/testfiles/ctmc/simple2.sm new file mode 100644 index 000000000..5fcc0dcab --- /dev/null +++ b/resources/examples/testfiles/ctmc/simple2.sm @@ -0,0 +1,28 @@ + +ctmc + + +module main + + s : [0..4]; // current state: + + + <> s=0 -> 4 : (s'=1) + 4 : (s'=2); + <> s=1 -> 0.3 : (s'=2) + 0.7 : (s'=1); + <> s=2 -> 0.5 : (s'=2) + 0.5 : (s'=3); + <> s=3 -> 1 : (s'=4); + <> s=4 -> 1 : (s'=3); + +endmodule + +rewards "rew1" + s=0 : 7; + [] s=2 : 1; +endrewards + + +rewards "rew2" + s=0 : 7; + [] s=2 : 1; + [] s=4 : 100; +endrewards diff --git a/resources/examples/testfiles/ma/simple2.ma b/resources/examples/testfiles/ma/simple2.ma new file mode 100644 index 000000000..95e0059b7 --- /dev/null +++ b/resources/examples/testfiles/ma/simple2.ma @@ -0,0 +1,40 @@ + +ma + + +module main + + s : [0..4]; // current state: + + + <> s=0 -> 4 : (s'=1) + 4 : (s'=2); + [alpha] s=1 -> 1 : (s'=0); + [beta] s=1 -> 0.3 : (s'=2) + 0.7 : (s'=1); + [gamma] s=2 -> 1 : (s'=1); + [delta] s=2 -> 0.5 : (s'=2) + 0.5 : (s'=3); + <> s=3 -> 1 : (s'=4); + [lambda] s=4 -> 1 : (s'=3); + +endmodule + +rewards "rew0" + [delta] s=2 : 1; +endrewards + +rewards "rew1" + s=0 : 7; + [delta] s=2 : 1; +endrewards + + +rewards "rew2" + s=0 : 7; + [delta] s=2 : 1; + [lambda] s=4 : 100; +endrewards + +rewards "rew3" + s=0 : 7; + [delta] s=2 : 1; + [gamma] s=4 : 100; +endrewards diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index 1b83be1c6..11d7d48a4 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -140,6 +140,7 @@ namespace { ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} bool isSparseModel() const { return std::is_same::value; } bool isSymbolicModel() const { return std::is_same::value; } + storm::settings::modules::CoreSettings::Engine getEngine() const { return TestType::engine; } template typename std::enable_if::value, std::pair, std::vector>>>::type @@ -362,7 +363,29 @@ namespace { result = checker->check(this->env(), tasks[6]); EXPECT_NEAR(this->parseNumber("0.9100373532"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(CtmcCslModelCheckerTest, simple2) { + std::string formulasString = "R{\"rew1\"}=? [ C ]"; + formulasString += "; R{\"rew2\"}=? [ C ]"; + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ctmc/simple2.sm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // Total reward formulas are currently not supported for non-sparse models. + if (this->isSparseModel()) { + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("23/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result), this->precision())); + } } } \ No newline at end of file diff --git a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp new file mode 100644 index 000000000..4bbf93b75 --- /dev/null +++ b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp @@ -0,0 +1,264 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "test/storm_gtest.h" + +#include "storm/api/builder.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + +#include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/models/symbolic/MarkovAutomaton.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/logic/Formulas.h" +#include "storm/storage/jani/Property.h" +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace { + class SparseDoubleValueIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + class SparseDoubleIntervalIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-6)); + env.solver().minMax().setRelativeTerminationCriterion(false); + return env; + } + }; + class SparseRationalPolicyIterationEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration); + return env; + } + }; + class SparseRationalRationalSearchEnvironment { + public: + static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models + static const storm::settings::modules::CoreSettings::Engine engine = storm::settings::modules::CoreSettings::Engine::Sparse; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::MarkovAutomaton ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch); + return env; + } + }; + + template + class MarkovAutomatonCslModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::MarkovAutomaton SparseModelType; + typedef typename storm::models::symbolic::MarkovAutomaton SymbolicModelType; + + MarkovAutomatonCslModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} + bool isSparseModel() const { return std::is_same::value; } + bool isSymbolicModel() const { return std::is_same::value; } + + template + typename std::enable_if::value, std::pair, std::vector>>>::type + buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSparseModel(program, result.second)->template as(); + return result; + } + + template + typename std::enable_if::value, std::pair, std::vector>>>::type + buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> result; + storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); + program = storm::utility::prism::preprocess(program, constantDefinitionString); + result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); + result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + return std::make_shared>(*model); + } + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + return std::make_shared>(*model); + } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { + return std::make_shared>(*model); + } + } + + bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQualitativeCheckResult().forallTrue(); + } + + ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); + } + + private: + storm::Environment _environment; + + std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { + if (isSparseModel()) { + return std::make_unique(model->template as()->getInitialStates()); + } else { + return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); + } + } + }; + + typedef ::testing::Types< + SparseDoubleValueIterationEnvironment, + SparseDoubleIntervalIterationEnvironment, + SparseRationalPolicyIterationEnvironment, + SparseRationalRationalSearchEnvironment, + > TestingTypes; + + TYPED_TEST_CASE(MarkovAutomatonCslModelCheckerTest, TestingTypes); + + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, server) { + std::string formulasString = "Tmax=? [F \"error\"]"; + formulasString += "; Pmax=? [F \"processB\"]"; + formulasString += "; Pmax=? [F<1 \"error\"]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/server.ma", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(6ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("11/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("2/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.455504"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + } + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple) { + std::string formulasString = "Pmin=? [F<1 s>2]"; + formulasString += "; Pmax=? [F<1.3 s=3]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple.ma", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.6321205588"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("0.727468207"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } + + TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple2) { + std::string formulasString = "R{\"rew0\"}max=? [C]"; + formulasString += "; R{\"rew0\"}min=? [C]"; + formulasString += "; R{\"rew1\"}max=? [C]"; + formulasString += "; R{\"rew1\"}min=? [C]"; + formulasString += "; R{\"rew2\"}max=? [C]"; + formulasString += "; R{\"rew2\"}min=? [C]"; + formulasString += "; R{\"rew3\"}min=? [C]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple2.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(5ul, model->getNumberOfStates()); + EXPECT_EQ(8ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("2"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[2]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + + result = checker->check(this->env(), tasks[3]); + EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[4]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + + result = checker->check(this->env(), tasks[5]); + EXPECT_NEAR(this->parseNumber("7/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[6]); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); + + } +} \ No newline at end of file From 5a16b2befa3134d13e1c6c261f75902e50c83018 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 25 Jun 2018 15:23:25 +0200 Subject: [PATCH 28/29] minor fixes to let the total reward tests compile and pass --- resources/examples/testfiles/ma/simple2.ma | 8 ++-- .../SparseMarkovAutomatonCslModelChecker.cpp | 2 +- .../modelchecker/CtmcCslModelCheckerTest.cpp | 2 +- .../MarkovAutomatonCslModelCheckerTest.cpp | 40 +++++++++++-------- 4 files changed, 30 insertions(+), 22 deletions(-) diff --git a/resources/examples/testfiles/ma/simple2.ma b/resources/examples/testfiles/ma/simple2.ma index 95e0059b7..46fa2207b 100644 --- a/resources/examples/testfiles/ma/simple2.ma +++ b/resources/examples/testfiles/ma/simple2.ma @@ -4,12 +4,13 @@ ma module main - s : [0..4]; // current state: + s : [0..5]; // current state: <> s=0 -> 4 : (s'=1) + 4 : (s'=2); [alpha] s=1 -> 1 : (s'=0); - [beta] s=1 -> 0.3 : (s'=2) + 0.7 : (s'=1); + [beta] s=1 -> 0.3 : (s'=5) + 0.7 : (s'=1); + <> s=5 -> 1 : (s'=2); [gamma] s=2 -> 1 : (s'=1); [delta] s=2 -> 0.5 : (s'=2) + 0.5 : (s'=3); <> s=3 -> 1 : (s'=4); @@ -36,5 +37,6 @@ endrewards rewards "rew3" s=0 : 7; [delta] s=2 : 1; - [gamma] s=4 : 100; + [gamma] s=2 : 100; + [lambda] s=4 : 27; endrewards diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index d72503cae..929ea8721 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -29,7 +29,7 @@ namespace storm { template bool SparseMarkovAutomatonCslModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); - if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) { + if(formula.isInFragment(storm::logic::csl().setGloballyFormulasAllowed(false).setNextFormulasAllowed(false).setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setTimeAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setLongRunAverageRewardFormulasAllowed(true))) { return true; } else { // Check whether we consider a multi-objective formula diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index 11d7d48a4..bf6f8654f 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -384,7 +384,7 @@ namespace { EXPECT_NEAR(this->parseNumber("23/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); result = checker->check(this->env(), tasks[1]); - EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result), this->precision())); + EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result))); } } diff --git a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp index 4bbf93b75..c979c3777 100644 --- a/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MarkovAutomatonCslModelCheckerTest.cpp @@ -135,11 +135,12 @@ namespace { template typename std::enable_if::value, std::shared_ptr>>::type createModelChecker(std::shared_ptr const& model) const { - if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { - return std::make_shared>(*model); - } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { - return std::make_shared>(*model); - } +// if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { +// return std::make_shared>(*model); +// } else if (TestType::engine == storm::settings::modules::CoreSettings::Engine::Dd) { +// return std::make_shared>(*model); +// } + return nullptr; } bool getQualitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { @@ -161,7 +162,8 @@ namespace { if (isSparseModel()) { return std::make_unique(model->template as()->getInitialStates()); } else { - return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); + // return std::make_unique>(model->template as()->getReachableStates(), model->template as()->getInitialStates()); + return nullptr; } } }; @@ -170,7 +172,7 @@ namespace { SparseDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseRationalPolicyIterationEnvironment, - SparseRationalRationalSearchEnvironment, + SparseRationalRationalSearchEnvironment > TestingTypes; TYPED_TEST_CASE(MarkovAutomatonCslModelCheckerTest, TestingTypes); @@ -196,8 +198,10 @@ namespace { result = checker->check(this->env(), tasks[1]); EXPECT_NEAR(this->parseNumber("2/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - result = checker->check(this->env(), tasks[2]); - EXPECT_NEAR(this->parseNumber("0.455504"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + if (!storm::utility::isZero(this->precision())) { + result = checker->check(this->env(), tasks[2]); + EXPECT_NEAR(this->parseNumber("0.455504"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } } @@ -214,11 +218,13 @@ namespace { auto checker = this->createModelChecker(model); std::unique_ptr result; - result = checker->check(this->env(), tasks[0]); - EXPECT_NEAR(this->parseNumber("0.6321205588"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); - - result = checker->check(this->env(), tasks[1]); - EXPECT_NEAR(this->parseNumber("0.727468207"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + if (!storm::utility::isZero(this->precision())) { + result = checker->check(this->env(), tasks[0]); + EXPECT_NEAR(this->parseNumber("0.6321205588"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(this->env(), tasks[1]); + EXPECT_NEAR(this->parseNumber("0.727468207"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } } TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple2) { @@ -230,11 +236,11 @@ namespace { formulasString += "; R{\"rew2\"}min=? [C]"; formulasString += "; R{\"rew3\"}min=? [C]"; - auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple2.nm", formulasString); + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/ma/simple2.ma", formulasString); auto model = std::move(modelFormulas.first); auto tasks = this->getTasks(modelFormulas.second); - EXPECT_EQ(5ul, model->getNumberOfStates()); - EXPECT_EQ(8ul, model->getNumberOfTransitions()); + EXPECT_EQ(6ul, model->getNumberOfStates()); + EXPECT_EQ(11ul, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::MarkovAutomaton); auto checker = this->createModelChecker(model); std::unique_ptr result; From ca2295be1ddaae7a9d90c14bc90af0ddb66337d7 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 25 Jun 2018 15:24:13 +0200 Subject: [PATCH 29/29] updated changelog: support for expected total rewards --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 54be35d3f..150d5ef1b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,7 @@ Version 1.2.x - `storm-dft`: test cases for DFT analysis - Sound value iteration (SVI) for DTMCs and MDPs - Topological solver for linear equation systems and MinMax equation systems. +- Added support for expected total rewards in the sparse engine ### Version 1.2.1 (2018/02)