diff --git a/stormpy/setup.py b/stormpy/setup.py
index 66d49a81d..a15acca1a 100755
--- a/stormpy/setup.py
+++ b/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,
diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp
index f650151c0..efbf508de 100644
--- a/stormpy/src/core/core.cpp
+++ b/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_readwrite("formulas", &storm::storage::ModelFormulasPair::formulas, "The formulas")
+ .def("model", [](storm::storage::ModelFormulasPair const& pair) {
+ 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"));
diff --git a/stormpy/src/core/modelchecking.cpp b/stormpy/src/core/modelchecking.cpp
index 3e9b7756b..dc1a7d08f 100644
--- a/stormpy/src/core/modelchecking.cpp
+++ b/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_readonly("constraints_well_formed", &PmcResult::constraintsWellFormed, "Constraints ensuring well-formed probabilities")
- .def_readonly("constraints_graph_preserving", &PmcResult::constraintsGraphPreserving, "Constraints ensuring graph preservation")
+ .def("result_function", &PmcResult::getResultFunction, "Result as rational function")
+ .def("constraints_well_formed", &PmcResult::getConstraintsWellFormed, "Constraints ensuring well-formed probabilities")
+ .def("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation")
;
}
diff --git a/stormpy/src/mod_storage.cpp b/stormpy/src/mod_storage.cpp
index 835f1e7b2..436caa96d 100644
--- a/stormpy/src/mod_storage.cpp
+++ b/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();
diff --git a/stormpy/src/storage/matrix.cpp b/stormpy/src/storage/matrix.cpp
index 1424ff792..6db2de7c3 100644
--- a/stormpy/src/storage/matrix.cpp
+++ b/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_readonly("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
+ //def_property threw "pointer being freed not allocated" after exiting
+ .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 */)
diff --git a/stormpy/src/storage/model.cpp b/stormpy/src/storage/model.cpp
index 6445973b2..64c247805 100644
--- a/stormpy/src/storage/model.cpp
+++ b/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();
}
diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py
index 5b46533f3..072f6cd07 100644
--- a/stormpy/tests/core/test_bisimulation.py
+++ b/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
diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py
index a275bc382..2a8e54b84 100644
--- a/stormpy/tests/core/test_modelchecking.py
+++ b/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
diff --git a/stormpy/tests/logic/test_formulas.py b/stormpy/tests/logic/test_formulas.py
index 7600f5a6f..57b27b626 100644
--- a/stormpy/tests/logic/test_formulas.py
+++ b/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\"]"
diff --git a/stormpy/tests/storage/test_matrix.py b/stormpy/tests/storage/test_matrix.py
index becf477a4..cde736f03 100644
--- a/stormpy/tests/storage/test_matrix.py
+++ b/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
diff --git a/stormpy/tests/storage/test_model.py b/stormpy/tests/storage/test_model.py
index 1e54378cb..94abdad61 100644
--- a/stormpy/tests/storage/test_model.py
+++ b/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