From d214e8783e1863bfa5044c58c261902468e132b1 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 3 Sep 2015 17:27:56 +0200 Subject: [PATCH 01/65] first version for python support Former-commit-id: 9a459146a56c3f39ae7226632e06952ece832905 --- CMakeLists.txt | 30 +++++++++++++++++++++++++++--- src/python/storm-info.cpp | 10 ++++++++++ 2 files changed, 37 insertions(+), 3 deletions(-) create mode 100644 src/python/storm-info.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index 4ed4fc438..48f26771e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,5 +1,5 @@ cmake_minimum_required (VERSION 2.8.6) - +cmake_policy(VERSION 3.2) # Set project name project (storm CXX C) @@ -29,6 +29,7 @@ option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF) option(USE_LIBCXX "Sets whether the standard library is libc++." OFF) option(USE_CARL "Sets whether carl should be included." ON) option(FORCE_COLOR "Force color output" ON) +option(STORM_PYTHON "Builds the API for Python" OFF) set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).") set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).") set(CUDA_ROOT "" CACHE STRING "The root directory of CUDA.") @@ -56,8 +57,11 @@ if(CUSTOM_BOOST_ROOT) endif(CUSTOM_BOOST_ROOT) set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb42_20140122_merged-win-lin-mac") - -find_package(Boost REQUIRED) +if(STORM_PYTHON) + find_package(Boost REQUIRED COMPONENTS python3) +else() + find_package(Boost REQUIRED) +endif() find_package(Doxygen REQUIRED) find_package(Gurobi) find_package(TBB) @@ -104,6 +108,13 @@ if(USE_CARL) endif() endif() +if(STORM_PYTHON) + set(Python_ADDITIONAL_VERSIONS 3.4) + FIND_PACKAGE(PythonInterp REQUIRED) + FIND_PACKAGE(PythonLibs 3.4 REQUIRED) + include_directories(${PYTHON_INCLUDE_DIR}) +endif() + message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}") message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") @@ -385,6 +396,8 @@ file(GLOB_RECURSE STORM_HEADERS_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.h) file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp) file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) +file(GLOB_RECURSE STORM_PY_SOURCES ${PROJECT_SOURCE_DIR}/src/python/*.cpp) +file(GLOB_RECURSE STORM_PY_HEADERS ${PROJECT_SOURCE_DIR}/src/python/*.h) file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) @@ -425,8 +438,10 @@ file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) set(STORM_LIB_SOURCES ${STORM_SOURCES_WITHOUT_MAIN}) list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_SOURCES_CLI}) +list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_PY_SOURCES}) set(STORM_LIB_HEADERS ${STORM_HEADERS}) list(REMOVE_ITEM STORM_LIB_HEADERS ${STORM_HEADERS_CLI}) +#list(REMOVE_ITEM STORM_LIB_HEADERS ${STORM_PY_HEADERS}) set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE}) set(STORM_MAIN_HEADERS ${STORM_HEADERS_CLI}) @@ -522,6 +537,15 @@ target_link_libraries(storm-functional-tests storm) add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_MAIN_FILE} ${STORM_PERFORMANCE_TEST_FILES}) target_link_libraries(storm-performance-tests storm) +############################################################# +## +## STORM PYTHON +## +############################################################# +if(STORM_PYTHON) + add_library(stormpy_info SHARED ${STORM_PY_SOURCES}) + target_link_libraries(stormpy storm ${BOOST_PYTHON_LIB} ${PYTHON_LIBRARIES}) +endif() ############################################################# ## ## Boost diff --git a/src/python/storm-info.cpp b/src/python/storm-info.cpp new file mode 100644 index 000000000..027f5541e --- /dev/null +++ b/src/python/storm-info.cpp @@ -0,0 +1,10 @@ +#include +#include "../utility/storm-version.h" + +BOOST_PYTHON_MODULE(libstormpy) +{ + using namespace boost::python; + class_("Version") + .def("short", &storm::utility::StormVersion::shortVersionString) + ; +} \ No newline at end of file From 98e3226fd197f72e0e24d2006e159b45918c159b Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 4 Sep 2015 10:54:23 +0200 Subject: [PATCH 02/65] first version of stormpy (we can parse a prism program) Former-commit-id: dc13d7f183cc989da6f3a1a1903e802e9e4bf1e8 --- CMakeLists.txt | 3 ++- src/CMakeLists.txt | 4 ++++ src/python/CMakeLists.txt | 30 ++++++++++++++++++++++++++++++ src/python/storm-core.cpp | 16 ++++++++++++++++ src/python/storm-info.cpp | 3 ++- stormpy/__init__.py | 0 stormpy/core/__init__.py | 1 + stormpy/info/__init__.py | 1 + 8 files changed, 56 insertions(+), 2 deletions(-) create mode 100644 src/python/CMakeLists.txt create mode 100644 src/python/storm-core.cpp create mode 100644 stormpy/__init__.py create mode 100644 stormpy/core/__init__.py create mode 100644 stormpy/info/__init__.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 77ccb1cf2..5b506affe 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -49,7 +49,8 @@ message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}") # Base path for test files set(STORM_CPP_TESTS_BASE_PATH "${PROJECT_SOURCE_DIR}/test") - +set(STORMPY_OUTPUT_DIR "${PROJECT_BINARY_DIR}/stormpy") +set(STORMPY_SOURCE_DIR "${PROJECT_SOURCE_DIR}/stormpy") ############################################################# ## diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 454fe8262..181e03cee 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -8,6 +8,7 @@ file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/*.h) file(GLOB_RECURSE STORM_HEADERS_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.h) file(GLOB_RECURSE STORM_SOURCES_WITHOUT_MAIN ${PROJECT_SOURCE_DIR}/src/*/*.cpp) file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) +file(GLOB_RECURSE STORM_SOURCES_PYTHON ${PROJECT_SOURCE_DIR}/src/python/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) @@ -45,6 +46,7 @@ file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h) set(STORM_LIB_SOURCES ${STORM_SOURCES_WITHOUT_MAIN}) list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_SOURCES_CLI}) +list(REMOVE_ITEM STORM_LIB_SOURCES ${STORM_SOURCES_PYTHON}) set(STORM_LIB_HEADERS ${STORM_HEADERS}) list(REMOVE_ITEM STORM_LIB_HEADERS ${STORM_HEADERS_CLI}) set(STORM_MAIN_SOURCES ${STORM_SOURCES_CLI} ${STORM_MAIN_FILE}) @@ -115,3 +117,5 @@ INSTALL(TARGETS storm-main LIBRARY DESTINATION lib ARCHIVE DESTINATION lib ) + +add_subdirectory(python EXCLUDE_FROM_ALL) \ No newline at end of file diff --git a/src/python/CMakeLists.txt b/src/python/CMakeLists.txt new file mode 100644 index 000000000..72a1ab63b --- /dev/null +++ b/src/python/CMakeLists.txt @@ -0,0 +1,30 @@ +############################################################# +## +## STORM PYTHON +## +############################################################# +if(STORM_PYTHON) + add_library(stormpy-info SHARED ${CMAKE_CURRENT_SOURCE_DIR}/storm-info.cpp) + target_link_libraries(stormpy-info storm ${BOOST_PYTHON_LIB} ${PYTHON_LIBRARIES}) + set_target_properties(stormpy-info PROPERTIES + OUTPUT_NAME _info + LIBRARY_OUTPUT_DIRECTORY ${STORMPY_OUTPUT_DIR}/info + PREFIX "" + SUFFIX ".so" + ) + add_library(stormpy-core SHARED ${CMAKE_CURRENT_SOURCE_DIR}/storm-core.cpp) + target_link_libraries(stormpy-core storm ${BOOST_PYTHON_LIB} ${PYTHON_LIBRARIES}) + set_target_properties(stormpy-core PROPERTIES + OUTPUT_NAME _core + LIBRARY_OUTPUT_DIRECTORY ${STORMPY_OUTPUT_DIR}/core + PREFIX "" + SUFFIX ".so" + ) + + + add_custom_target(stormpy DEPENDS stormpy-info stormpy-core) + + add_custom_command(TARGET stormpy PRE_BUILD + COMMAND ${CMAKE_COMMAND} -E copy_directory + ${STORMPY_SOURCE_DIR} ${STORMPY_OUTPUT_DIR}) +endif() diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp new file mode 100644 index 000000000..be512bf22 --- /dev/null +++ b/src/python/storm-core.cpp @@ -0,0 +1,16 @@ + +#include +#include "../utility/storm.h" + +BOOST_PYTHON_MODULE(_core) +{ + using namespace boost::python; + def("setUp", storm::utility::setUp); + + class_("Program") + .def("getNumberOfModules", &storm::prism::Program::getNumberOfModules) + ; + + def("parseProgram", storm::parseProgram); + +} \ No newline at end of file diff --git a/src/python/storm-info.cpp b/src/python/storm-info.cpp index 027f5541e..c9d3acc99 100644 --- a/src/python/storm-info.cpp +++ b/src/python/storm-info.cpp @@ -1,10 +1,11 @@ #include #include "../utility/storm-version.h" -BOOST_PYTHON_MODULE(libstormpy) +BOOST_PYTHON_MODULE(_info) { using namespace boost::python; class_("Version") .def("short", &storm::utility::StormVersion::shortVersionString) + .def("long", &storm::utility::StormVersion::longVersionString) ; } \ No newline at end of file diff --git a/stormpy/__init__.py b/stormpy/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/stormpy/core/__init__.py b/stormpy/core/__init__.py new file mode 100644 index 000000000..ab88a96bd --- /dev/null +++ b/stormpy/core/__init__.py @@ -0,0 +1 @@ +from stormpy.core._core import * \ No newline at end of file diff --git a/stormpy/info/__init__.py b/stormpy/info/__init__.py new file mode 100644 index 000000000..0ebe48cb2 --- /dev/null +++ b/stormpy/info/__init__.py @@ -0,0 +1 @@ +from stormpy.info._info import * \ No newline at end of file From 3e9f095cd4b3d1ccf86657d66c824ac5b16ad195 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 7 Sep 2015 18:08:13 +0200 Subject: [PATCH 03/65] new version of storm-core python api Former-commit-id: c37fff4f27c87050ae201d1fd1100fcd8ebb3fbe --- src/python/storm-core.cpp | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp index be512bf22..bcdd4c994 100644 --- a/src/python/storm-core.cpp +++ b/src/python/storm-core.cpp @@ -1,16 +1,37 @@ - #include +#include #include "../utility/storm.h" +#include "../logic/Formulas.h" + +namespace boost { + template T* get_pointer(std::shared_ptr p) { return p.get(); } +} BOOST_PYTHON_MODULE(_core) { using namespace boost::python; def("setUp", storm::utility::setUp); + class_, boost::noncopyable>("Formula", no_init) + .def("toString", &storm::logic::Formula::toString); + class_>>("FormulaVec") + .def(vector_indexing_suite>, true>()) + ; + + + class_, bases>("ProbabilityOperatorFormula", no_init) + .def("toString", &storm::logic::ProbabilityOperatorFormula::toString); class_("Program") .def("getNumberOfModules", &storm::prism::Program::getNumberOfModules) ; - + + + + def("parseFormulae", storm::parseFormulasForProgram); def("parseProgram", storm::parseProgram); + + def("buildAndCheck", storm::buildAndCheckSymbolicModel); + + } \ No newline at end of file From 93a0f7f8bb997b6b6b9169d2e322d21648cce93d Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 9 Sep 2015 12:08:42 +0200 Subject: [PATCH 04/65] settings: checks after config file, added finalize Former-commit-id: 6b3769a7a9366ed86b5b8d3dc9288c65e71ad61d --- src/settings/SettingsManager.cpp | 8 ++++++-- src/settings/SettingsManager.h | 3 ++- src/settings/modules/ModuleSettings.cpp | 4 +++- src/settings/modules/ModuleSettings.h | 7 ++++++- 4 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index 18225f712..618fbfe77 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -137,7 +137,7 @@ namespace storm { } // Finally, check whether all modules are okay with the current settings. - this->checkAllModules(); + this->finalizeAllModules(); } void SettingsManager::setFromConfigurationFile(std::string const& configFilename) { @@ -162,6 +162,8 @@ namespace storm { } } } + // Finally, check whether all modules are okay with the current settings. + this->finalizeAllModules(); } void SettingsManager::printHelp(std::string const& hint) const { @@ -379,9 +381,11 @@ namespace storm { } } - void SettingsManager::checkAllModules() const { + void SettingsManager::finalizeAllModules() { for (auto const& nameModulePair : this->modules) { + nameModulePair.second->finalize(); nameModulePair.second->check(); + } } diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h index f4fad9919..fd00654c3 100644 --- a/src/settings/SettingsManager.h +++ b/src/settings/SettingsManager.h @@ -189,9 +189,10 @@ namespace storm { static void addOptionToMap(std::string const& name, std::shared_ptr