From 21e678b59c7a8bb3f3ed4e97dc42386cb3aede20 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 20 Jan 2016 16:07:47 +0100 Subject: [PATCH] stormpy logic and using dynamic boost::python version Former-commit-id: 6b203a4d6d5e31db2e9d5fa3cd4bb7d44e51c781 --- CMakeLists.txt | 2 +- setup.py | 11 +++-- src/python/CMakeLists.txt | 25 +--------- src/python/storm-core.cpp | 15 ++---- src/python/storm-logic.cpp | 95 ++++++++++++++++++++++++++++++++++++++ stormpy/logic/__init__.py | 1 + 6 files changed, 110 insertions(+), 39 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 9a7bc31be..6c162b7fe 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -169,7 +169,7 @@ find_package(GMP) ############################################################# # Boost Option variables -set(Boost_USE_STATIC_LIBS ON) +set(Boost_USE_STATIC_LIBS ${USE_BOOST_STATIC_LIBRARIES}) set(Boost_USE_MULTITHREADED ON) set(Boost_USE_STATIC_RUNTIME OFF) diff --git a/setup.py b/setup.py index bfa8592c6..a9c58a489 100644 --- a/setup.py +++ b/setup.py @@ -51,7 +51,7 @@ class MyEggInfo(egg_info): class MyInstall(install): def run(self): - ret = call(["cmake", "-DSTORM_PYTHON=ON", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d) + ret = call(["cmake", "-DSTORM_PYTHON=ON", "-DUSE_BOOST_STATIC_LIBRARIES=OFF", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d) if ret != 0: raise RuntimeError("Cmake exited with return code {}".format(ret)) ret = call(["make", "stormpy"], cwd=d) @@ -60,7 +60,7 @@ class MyInstall(install): install.run(self) class MyDevelop(develop): def run(self): - ret = call(["cmake", "-DSTORM_PYTHON=ON", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d) + ret = call(["cmake", "-DSTORM_PYTHON=ON","-DUSE_BOOST_STATIC_LIBRARIES=OFF", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC, os.path.abspath(os.path.dirname(os.path.realpath(__file__)))], cwd=d) if ret != 0: raise RuntimeError("Cmake exited with return code {}".format(ret)) ret = call(["make", "stormpy"], cwd=d) @@ -74,7 +74,10 @@ setup(cmdclass={'install': MyInstall, 'develop': MyDevelop, 'egg_info': MyEggInf version="0.2", description="Stormpy - Python Bindings for Storm", package_dir={'':d}, - packages=['stormpy', 'stormpy.core', 'stormpy.info'], - package_data={'stormpy.core': ['_core.so'], 'stormpy.info' : ['_info.so'] , 'stormpy': ['*.so', '*.dylib', '*.a']}, + packages=['stormpy', 'stormpy.core', 'stormpy.info', 'stormpy.logic'], + package_data={'stormpy.core': ['_core.so'], + 'stormpy.logic': ['_logic.so'], + 'stormpy.info' : ['_info.so'] , + 'stormpy': ['*.so', '*.dylib', '*.a']}, include_package_data=True) \ No newline at end of file diff --git a/src/python/CMakeLists.txt b/src/python/CMakeLists.txt index 427a3bd30..bc9a1f19e 100644 --- a/src/python/CMakeLists.txt +++ b/src/python/CMakeLists.txt @@ -20,27 +20,6 @@ endfunction() if(STORM_PYTHON) add_python_module(stormpy-info info ${CMAKE_CURRENT_SOURCE_DIR}/storm-info.cpp) add_python_module(stormpy-core core ${CMAKE_CURRENT_SOURCE_DIR}/storm-core.cpp) - - # 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_python_module(stormpy-logic logic ${CMAKE_CURRENT_SOURCE_DIR}/storm-logic.cpp) + add_custom_target(stormpy DEPENDS stormpy-info stormpy-core stormpy-logic) endif() diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp index 4f9dcd2a5..70d5d719c 100644 --- a/src/python/storm-core.cpp +++ b/src/python/storm-core.cpp @@ -30,18 +30,8 @@ BOOST_PYTHON_MODULE(_core) using namespace boost::python; def("setUp", setupStormLib); - //////////////////////////////////////////// - // Formula - //////////////////////////////////////////// - class_, boost::noncopyable>("Formula", no_init) - .def("__str__", &storm::logic::Formula::toString); - class_>>("FormulaVec") - .def(vector_indexing_suite>, true>()) - ; - class_, bases>("ProbabilityOperatorFormula", no_init) - .def("__str__", &storm::logic::ProbabilityOperatorFormula::toString); - register_ptr_to_python>(); + //////////////////////////////////////////// // Program @@ -92,6 +82,9 @@ BOOST_PYTHON_MODULE(_core) defineClass, storm::models::sparse::Model>("SparseParametricMc", ""); defineClass, storm::models::sparse::Model>("SparseParametricMdp", ""); + defineClass>, void, void>("FormulaVec", "Vector of formulas") + .def(vector_indexing_suite>, true>()) + ; def("parse_formulae", storm::parseFormulasForProgram); def("parse_program", storm::parseProgram); diff --git a/src/python/storm-logic.cpp b/src/python/storm-logic.cpp index e69de29bb..78be3af27 100644 --- a/src/python/storm-logic.cpp +++ b/src/python/storm-logic.cpp @@ -0,0 +1,95 @@ +#include +#include +#include "../logic/Formulas.h" + + +#include "helpers.h" +#include "boostPyExtension.h" + + + +BOOST_PYTHON_MODULE(_logic) +{ + using namespace boost::python; + + //////////////////////////////////////////// + // Formula + //////////////////////////////////////////// + defineClass("Formula", + "Generic Storm Formula") + .def("__str__", &storm::logic::Formula::toString) + ; + + // + // Path Formulae + // + defineClass("PathFormula", + "Formula about the probability of a set of paths in an automaton"); + defineClass("UnaryPathFormula", + "Path formula with one operand"); + defineClass("EventuallyFormula", + "Formula for eventually"); + defineClass("GloballyFormula", + "Formula for globally"); + defineClass("BinaryPathFormula", + "Path formula with two operands"); + defineClass("BoundedUntilFormula", + "Until Formula with either a step or a time bound."); + defineClass("ConditionalPathFormula", + "Path Formula with the right hand side being a condition."); + defineClass("UntilFormula", + "Path Formula for unbounded until"); + + + // + // Reward Path Formulae + // + defineClass("RewardPathFormula", + "Formula about the rewards of a set of paths in an automaton"); + defineClass("CumulativeRewardFormula", + "Summed rewards over a the paths"); + defineClass("InstanteneousRewardFormula", + ""); + defineClass("LongRunAverageRewardFormula", + ""); + defineClass("ReachabilityRewardFormula", + ""); + + + // + // State Formulae + // + defineClass("StateFormula", + "Formula about a state of an automaton"); + defineClass("AtomicExpressionFormula", + ""); + defineClass("AtomicLabelFormula", + ""); + defineClass("BooleanLiteralFormula", + ""); + defineClass("UnaryStateFormula", + "State formula with one operand"); + defineClass("UnaryBooleanStateFormula", + ""); + defineClass("OperatorFormula", + ""); + defineClass("ExpectedTimeOperator", + "The expected time between two events"); + defineClass("LongRunAvarageOperator", + ""); + defineClass("ProbabilityOperator", + ""); + defineClass("RewardOperatorFormula", + ""); + defineClass("BinaryStateFormula", + "State formula with two operands"); + defineClass("BooleanBinaryStateFormula", + ""); + + + + + + + +} \ No newline at end of file diff --git a/stormpy/logic/__init__.py b/stormpy/logic/__init__.py index e69de29bb..283bad54d 100644 --- a/stormpy/logic/__init__.py +++ b/stormpy/logic/__init__.py @@ -0,0 +1 @@ +from stormpy.logic._logic import * \ No newline at end of file