diff --git a/setup.py b/setup.py deleted file mode 100644 index f2d70890d..000000000 --- a/setup.py +++ /dev/null @@ -1,122 +0,0 @@ -from setuptools import setup, find_packages -from setuptools.command.install import install -from setuptools.command.develop import develop -from setuptools.command.egg_info import egg_info -from subprocess import call, STDOUT -import distutils.sysconfig -import os -import os.path -import tempfile -import glob -import shutil -import distutils -import multiprocessing -print(os.getcwd()) - - -PYTHONINC = distutils.sysconfig.get_python_inc() -PYTHONLIB = distutils.sysconfig.get_python_lib(plat_specific=True, standard_lib=True) -PYTHONLIBDIR = distutils.sysconfig.get_config_var("LIBDIR") -PYTHONLIBS = glob.glob(os.path.join(PYTHONLIBDIR, "*.dylib")) -PYTHONLIBS.extend(glob.glob(os.path.join(PYTHONLIBDIR, "*.so"))) -PYTHONLIB = PYTHONLIBS[0] - -NO_COMPILE_CORES = multiprocessing.cpu_count() -#print(os.path.abspath(os.path.join(os.path.dirname(os.path.realpath(__file__)), os.pardir))) -#print(PYTHONINC) -#print(PYTHONLIB) - -d = "setuppy_build" - -PROJECT_PYTHON_DIR = "stormpy" -PROJECT_PYTHON_FILES = os.path.join(os.path.dirname(os.path.realpath(__file__)), PROJECT_PYTHON_DIR) -PROJECT_PYTHON_TMP_DESTINATION = os.path.join(os.path.realpath(d), PROJECT_PYTHON_DIR) - -print(d) -if not os.path.exists(d): - os.makedirs(d) - -class MyEggInfo(egg_info): - def run(self): - try: - src = PROJECT_PYTHON_FILES - print(src) - dst = PROJECT_PYTHON_TMP_DESTINATION - print(dst) - distutils.dir_util.copy_tree(src, dst) - egg_info.run(self) - except: - print("Exception occurred") - egg_info.run(self) - - -class MyInstall(install): - user_options = install.user_options + [ - ('cmake=', None, 'Additional cmake arguments'), - ('make=', None, 'Additional make arguments'), - ] - - def initialize_options(self): - install.initialize_options(self) - self.cmake = "" - self.make = "" - - def run(self): - # Call cmake - cmake_args = ["cmake", "-DSTORM_PYTHON=ON", "-DUSE_BOOST_STATIC_LIBRARIES=OFF", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC] - cmake_args.extend(self.cmake.split()) - cmake_args.append(os.path.abspath(os.path.dirname(os.path.realpath(__file__)))) - ret = call(cmake_args, cwd=d) - if ret != 0: - raise RuntimeError("Cmake exited with return code {}".format(ret)) - - # Call make - make_args = ["make", "stormpy", "-j"+str(NO_COMPILE_CORES)] - make_args.extend(self.make.split()) - ret = call(make_args, cwd=d) - if ret != 0: - raise RuntimeError("Make exited with return code {}".format(ret)) - install.run(self) - -class MyDevelop(develop): - user_options = develop.user_options + [ - ('cmake=', None, 'Additional cmake arguments'), - ('make=', None, 'Additional make arguments'), - ] - - def initialize_options(self): - develop.initialize_options(self) - self.cmake = "" - self.make = "" - - def run(self): - # Call cmake - cmake_args = ["cmake", "-DSTORM_PYTHON=ON", "-DUSE_BOOST_STATIC_LIBRARIES=OFF", "-DPYTHON_LIBRARY="+PYTHONLIB, "-DPYTHON_INCLUDE_DIR="+PYTHONINC] - cmake_args.extend(self.cmake.split()) - cmake_args.append(os.path.abspath(os.path.dirname(os.path.realpath(__file__)))) - ret = call(cmake_args, cwd=d) - if ret != 0: - raise RuntimeError("Cmake exited with return code {}".format(ret)) - - # Call make - make_args = ["make", "stormpy", "-j"+str(NO_COMPILE_CORES)] - make_args.extend(self.make.split()) - ret = call(make_args, cwd=d) - if ret != 0: - raise RuntimeError("Make exited with return code {}".format(ret)) - develop.run(self) - - -setup(cmdclass={'install': MyInstall, 'develop': MyDevelop, 'egg_info': MyEggInfo}, - name="stormpy", - version="0.2", - description="Stormpy - Python Bindings for Storm", - package_dir={'':d}, - 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) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c36e4c9c2..d75204355 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -8,7 +8,6 @@ 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) @@ -51,7 +50,6 @@ 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}) @@ -129,5 +127,3 @@ INSTALL(TARGETS storm-main LIBRARY DESTINATION lib ARCHIVE DESTINATION lib ) - -add_subdirectory(python EXCLUDE_FROM_ALL) diff --git a/src/python/CMakeLists.txt b/src/python/CMakeLists.txt deleted file mode 100644 index 7837bc169..000000000 --- a/src/python/CMakeLists.txt +++ /dev/null @@ -1,26 +0,0 @@ -############################################################# -## -## STORM PYTHON -## -############################################################# - -function (add_python_module _libname _modulename _sources) - add_library(${_libname} SHARED ${_sources}) - target_link_libraries(${_libname} storm ${BOOST_PYTHON_LIB} ${PYTHON_LIBRARIES}) - set_target_properties(${_libname} PROPERTIES - OUTPUT_NAME "_${_modulename}" - LIBRARY_OUTPUT_DIRECTORY "${STORMPY_OUTPUT_DIR}/${_modulename}" - PREFIX "" - SUFFIX ".so" - ) -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_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() diff --git a/src/python/boostPyExtension.h b/src/python/boostPyExtension.h deleted file mode 100644 index ad3a36f37..000000000 --- a/src/python/boostPyExtension.h +++ /dev/null @@ -1,44 +0,0 @@ -#pragma once -#include - - -namespace boost { namespace python { namespace converter { - - template - PyObject* shared_ptr_to_python(std::shared_ptr const& x) - { - if (!x) - return python::detail::none(); - else if (shared_ptr_deleter* d = std::get_deleter(x)) - return incref( d->owner.get() ); - else - return converter::registered const&>::converters.to_python(&x); - } - - /// @brief Adapter a non-member function that returns a unique_ptr to - /// a python function object that returns a raw pointer but - /// explicitly passes ownership to Python. - template - object adapt_unique(std::unique_ptr (*fn)(Args...)) - { - return make_function( - [fn](Args... args) { return fn(args...).release(); }, - return_value_policy(), - boost::mpl::vector() - ); - } - - /// @brief Adapter a member function that returns a unique_ptr to - /// a python function object that returns a raw pointer but - /// explicitly passes ownership to Python. - template - object adapt_unique(std::unique_ptr (C::*fn)(Args...)) - { - return make_function( - [fn](C& self, Args... args) { return (self.*fn)(args...).release(); }, - python::return_value_policy(), - boost::mpl::vector() - ); - } - -}}} // namespace boost::python::converter diff --git a/src/python/helpers.h b/src/python/helpers.h deleted file mode 100644 index f37d350d9..000000000 --- a/src/python/helpers.h +++ /dev/null @@ -1,57 +0,0 @@ -#pragma once - -#include - -template -void shared_ptr_implicitly_convertible() { - boost::python::implicitly_convertible, std::shared_ptr>(); -} - -template -void register_shared_ptr() { - boost::python::register_ptr_to_python>(); - boost::python::register_ptr_to_python>(); - -} - - - -namespace dtl{ -// primary class template - template - struct ImplConversionSharedPtr { - void c() { shared_ptr_implicitly_convertible(); } - }; - -// specialized class template - template - struct ImplConversionSharedPtr::value>::type> { - void c() { } - }; - - template - struct bases_holder { - typedef boost::python::bases Type; - }; - - template<> - struct bases_holder { - typedef boost::python::bases<> Type; - }; -} - -template -boost::python::class_, typename dtl::bases_holder::Type, NC> defineClass(char const* name, char const* docstring, typename std::enable_if_t::value>::type* = 0) { - auto inst = boost::python::class_, typename dtl::bases_holder::Type, NC>(name, docstring); - register_shared_ptr(); - dtl::ImplConversionSharedPtr().c(); - return inst; -}; - -template -boost::python::class_, typename dtl::bases_holder::Type, NC> defineClass(char const* name, char const* docstring) { - auto inst = boost::python::class_, typename dtl::bases_holder::Type, NC>(name, docstring, boost::python::no_init); - register_shared_ptr(); - dtl::ImplConversionSharedPtr().c(); - return inst; -}; diff --git a/src/python/storm-core.cpp b/src/python/storm-core.cpp deleted file mode 100644 index 4bde9ca91..000000000 --- a/src/python/storm-core.cpp +++ /dev/null @@ -1,130 +0,0 @@ -#include -#include -#include "../utility/storm.h" -#include "../logic/Formulas.h" - -#include - -#include "helpers.h" -#include "boostPyExtension.h" - -// Holds the rational function and constraints after parametric model checking -class PmcResult { -public: - storm::RationalFunction resultFunction; - std::unordered_set> constraintsWellFormed; - std::unordered_set> constraintsGraphPreserving; -}; - -// Thin wrapper for model building -std::shared_ptr buildModel(storm::prism::Program const& program, std::shared_ptr const& formula) { - return storm::buildSymbolicModel(program, std::vector>(1,formula)).model; -} - -// Thin wrapper for parametric state elimination -std::shared_ptr performStateElimination(std::shared_ptr> model, std::shared_ptr const& formula) { - std::unique_ptr checkResult = storm::verifySparseModel(model, formula); - std::shared_ptr result = std::make_shared(); - result->resultFunction = (checkResult->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()]); - storm::models::sparse::Dtmc::ConstraintCollector constraintCollector(*(model->template as>())); - result->constraintsWellFormed = constraintCollector.getWellformedConstraints(); - result->constraintsGraphPreserving = constraintCollector.getGraphPreservingConstraints(); - return result; -} - -// Thin wrapper for initializing -void setupStormLib(std::string const& args) { - storm::utility::setUp(); - storm::settings::SettingsManager::manager().setFromString(args); -} - -BOOST_PYTHON_MODULE(_core) -{ - using namespace boost::python; - def("set_up", setupStormLib); - - - //////////////////////////////////////////// - // Program - //////////////////////////////////////////// - - defineClass("Program", "") - .add_property("nr_modules", &storm::prism::Program::getNumberOfModules) - ; - - - //////////////////////////////////////////// - // PmcResult - //////////////////////////////////////////// - class_, boost::noncopyable>("PmcResult", "Holds the results after parametric model checking") - .add_property("result_function", &PmcResult::resultFunction) - .add_property("constraints_well_formed", &PmcResult::constraintsWellFormed) - .add_property("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving) - ; - register_ptr_to_python>(); - - - //////////////////////////////////////////// - // Models - //////////////////////////////////////////// - - enum_("ModelType") - .value("DTMC", storm::models::ModelType::Dtmc) - .value("MDP", storm::models::ModelType::Mdp) - .value("CTMC", storm::models::ModelType::Ctmc) - .value("MA", storm::models::ModelType::MarkovAutomaton) - ; - - defineClass("ModelBase", "") - .add_property("nr_states", &storm::models::ModelBase::getNumberOfStates) - .add_property("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions) - .add_property("model_type", &storm::models::ModelBase::getType) - .add_property("parametric", &storm::models::ModelBase::isParametric) - .def("as_dtmc", &storm::models::ModelBase::as>) - .def("as_pdtmc", &storm::models::ModelBase::as>) - .def("as_mdp", &storm::models::ModelBase::as>) - .def("as_pmdp", &storm::models::ModelBase::as>) - ; - - - defineClass, storm::models::ModelBase, boost::noncopyable>("SparseModel", - "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); - defineClass, storm::models::sparse::Model, boost::noncopyable>("SparseDtmc", ""); - defineClass, storm::models::sparse::Model>("SparseMdp", ""); - - defineClass, storm::models::ModelBase, boost::noncopyable>("SparseParametricModel", "") - .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters) - ; - defineClass, storm::models::sparse::Model>("SparseParametricDtmc", ""); - defineClass, storm::models::sparse::Model>("SparseParametricMdp", ""); - - - //////////////////////////////////////////// - // Bisimulation - //////////////////////////////////////////// - enum_("BisimulationType") - .value("STRONG", storm::storage::BisimulationType::Strong) - .value("WEAK", storm::storage::BisimulationType::Weak) - ; - def("perform_bisimulation_parametric", static_cast> (*)(std::shared_ptr> const&, std::shared_ptr const&, storm::storage::BisimulationType)>(&storm::performBisimulationMinimization>)); - - - - def("parse_formulae", storm::parseFormulasForProgram); - def("parse_program", storm::parseProgram); - - def("build_model", buildModel, return_value_policy()); - - def("build_model_from_prism_program", storm::buildSymbolicModel); - def("build_parametric_model_from_prism_program", storm::buildSymbolicModel); - - ////////////////////////////////////////////// - // Model Checking - ////////////////////////////////////////////// - class_("ModelProgramPair", no_init) - .add_property("model", &storm::storage::ModelFormulasPair::model) - .add_property("program", &storm::storage::ModelFormulasPair::formulas) - ; - - def("perform_state_elimination", performStateElimination); -} diff --git a/src/python/storm-logic.cpp b/src/python/storm-logic.cpp deleted file mode 100644 index e2934859c..000000000 --- a/src/python/storm-logic.cpp +++ /dev/null @@ -1,104 +0,0 @@ -#include -#include -#include "../logic/Formulas.h" - - -#include "helpers.h" -#include "boostPyExtension.h" -// Less, LessEqual, Greater, GreaterEqual - - -BOOST_PYTHON_MODULE(_logic) -{ - using namespace boost::python; - - enum_("ComparisonType") - .value("LESS", storm::logic::ComparisonType::Less) - .value("LEQ", storm::logic::ComparisonType::LessEqual) - .value("GREATER", storm::logic::ComparisonType::Greater) - .value("GEQ", storm::logic::ComparisonType::GreaterEqual) - ; - - defineClass>, void, void>("FormulaVec", "Vector of formulas") - .def(vector_indexing_suite>, true>()) - ; - - //////////////////////////////////////////// - // 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", - "") - .add_property("has_bound", &storm::logic::OperatorFormula::hasBound) - .add_property("bound", &storm::logic::OperatorFormula::getBound, &storm::logic::OperatorFormula::setBound) - .add_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType) - ; - defineClass("ExpectedTimeOperator", - "The expected time between two events"); - defineClass("LongRunAvarageOperator", - ""); - defineClass("ProbabilityOperator", - ""); - defineClass("RewardOperatorFormula", - ""); - defineClass("BinaryStateFormula", - "State formula with two operands"); - defineClass("BooleanBinaryStateFormula", - ""); - -} diff --git a/stormpy_old/__init__.py b/stormpy_old/__init__.py deleted file mode 100644 index e69de29bb..000000000 diff --git a/stormpy_old/core/__init__.py b/stormpy_old/core/__init__.py deleted file mode 100644 index 977c7f2c8..000000000 --- a/stormpy_old/core/__init__.py +++ /dev/null @@ -1,20 +0,0 @@ -from stormpy.core._core import * - -def _build_model(program, formulae): - intermediate = _core.build_model(program, formulae) - if intermediate.parametric: - if intermediate.model_type == ModelType.DTMC: - return intermediate.as_pdtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate.as_pmdp() - else: - raise RuntimeError("Not supported parametric model constructed") - else: - if intermediate.model_type == ModelType.DTMC: - return intermediate.as_pdtmc() - elif intermediate.model_type == ModelType.MDP: - return intermediate.as_pmdp() - else: - raise RuntimeError("Not supported non-parametric model constructed") - -build_model = _build_model \ No newline at end of file diff --git a/stormpy_old/expressions/__init__.py b/stormpy_old/expressions/__init__.py deleted file mode 100644 index 6522889ea..000000000 --- a/stormpy_old/expressions/__init__.py +++ /dev/null @@ -1 +0,0 @@ -from stormpy.expressions._expressions import * \ No newline at end of file diff --git a/stormpy_old/info/__init__.py b/stormpy_old/info/__init__.py deleted file mode 100644 index 0ebe48cb2..000000000 --- a/stormpy_old/info/__init__.py +++ /dev/null @@ -1 +0,0 @@ -from stormpy.info._info import * \ No newline at end of file diff --git a/stormpy_old/logic/__init__.py b/stormpy_old/logic/__init__.py deleted file mode 100644 index 283bad54d..000000000 --- a/stormpy_old/logic/__init__.py +++ /dev/null @@ -1 +0,0 @@ -from stormpy.logic._logic import * \ No newline at end of file