Current status

Former-commit-id: 067d99e464

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)

stormpy/src/common.h

@@ -12,6 +12,7 @@
 #include <pybind11/stl.h>
 #include <tuple>
 
+#include "includes.h"
 namespace py = pybind11;
 
 #if PY_MAJOR_VERSION >= 3

stormpy/src/core/common.h

@@ -1,4 +0,0 @@
-#include "types.h"
-
-//toString
-#include "src/helpers.h"

stormpy/src/core/core.cpp

@@ -1,8 +1,8 @@
 #include "core.h"
 
-#include "common.h"
+#include "src/common.h"
 
-//#include <src/utility/storm.h>
+#include <src/utility/storm.h>
 
 // Thin wrapper for initializing
 void setupStormLib(std::string const& args) {

stormpy/src/core/types.h

@@ -1,26 +0,0 @@
-#ifndef PYTHON_CORE_TYPES_H_
-#define PYTHON_CORE_TYPES_H_
-
-/*#include <carl/numbers/numbers.h>
-#include <carl/core/Variable.h>
-#include <carl/core/Monomial.h>
-#include <carl/core/Term.h>
-#include <carl/core/MultivariatePolynomial.h>
-#include <carl/core/FactorizedPolynomial.h>
-#include <carl/core/RationalFunction.h>
-
-#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<Rational> Term;
-typedef carl::MultivariatePolynomial<Rational> Polynomial;
-typedef carl::FactorizedPolynomial<Polynomial> FactorizedPolynomial;
-typedef carl::RationalFunction<Polynomial> RationalFunction;
-typedef carl::RationalFunction<FactorizedPolynomial> FactorizedRationalFunction;
-typedef carl::PolynomialFactorizationPair<Polynomial> FactorizationPair;
-*/
-#endif /* PYTHON_CORE_TYPES_H_ */

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_ */

stormpy/src/logic/formulas.cpp

@@ -1,12 +1,9 @@
 #include "formulas.h"
 
-#include "common.h"
-
-#include <src/logic/Formulas.h>
-#include <src/logic/ComparisonType.h>
+#include "src/common.h"
 
 void define_formulas(py::module& m) {
-    
+ 
     py::enum_<storm::logic::ComparisonType>(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<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
+    /*py::class_<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>())
-    ;
+    ;*/
     
-    ////////////////////////////////////////////
-    // Formula
-    ////////////////////////////////////////////
-    defineClass<storm::logic::Formula, void, boost::noncopyable>("Formula",
-    "Generic Storm Formula")
+    py::class_<std::shared_ptr<storm::logic::Formula>>(m, "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");
-
+    py::class_<std::shared_ptr<storm::logic::PathFormula>>(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", py::base<std::shared_ptr<storm::logic::Formula>>());
+    //py::class_<storm::logic::UnaryPathFormula, storm::logic::PathFormula>(m, "UnaryPathFormula", "Path formula with one operand");
+    //py::class_<storm::logic::EventuallyFormula, storm::logic::UnaryPathFormula>(m, "EventuallyFormula", "Formula for eventually");
+    //py::class_<storm::logic::GloballyFormula, storm::logic::UnaryPathFormula>(m, "GloballyFormula", "Formula for globally");
+    //py::class_<storm::logic::BinaryPathFormula, storm::logic::PathFormula>(m, "BinaryPathFormula", "Path formula with two operands");
+    //py::class_<storm::logic::BoundedUntilFormula, storm::logic::BinaryPathFormula>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.");
+    //py::class_<storm::logic::ConditionalPathFormula, storm::logic::BinaryPathFormula>(m, "ConditionalPathFormula", "Path Formula with the right hand side being a condition.");
+    //py::class_<storm::logic::UntilFormula, storm::logic::BinaryPathFormula>(m, "UntilFormula", "Path Formula for unbounded until");
 
+/*
     //
     // Reward Path Formulae
     //