Merge branch 'python_api' of https://sselab.de/lab9/private/git/storm into python_api

Former-commit-id: 87687bb945

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)
 

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,11 @@ 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', 'stormpy.expressions'],
+      package_data={'stormpy.core': ['_core.so'],
+                    'stormpy.logic': ['_logic.so'],
+                    'stormpy.info' : ['_info.so'] ,
+                    'stormpy.expressions' : ['_expressions.so'],
+                     'stormpy': ['*.so', '*.dylib', '*.a']},
 
       include_package_data=True)

src/python/CMakeLists.txt

@@ -20,27 +20,7 @@ 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_python_module(stormpy-expression expressions ${CMAKE_CURRENT_SOURCE_DIR}/storm-expression.cpp)
+    add_custom_target(stormpy DEPENDS stormpy-info stormpy-core stormpy-logic stormpy-expression)
 endif()

src/python/storm-core.cpp

@@ -41,18 +41,8 @@ BOOST_PYTHON_MODULE(_core)
     using namespace boost::python;
     def("setUp", setupStormLib);
 
-    ////////////////////////////////////////////
-    // Formula
-    ////////////////////////////////////////////
-    class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula>, boost::noncopyable>("Formula", no_init)
-        .def("__str__", &storm::logic::Formula::toString);
-	class_<std::vector<std::shared_ptr<storm::logic::Formula>>>("FormulaVec")
-			.def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
-			;
-    class_<storm::logic::ProbabilityOperatorFormula, std::shared_ptr<storm::logic::ProbabilityOperatorFormula>, bases<storm::logic::Formula>>("ProbabilityOperatorFormula", no_init)
-        .def("__str__", &storm::logic::ProbabilityOperatorFormula::toString);
 
-    register_ptr_to_python<std::shared_ptr<storm::logic::Formula>>();
+
 
     ////////////////////////////////////////////
     // Program
@@ -104,6 +94,9 @@ BOOST_PYTHON_MODULE(_core)
     defineClass<storm::models::sparse::Dtmc<storm::RationalFunction>,  storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMc", "");
     defineClass<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Model<storm::RationalFunction>>("SparseParametricMdp", "");
 
+    defineClass<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
+            .def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
+            ;
 
     def("parse_formulae", storm::parseFormulasForProgram);
     def("parse_program", storm::parseProgram);

src/python/storm-expression.cpp

@@ -0,0 +1,19 @@
+#include <boost/python.hpp>
+#include <boost/python/suite/indexing/vector_indexing_suite.hpp>
+
+#include "helpers.h"
+#include "boostPyExtension.h"
+
+#include "../storage/expressions/ExpressionManager.h"
+
+
+BOOST_PYTHON_MODULE(_expressions)
+{
+    using namespace boost::python;
+
+    defineClass<storm::expressions::ExpressionManager, void, boost::noncopyable>("ExpressionManager",
+    "Manages variables for expressions");
+    defineClass<storm::expressions::Expression, void, boost::noncopyable>("Expression",
+    "");
+
+}

src/python/storm-logic.cpp

@@ -0,0 +1,95 @@
+#include <boost/python.hpp>
+#include <boost/python/suite/indexing/vector_indexing_suite.hpp>
+#include "../logic/Formulas.h"
+
+
+#include "helpers.h"
+#include "boostPyExtension.h"
+
+
+
+BOOST_PYTHON_MODULE(_logic)
+{
+    using namespace boost::python;
+
+    ////////////////////////////////////////////
+    // Formula
+    ////////////////////////////////////////////
+    defineClass<storm::logic::Formula, void, boost::noncopyable>("Formula",
+    "Generic Storm Formula")
+        .def("__str__", &storm::logic::Formula::toString)
+    ;
+
+    //
+    // Path Formulae
+    //
+    defineClass<storm::logic::PathFormula, storm::logic::Formula, boost::noncopyable>("PathFormula",
+    "Formula about the probability of a set of paths in an automaton");
+    defineClass<storm::logic::UnaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("UnaryPathFormula",
+    "Path formula with one operand");
+    defineClass<storm::logic::EventuallyFormula, storm::logic::UnaryPathFormula>("EventuallyFormula",
+    "Formula for eventually");
+    defineClass<storm::logic::GloballyFormula, storm::logic::UnaryPathFormula>("GloballyFormula",
+    "Formula for globally");
+    defineClass<storm::logic::BinaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("BinaryPathFormula",
+    "Path formula with two operands");
+    defineClass<storm::logic::BoundedUntilFormula, storm::logic::BinaryPathFormula, boost::noncopyable>("BoundedUntilFormula",
+    "Until Formula with either a step or a time bound.");
+    defineClass<storm::logic::ConditionalPathFormula, storm::logic::BinaryPathFormula>("ConditionalPathFormula",
+    "Path Formula with the right hand side being a condition.");
+    defineClass<storm::logic::UntilFormula, storm::logic::BinaryPathFormula>("UntilFormula",
+    "Path Formula for unbounded until");
+
+
+    //
+    // Reward Path Formulae
+    //
+    defineClass<storm::logic::RewardPathFormula, storm::logic::Formula, boost::noncopyable>("RewardPathFormula",
+    "Formula about the rewards of a set of paths in an automaton");
+    defineClass<storm::logic::CumulativeRewardFormula, storm::logic::RewardPathFormula>("CumulativeRewardFormula",
+    "Summed rewards over a the paths");
+    defineClass<storm::logic::InstantaneousRewardFormula, storm::logic::RewardPathFormula>("InstanteneousRewardFormula",
+    "");
+    defineClass<storm::logic::LongRunAverageRewardFormula, storm::logic::RewardPathFormula>("LongRunAverageRewardFormula",
+    "");
+    defineClass<storm::logic::ReachabilityRewardFormula, storm::logic::RewardPathFormula>("ReachabilityRewardFormula",
+    "");
+
+
+    //
+    // State Formulae
+    //
+    defineClass<storm::logic::StateFormula, storm::logic::Formula, boost::noncopyable>("StateFormula",
+    "Formula about a state of an automaton");
+    defineClass<storm::logic::AtomicExpressionFormula, storm::logic::StateFormula>("AtomicExpressionFormula",
+    "");
+    defineClass<storm::logic::AtomicLabelFormula, storm::logic::StateFormula>("AtomicLabelFormula",
+    "");
+    defineClass<storm::logic::BooleanLiteralFormula, storm::logic::StateFormula>("BooleanLiteralFormula",
+    "");
+    defineClass<storm::logic::UnaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("UnaryStateFormula",
+    "State formula with one operand");
+    defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula",
+    "");
+    defineClass<storm::logic::OperatorFormula, storm::logic::UnaryStateFormula, boost::noncopyable>("OperatorFormula",
+    "");
+    defineClass<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator",
+    "The expected time between two events");
+    defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator",
+    "");
+    defineClass<storm::logic::ProbabilityOperatorFormula, storm::logic::OperatorFormula>("ProbabilityOperator",
+    "");
+    defineClass<storm::logic::RewardOperatorFormula, storm::logic::OperatorFormula>("RewardOperatorFormula",
+    "");
+    defineClass<storm::logic::BinaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("BinaryStateFormula",
+    "State formula with two operands");
+    defineClass<storm::logic::BinaryBooleanStateFormula, storm::logic::BinaryStateFormula>("BooleanBinaryStateFormula",
+    "");
+
+
+
+
+
+
+
+}

stormpy/expressions/__init__.py

@@ -0,0 +1 @@
+from stormpy.expressions._expressions import *

stormpy/logic/__init__.py

@@ -0,0 +1 @@
+from stormpy.logic._logic import *