From 6763871140e5983fda34db135b4236ae5e4b76bd Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 29 Apr 2016 16:47:18 +0200 Subject: [PATCH] Current status Former-commit-id: 067d99e46487a3635c6379f8bb128827530c4ea7 --- stormpy/setup.py | 14 ++++++++++- stormpy/src/common.h | 1 + stormpy/src/core/common.h | 4 --- stormpy/src/core/core.cpp | 4 +-- stormpy/src/core/types.h | 26 -------------------- stormpy/src/includes.h | 37 ++++++++++++++++++++++++++++ stormpy/src/logic/formulas.cpp | 45 +++++++++++----------------------- 7 files changed, 67 insertions(+), 64 deletions(-) delete mode 100644 stormpy/src/core/common.h delete mode 100644 stormpy/src/core/types.h create mode 100644 stormpy/src/includes.h diff --git a/stormpy/setup.py b/stormpy/setup.py index 08204ff4d..934a482d8 100755 --- a/stormpy/setup.py +++ b/stormpy/setup.py @@ -16,7 +16,19 @@ logic_sources = glob(os.path.join('src', 'logic', '*.cpp')) # Configuration shared between external modules follows # To help along, if storm and/or pybind is not system installed, retrieve from storm distribution -include_dirs = ['.', 'src', 'resources/pybind11/include'] +include_dirs = ['.', 'src', 'resources/pybind11/include/'] +# Add more include dirs +# TODO handle by cmake +include_dirs.extend(['../build/include/', '../resources/3rdparty/sylvan/src/', '../resources/3rdparty/exprtk/', '../resources/3rdparty/gmm-5.0/include/']) +carl_dir = "/Users/mvolk/develop/carl/src/" +include_dirs.append(carl_dir) +boost_dir = '/usr/local/include/' +include_dirs.append(boost_dir) +cudd_dirs = ['../resources/3rdparty/cudd-2.5.0/src/obj/', '../resources/3rdparty/cudd-2.5.0/src/cudd', '../resources/3rdparty/cudd-2.5.0/src/mtr/', '../resources/3rdparty/cudd-2.5.0/src/epd/'] +include_dirs.extend(cudd_dirs) +log4cplus_dirs = ['../resources/3rdparty/log4cplus-1.1.3-rc1/include/', '../build/resources/3rdparty/log4cplus-1.1.3-rc1/include/'] +include_dirs.extend(log4cplus_dirs) + local_storm_path = os.path.join(PROJECT_DIR, '..') if os.path.exists(local_storm_path): include_dirs.append(local_storm_path) diff --git a/stormpy/src/common.h b/stormpy/src/common.h index bff6e3be3..bf8a19c39 100644 --- a/stormpy/src/common.h +++ b/stormpy/src/common.h @@ -12,6 +12,7 @@ #include #include +#include "includes.h" namespace py = pybind11; #if PY_MAJOR_VERSION >= 3 diff --git a/stormpy/src/core/common.h b/stormpy/src/core/common.h deleted file mode 100644 index 8ef7c3fa7..000000000 --- a/stormpy/src/core/common.h +++ /dev/null @@ -1,4 +0,0 @@ -#include "types.h" - -//toString -#include "src/helpers.h" diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index 8728f81d4..13a5aab09 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -1,8 +1,8 @@ #include "core.h" -#include "common.h" +#include "src/common.h" -//#include +#include // Thin wrapper for initializing void setupStormLib(std::string const& args) { diff --git a/stormpy/src/core/types.h b/stormpy/src/core/types.h deleted file mode 100644 index e852c6761..000000000 --- a/stormpy/src/core/types.h +++ /dev/null @@ -1,26 +0,0 @@ -#ifndef PYTHON_CORE_TYPES_H_ -#define PYTHON_CORE_TYPES_H_ - -/*#include -#include -#include -#include -#include -#include -#include - -#ifdef PYCARL_USE_CLN -typedef cln::cl_RA Rational; -#else -//typedef double Rational; -typedef mpq_class Rational; -#endif -typedef carl::Monomial::Arg Monomial; -typedef carl::Term Term; -typedef carl::MultivariatePolynomial Polynomial; -typedef carl::FactorizedPolynomial FactorizedPolynomial; -typedef carl::RationalFunction RationalFunction; -typedef carl::RationalFunction FactorizedRationalFunction; -typedef carl::PolynomialFactorizationPair FactorizationPair; -*/ -#endif /* PYTHON_CORE_TYPES_H_ */ diff --git a/stormpy/src/includes.h b/stormpy/src/includes.h new file mode 100644 index 000000000..eee39276d --- /dev/null +++ b/stormpy/src/includes.h @@ -0,0 +1,37 @@ +#ifndef PYTHON_INCLUDES_H_ +#define PYTHON_INCLUDES_H_ + +// Formulae +#include "src/logic/Formula.h" +#include "src/logic/AtomicExpressionFormula.h" +#include "src/logic/AtomicLabelFormula.h" +#include "src/logic/BinaryBooleanStateFormula.h" +#include "src/logic/BinaryPathFormula.h" +#include "src/logic/BinaryStateFormula.h" +#include "src/logic/BooleanLiteralFormula.h" +#include "src/logic/BoundedUntilFormula.h" +#include "src/logic/CumulativeRewardFormula.h" +#include "src/logic/EventuallyFormula.h" +#include "src/logic/GloballyFormula.h" +#include "src/logic/InstantaneousRewardFormula.h" +#include "src/logic/NextFormula.h" +#include "src/logic/PathFormula.h" +#include "src/logic/RewardPathFormula.h" +#include "src/logic/OperatorFormula.h" +#include "src/logic/ProbabilityOperatorFormula.h" +#include "src/logic/ReachabilityRewardFormula.h" +#include "src/logic/LongRunAverageRewardFormula.h" +#include "src/logic/RewardOperatorFormula.h" +#include "src/logic/StateFormula.h" +#include "src/logic/LongRunAverageOperatorFormula.h" +#include "src/logic/ExpectedTimeOperatorFormula.h" +#include "src/logic/UnaryBooleanStateFormula.h" +#include "src/logic/UnaryPathFormula.h" +#include "src/logic/UnaryStateFormula.h" +#include "src/logic/UntilFormula.h" +#include "src/logic/ConditionalPathFormula.h" +#include "src/logic/ProbabilityOperatorFormula.h" +#include "src/logic/RewardOperatorFormula.h" +#include "src/logic/ComparisonType.h" + +#endif /* PYTHON_INCLUDES_H_ */ diff --git a/stormpy/src/logic/formulas.cpp b/stormpy/src/logic/formulas.cpp index e3c448301..47e347d74 100644 --- a/stormpy/src/logic/formulas.cpp +++ b/stormpy/src/logic/formulas.cpp @@ -1,12 +1,9 @@ #include "formulas.h" -#include "common.h" - -#include -#include +#include "src/common.h" void define_formulas(py::module& m) { - + py::enum_(m, "ComparisonType") .value("LESS", storm::logic::ComparisonType::Less) .value("LEQ", storm::logic::ComparisonType::LessEqual) @@ -14,39 +11,25 @@ void define_formulas(py::module& m) { .value("GEQ", storm::logic::ComparisonType::GreaterEqual) ; - /*defineClass>, void, void>("FormulaVec", "Vector of formulas") + /*py::class_>, void, void>("FormulaVec", "Vector of formulas") .def(vector_indexing_suite>, true>()) - ; + ;*/ - //////////////////////////////////////////// - // Formula - //////////////////////////////////////////// - defineClass("Formula", - "Generic Storm Formula") + py::class_>(m, "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"); - + py::class_>(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", py::base>()); + //py::class_(m, "UnaryPathFormula", "Path formula with one operand"); + //py::class_(m, "EventuallyFormula", "Formula for eventually"); + //py::class_(m, "GloballyFormula", "Formula for globally"); + //py::class_(m, "BinaryPathFormula", "Path formula with two operands"); + //py::class_(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound."); + //py::class_(m, "ConditionalPathFormula", "Path Formula with the right hand side being a condition."); + //py::class_(m, "UntilFormula", "Path Formula for unbounded until"); +/* // // Reward Path Formulae //