Workaround for problems with def_property() by changing to simple def()

Former-commit-id: b457d861c9

stormpy/setup.py

@@ -90,7 +90,7 @@ ext_logic = Extension(
     extra_link_args=extra_link_args
 )
 
-ext_logic = Extension(
+ext_storage = Extension(
     name='storage.storage',
     sources=['src/mod_storage.cpp'] + storage_sources,
     include_dirs=include_dirs,
@@ -154,7 +154,7 @@ setup(name="stormpy",
       packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic'],
       package_dir={'':'lib'},
       ext_package='stormpy',
-      ext_modules=[ext_core, ext_info, ext_expressions, ext_logic
+      ext_modules=[ext_core, ext_info, ext_expressions, ext_logic, ext_storage
                    ],
       cmdclass={
         'build_ext': stormpy_build_ext,

stormpy/src/core/core.cpp

@@ -1,9 +1,8 @@
 #include "core.h"
 
 void define_core(py::module& m) {
-    
     // Init
-    m.def("set_up", [] (std::string const& args) {
+    m.def("set_up", [](std::string const& args) {
             storm::utility::setUp();
             storm::settings::SettingsManager::manager().setFromString(args);
         }, "Initialize Storm", py::arg("arguments"));
@@ -16,8 +15,12 @@ void define_parse(py::module& m) {
 
     // Pair <Model,Formulas>
     py::class_<storm::storage::ModelFormulasPair>(m, "ModelFormulasPair", "Pair of model and formulas")
-        .def_readwrite("model", &storm::storage::ModelFormulasPair::model, "The model")
+        .def("model", [](storm::storage::ModelFormulasPair const& pair) {
-        .def_readwrite("formulas", &storm::storage::ModelFormulasPair::formulas, "The formulas")
+                return pair.model;
+            }, "The model")
+        .def("formulas", [](storm::storage::ModelFormulasPair const& pair) {
+                return pair.formulas;
+            }, "The formulas")
     ;
 
     // Parse explicit models
@@ -31,7 +34,6 @@ std::shared_ptr<storm::models::ModelBase> buildModel(storm::prism::Program const
 }
 
 void define_build(py::module& m) {
-   
     // Build model
     m.def("_build_model", &buildModel<double>, "Build the model", py::arg("program"), py::arg("formula"));
     m.def("_build_parametric_model", &buildModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formula"));

stormpy/src/core/modelchecking.cpp

@@ -7,6 +7,18 @@ class PmcResult {
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsWellFormed;
         std::unordered_set<storm::ArithConstraint<storm::RationalFunction>> constraintsGraphPreserving;
 
+        storm::RationalFunction getResultFunction() const {
+            return resultFunction;
+        }
+
+        std::unordered_set<storm::ArithConstraint<storm::RationalFunction>>  getConstraintsWellFormed() const {
+            return constraintsWellFormed;
+        }
+
+        std::unordered_set<storm::ArithConstraint<storm::RationalFunction>>  getConstraintsGraphPreserving() const {
+            return constraintsGraphPreserving;
+        }
+
         std::string toString() {
             std::stringstream stream;
             stream << resultFunction << std::endl;
@@ -49,9 +61,9 @@ void define_modelchecking(py::module& m) {
     // PmcResult
     py::class_<PmcResult, std::shared_ptr<PmcResult>>(m, "PmcResult", "Holds the results after parametric model checking")
         .def("__str__", &PmcResult::toString)
-        .def_readonly("result_function", &PmcResult::resultFunction, "Result as rational function")
+        .def("result_function", &PmcResult::getResultFunction, "Result as rational function")
-        .def_readonly("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
+        .def("constraints_well_formed", &PmcResult::getConstraintsWellFormed, "Constraints ensuring well-formed probabilities")
-        .def_readonly("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
+        .def("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation")
     ;
 
 }

stormpy/src/mod_storage.cpp

@@ -4,7 +4,7 @@
 #include "storage/matrix.h"
 
 PYBIND11_PLUGIN(storage) {
-    py::module m("storage");
+    py::module m("stormpy.storage");
     define_model(m);
     define_sparse_matrix(m);
     return m.ptr();

stormpy/src/storage/matrix.cpp

@@ -12,12 +12,13 @@ void define_sparse_matrix(py::module& m) {
                 stream << entry;
                 return stream.str();
             })
-        .def_property("val", &storm::storage::MatrixEntry<entry_index, double>::getValue, &storm::storage::MatrixEntry<entry_index, double>::setValue, "Value")
+        //def_property threw "pointer being freed not allocated" after exiting
-        .def_property_readonly("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
+        .def("val", &storm::storage::MatrixEntry<entry_index, double>::getValue, "Value")
+        .def("set_val", &storm::storage::MatrixEntry<entry_index, double>::setValue, "Set value")
+        .def("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
     ;
  
     py::class_<storm::storage::SparseMatrix<double>>(m, "SparseMatrix", "Sparse matrix")
-        //.def("__str__", &storm::logic::Formula::toString)
         .def("__iter__", [](storm::storage::SparseMatrix<double> const& matrix) {
                 return py::make_iterator(matrix.begin(), matrix.end());
             }, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */)

stormpy/src/storage/model.cpp

@@ -16,6 +16,7 @@ std::vector<storm::storage::sparse::state_type> getInitialStates(storm::models::
     return initialStates;
 }
 
+// Thin wrapper for getting transition matrix
 storm::storage::SparseMatrix<double> getTransitionMatrix(storm::models::sparse::Model<double> const& model) {
     return model.getTransitionMatrix();
 }

stormpy/tests/core/test_bisimulation.py

@@ -9,7 +9,7 @@ class TestBisimulation:
         prop = "P=? [F \"observe0Greater1\"]"
         formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_model_from_prism_program(program, formulas)
-        model = pair.model
+        model = pair.model()
         assert model.nr_states() == 7403
         assert model.nr_transitions() == 13041
         assert model.model_type() == stormpy.ModelType.DTMC
@@ -28,7 +28,7 @@ class TestBisimulation:
         prop = "P=? [F \"observe0Greater1\"]"
         formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
-        model = pair.model
+        model = pair.model()
         assert model.nr_states() == 1367
         assert model.nr_transitions() == 2027
         assert model.model_type() == stormpy.ModelType.DTMC

stormpy/tests/core/test_modelchecking.py

@@ -18,18 +18,18 @@ class TestModelChecking:
         prop = "P=? [F \"target\"]"
         formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
-        model = pair.model
+        model = pair.model()
         assert model.nr_states() == 613
         assert model.nr_transitions() == 803
         assert model.model_type() == stormpy.ModelType.DTMC
         assert model.has_parameters()
         result = stormpy.model_checking(model, formulas[0])
-        func = result.result_function
+        func = result.result_function()
         one = pycarl.FactorizedPolynomial(pycarl.Rational(1))
         assert func.denominator == one
-        constraints_well_formed = result.constraints_well_formed
+        constraints_well_formed = result.constraints_well_formed()
         for constraint in constraints_well_formed:
             assert constraint.rel() == pycarl.formula.Relation.GEQ or constraint.rel() == pycarl.formula.Relation.LEQ
-        constraints_graph_preserving = result.constraints_graph_preserving
+        constraints_graph_preserving = result.constraints_graph_preserving()
         for constraint in constraints_graph_preserving:
             assert constraint.rel() == pycarl.formula.Relation.GREATER

stormpy/tests/logic/test_formulas.py

@@ -1,5 +1,5 @@
 import stormpy
-from stormpy.logic import logic
+import stormpy.logic
 
 class TestFormulas:
 
@@ -7,7 +7,7 @@ class TestFormulas:
         prop = "P=? [F \"one\"]"
         formulas = stormpy.parse_formulas(prop)
         formula = formulas[0]
-        assert type(formula) == logic.ProbabilityOperator
+        assert type(formula) == stormpy.logic.ProbabilityOperator
         assert len(formulas) == 1
         assert str(formula) == prop
 
@@ -15,7 +15,7 @@ class TestFormulas:
         prop = "R=? [F \"one\"]"
         formulas = stormpy.parse_formulas(prop)
         formula = formulas[0]
-        assert type(formula) == logic.RewardOperator
+        assert type(formula) == stormpy.logic.RewardOperator
         assert len(formulas) == 1
         assert str(formula) == "R[exp]=? [F \"one\"]"
 
@@ -38,13 +38,13 @@ class TestFormulas:
         formula = stormpy.parse_formulas(prop)[0]
         assert formula.has_bound()
         assert formula.threshold == 0.4
-        assert formula.comparison_type == logic.ComparisonType.LESS
+        assert formula.comparison_type == stormpy.logic.ComparisonType.LESS
 
     def test_set_bounds(self):
         prop = "P<0.4 [F \"one\"]"
         formula = stormpy.parse_formulas(prop)[0]
         formula.threshold = 0.2
-        formula.comparison_type = logic.ComparisonType.GEQ
+        formula.comparison_type = stormpy.logic.ComparisonType.GEQ
         assert formula.threshold == 0.2
-        assert formula.comparison_type == logic.ComparisonType.GEQ
+        assert formula.comparison_type == stormpy.logic.ComparisonType.GEQ
         assert str(formula) == "P>=0.2 [F \"one\"]"

stormpy/tests/storage/test_matrix.py

@@ -9,18 +9,18 @@ class TestMatrix:
         assert matrix.nr_columns() == model.nr_states()
         assert matrix.nr_entries() == 27 #model.nr_transitions()
         for e in matrix:
-            assert e.val == 0.5 or e.val == 0 or (e.val == 1 and e.column > 6)
+            assert e.val() == 0.5 or e.val() == 0 or (e.val() == 1 and e.column() > 6)
     
     def test_change_sparse_matrix(self):
         model = stormpy.parse_explicit_model("../examples/dtmc/die/die.tra", "../examples/dtmc/die/die.lab")
         matrix = model.transition_matrix()
         for e in matrix:
-            assert e.val == 0.5 or e.val == 0 or e.val == 1
+            assert e.val() == 0.5 or e.val() == 0 or e.val() == 1
         i = 0
         for e in matrix:
-            e.val = i
+            e.set_val(i)
             i += 0.1
         i = 0
         for e in matrix:
-            assert e.val == i
+            assert e.val() == i
             i += 0.1

stormpy/tests/storage/test_model.py

@@ -7,7 +7,7 @@ class TestModel:
         prop = "P=? [F \"one\"]"
         formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_model_from_prism_program(program, formulas)
-        model = pair.model
+        model = pair.model()
         assert model.nr_states() == 13
         assert model.nr_transitions() == 20
         assert model.model_type() == stormpy.ModelType.DTMC
@@ -22,7 +22,7 @@ class TestModel:
         prop = "P=? [F \"target\"]"
         formulas = stormpy.parse_formulas_for_prism_program(prop, program)
         pair = stormpy.build_parametric_model_from_prism_program(program, formulas)
-        model = pair.model
+        model = pair.model()
         assert model.nr_states() == 613
         assert model.nr_transitions() == 803
         assert model.model_type() == stormpy.ModelType.DTMC