From 12e84178bcf032ec21e0c345f389ef9768056749 Mon Sep 17 00:00:00 2001 From: Mavo Date: Tue, 15 Nov 2016 16:54:23 +0100 Subject: [PATCH] Made python bindings more pythony Former-commit-id: 41d9f4d7fd24cf51eba0e0fc9495ace99a8421bd --- stormpy/lib/stormpy/__init__.py | 16 ++--- stormpy/lib/stormpy/storage/action.py | 2 +- stormpy/lib/stormpy/storage/state.py | 4 +- stormpy/src/core/core.cpp | 7 +-- stormpy/src/core/modelchecking.cpp | 6 +- stormpy/src/core/prism.cpp | 6 +- stormpy/src/logic/formulae.cpp | 2 +- stormpy/src/mod_info.cpp | 6 +- stormpy/src/storage/matrix.cpp | 24 ++++---- stormpy/src/storage/model.cpp | 32 +++++----- stormpy/tests/core/test_bisimulation.py | 42 ++++++------- stormpy/tests/core/test_modelchecking.py | 22 +++---- stormpy/tests/core/test_parse.py | 22 +++---- stormpy/tests/info/test_info.py | 6 +- stormpy/tests/logic/test_formulas.py | 4 +- stormpy/tests/storage/test_matrix.py | 20 +++---- stormpy/tests/storage/test_model.py | 60 +++++++++---------- stormpy/tests/storage/test_model_iterators.py | 10 ++-- 18 files changed, 145 insertions(+), 146 deletions(-) diff --git a/stormpy/lib/stormpy/__init__.py b/stormpy/lib/stormpy/__init__.py index 0ecddd76e..3dee81dd7 100644 --- a/stormpy/lib/stormpy/__init__.py +++ b/stormpy/lib/stormpy/__init__.py @@ -39,32 +39,32 @@ core.set_up("") def build_model(program, formulae): intermediate = core._build_model(program, formulae) - assert not intermediate.supports_parameters() - if intermediate.model_type() == ModelType.DTMC: + assert not intermediate.supports_parameters + if intermediate.model_type == ModelType.DTMC: return intermediate.as_dtmc() - elif intermediate.model_type() == ModelType.MDP: + elif intermediate.model_type == ModelType.MDP: return intermediate.as_mdp() else: raise RuntimeError("Not supported non-parametric model constructed") def build_parametric_model(program, formulae): intermediate = core._build_parametric_model(program, formulae) - assert intermediate.supports_parameters() - if intermediate.model_type() == ModelType.DTMC: + assert intermediate.supports_parameters + if intermediate.model_type == ModelType.DTMC: return intermediate.as_pdtmc() - elif intermediate.model_type() == ModelType.MDP: + elif intermediate.model_type == ModelType.MDP: return intermediate.as_pmdp() else: raise RuntimeError("Not supported parametric model constructed") def perform_bisimulation(model, formula, bisimulation_type): - if model.supports_parameters(): + if model.supports_parameters: return core._perform_parametric_bisimulation(model, formula, bisimulation_type) else: return core._perform_bisimulation(model, formula, bisimulation_type) def model_checking(model, formula): - if model.supports_parameters(): + if model.supports_parameters: return core._parametric_model_checking(model, formula) else: return core._model_checking(model, formula) diff --git a/stormpy/lib/stormpy/storage/action.py b/stormpy/lib/stormpy/storage/action.py index cc476d9b8..420f5b3ba 100644 --- a/stormpy/lib/stormpy/storage/action.py +++ b/stormpy/lib/stormpy/storage/action.py @@ -33,4 +33,4 @@ class Action: """ row = self.row_group_start + self.row #return self.model.transition_matrix().get_row(self.row_group_start + self.row) - return self.model.transition_matrix().row_iter(row, row) + return self.model.transition_matrix.row_iter(row, row) diff --git a/stormpy/lib/stormpy/storage/state.py b/stormpy/lib/stormpy/storage/state.py index f443ac095..6a315e76d 100644 --- a/stormpy/lib/stormpy/storage/state.py +++ b/stormpy/lib/stormpy/storage/state.py @@ -15,7 +15,7 @@ class State: return self def __next__(self): - if self.id >= self.model.nr_states() - 1: + if self.id >= self.model.nr_states - 1: raise StopIteration else: self.id += 1 @@ -28,7 +28,7 @@ class State: """ Get actions associated with the state :return List of actions """ - row_group_indices = self.model.transition_matrix()._row_group_indices() + row_group_indices = self.model.transition_matrix._row_group_indices start = row_group_indices[self.id] end = row_group_indices[self.id+1] return action.Action(start, end, 0, self.model) diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index a217cea2c..422ecb53d 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -16,10 +16,10 @@ void define_parse(py::module& m) { // Pair py::class_(m, "ModelFormulasPair", "Pair of model and formulas") - .def("model", [](storm::storage::ModelFormulasPair const& pair) { + .def_property_readonly("model", [](storm::storage::ModelFormulasPair const& pair) { return pair.model; }, "The model") - .def("formulas", [](storm::storage::ModelFormulasPair const& pair) { + .def_property_readonly("formulas", [](storm::storage::ModelFormulasPair const& pair) { return pair.formulas; }, "The formulas") ; @@ -35,8 +35,7 @@ std::shared_ptr buildModel(storm::prism::Program const } template -std::shared_ptr buildSparseModel(storm::prism::Program const& program, std::shared_ptr const& formula, - bool onlyInitialStatesRelevant = false) { +std::shared_ptr buildSparseModel(storm::prism::Program const& program, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { return storm::buildSparseModel(program, std::vector>(1,formula), onlyInitialStatesRelevant); } diff --git a/stormpy/src/core/modelchecking.cpp b/stormpy/src/core/modelchecking.cpp index c4c9cfbbc..dd00a281b 100644 --- a/stormpy/src/core/modelchecking.cpp +++ b/stormpy/src/core/modelchecking.cpp @@ -68,9 +68,9 @@ void define_modelchecking(py::module& m) { // PmcResult py::class_>(m, "PmcResult", "Holds the results after parametric model checking") .def("__str__", &PmcResult::toString) - .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") + .def_property_readonly("result_function", &PmcResult::getResultFunction, "Result as rational function") + .def_property_readonly("constraints_well_formed", &PmcResult::getConstraintsWellFormed, "Constraints ensuring well-formed probabilities") + .def_property_readonly("constraints_graph_preserving", &PmcResult::getConstraintsGraphPreserving, "Constraints ensuring graph preservation") ; } diff --git a/stormpy/src/core/prism.cpp b/stormpy/src/core/prism.cpp index 20fa654a6..9c88bc13d 100644 --- a/stormpy/src/core/prism.cpp +++ b/stormpy/src/core/prism.cpp @@ -18,9 +18,9 @@ void define_prism(py::module& m) { // PrismProgram py::class_(m, "PrismProgram", "Prism program") - .def("nr_modules", &storm::prism::Program::getNumberOfModules, "Get number of modules") - .def("model_type", &storm::prism::Program::getModelType, "Get model type") - .def("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Check if program has undefined constants") + .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules") + .def_property_readonly("model_type", &storm::prism::Program::getModelType, "Model type") + .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants") ; } diff --git a/stormpy/src/logic/formulae.cpp b/stormpy/src/logic/formulae.cpp index 09d6c1239..9d52c1918 100644 --- a/stormpy/src/logic/formulae.cpp +++ b/stormpy/src/logic/formulae.cpp @@ -46,7 +46,7 @@ void define_formulae(py::module& m) { py::class_>(m, "UnaryStateFormula", "State formula with one operand", py::base()); py::class_>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", py::base()); py::class_>(m, "OperatorFormula", "Operator formula", py::base()) - .def("has_bound", &storm::logic::OperatorFormula::hasBound, "Check if formula is bounded") + .def_property_readonly("has_bound", &storm::logic::OperatorFormula::hasBound, "Flag if formula is bounded") .def_property("threshold", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold of bound") .def_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType, "Comparison type of bound") ; diff --git a/stormpy/src/mod_info.cpp b/stormpy/src/mod_info.cpp index dd41617f3..c4d199842 100644 --- a/stormpy/src/mod_info.cpp +++ b/stormpy/src/mod_info.cpp @@ -6,9 +6,9 @@ PYBIND11_PLUGIN(info) { py::module m("info", "Storm information"); py::class_(m, "Version", "Version information for Storm") - .def("short", &storm::utility::StormVersion::shortVersionString, "Storm version in short representation") - .def("long", &storm::utility::StormVersion::longVersionString, "Storm version in long representation") - .def("build_info", &storm::utility::StormVersion::buildInfo, "Build info for Storm") + .def_property_readonly("short", &storm::utility::StormVersion::shortVersionString, "Storm version in short representation") + .def_property_readonly("long", &storm::utility::StormVersion::longVersionString, "Storm version in long representation") + .def_property_readonly("build_info", &storm::utility::StormVersion::buildInfo, "Build info for Storm") ; return m.ptr(); } diff --git a/stormpy/src/storage/matrix.cpp b/stormpy/src/storage/matrix.cpp index 1d79b4ef7..d2bc91a1d 100644 --- a/stormpy/src/storage/matrix.cpp +++ b/stormpy/src/storage/matrix.cpp @@ -19,7 +19,7 @@ void define_sparse_matrix(py::module& m) { //def_property threw "pointer being freed not allocated" after exiting .def("value", &storm::storage::MatrixEntry::getValue, "Value") .def("set_value", &storm::storage::MatrixEntry::setValue, py::arg("value"), "Set value") - .def("column", &storm::storage::MatrixEntry::getColumn, "Column") + .def_property_readonly("column", &storm::storage::MatrixEntry::getColumn, "Column") ; py::class_>(m, "ParametricSparseMatrixEntry", "Entry of parametric sparse matrix") @@ -31,7 +31,7 @@ void define_sparse_matrix(py::module& m) { //def_property threw "pointer being freed not allocated" after exiting .def("value", &storm::storage::MatrixEntry::getValue, "Value") .def("set_value", &storm::storage::MatrixEntry::setValue, py::arg("value"), "Set value") - .def("column", &storm::storage::MatrixEntry::getColumn, "Column") + .def_property_readonly("column", &storm::storage::MatrixEntry::getColumn, "Column") ; // SparseMatrix @@ -44,10 +44,10 @@ void define_sparse_matrix(py::module& m) { stream << matrix; return stream.str(); }) - .def("nr_rows", &storm::storage::SparseMatrix::getRowCount, "Number of rows") - .def("nr_columns", &storm::storage::SparseMatrix::getColumnCount, "Number of columns") - .def("nr_entries", &storm::storage::SparseMatrix::getEntryCount, "Number of non-zero entries") - .def("_row_group_indices", &storm::storage::SparseMatrix::getRowGroupIndices, "Get starting rows of row groups") + .def_property_readonly("nr_rows", &storm::storage::SparseMatrix::getRowCount, "Number of rows") + .def_property_readonly("nr_columns", &storm::storage::SparseMatrix::getColumnCount, "Number of columns") + .def_property_readonly("nr_entries", &storm::storage::SparseMatrix::getEntryCount, "Number of non-zero entries") + .def_property_readonly("_row_group_indices", &storm::storage::SparseMatrix::getRowGroupIndices, "Starting rows of row groups") .def("get_row", [](storm::storage::SparseMatrix& matrix, entry_index row) { return matrix.getRows(row, row+1); }, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row") @@ -62,7 +62,7 @@ void define_sparse_matrix(py::module& m) { } return stream.str(); }, py::arg("row"), "Print row") - // Entry_index lead to problems + // Entry_index lead to problems .def("row_iter", [](storm::storage::SparseMatrix& matrix, row_index start, row_index end) { return py::make_iterator(matrix.begin(start), matrix.end(end)); }, py::keep_alive<0, 1>() /* keep object alive while iterator exists */, py::arg("row_start"), py::arg("row_end"), "Get iterator from start to end") @@ -77,10 +77,10 @@ void define_sparse_matrix(py::module& m) { stream << matrix; return stream.str(); }) - .def("nr_rows", &storm::storage::SparseMatrix::getRowCount, "Number of rows") - .def("nr_columns", &storm::storage::SparseMatrix::getColumnCount, "Number of columns") - .def("nr_entries", &storm::storage::SparseMatrix::getEntryCount, "Number of non-zero entries") - .def("_row_group_indices", &storm::storage::SparseMatrix::getRowGroupIndices, "Get starting rows of row groups") + .def_property_readonly("nr_rows", &storm::storage::SparseMatrix::getRowCount, "Number of rows") + .def_property_readonly("nr_columns", &storm::storage::SparseMatrix::getColumnCount, "Number of columns") + .def_property_readonly("nr_entries", &storm::storage::SparseMatrix::getEntryCount, "Number of non-zero entries") + .def_property_readonly("_row_group_indices", &storm::storage::SparseMatrix::getRowGroupIndices, "Starting rows of row groups") .def("get_row", [](storm::storage::SparseMatrix& matrix, parametric_entry_index row) { return matrix.getRows(row, row+1); }, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row") @@ -95,7 +95,7 @@ void define_sparse_matrix(py::module& m) { } return stream.str(); }, py::arg("row"), "Print row") - // Entry_index lead to problems + // Entry_index lead to problems .def("row_iter", [](storm::storage::SparseMatrix& matrix, parametric_row_index start, parametric_row_index end) { return py::make_iterator(matrix.begin(start), matrix.end(end)); }, py::keep_alive<0, 1>() /* keep object alive while iterator exists */, py::arg("row_start"), py::arg("row_end"), "Get iterator from start to end") diff --git a/stormpy/src/storage/model.cpp b/stormpy/src/storage/model.cpp index 0f29cac93..98f485766 100644 --- a/stormpy/src/storage/model.cpp +++ b/stormpy/src/storage/model.cpp @@ -35,12 +35,12 @@ void define_model(py::module& m) { // ModelBase py::class_>(m, "ModelBase", "Base class for all models") - .def("nr_states", &storm::models::ModelBase::getNumberOfStates, "Get number of states") - .def("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions, "Get number of transitions") - .def("model_type", &storm::models::ModelBase::getType, "Get model type") - .def("supports_parameters", &storm::models::ModelBase::supportsParameters, "Check if model supports parameters") - .def("has_parameters", &storm::models::ModelBase::hasParameters, "Check if model has parameters") - .def("is_exact", &storm::models::ModelBase::isExact, "Check if model is exact") + .def_property_readonly("nr_states", &storm::models::ModelBase::getNumberOfStates, "Number of states") + .def_property_readonly("nr_transitions", &storm::models::ModelBase::getNumberOfTransitions, "Number of transitions") + .def_property_readonly("model_type", &storm::models::ModelBase::getType, "Model type") + .def_property_readonly("supports_parameters", &storm::models::ModelBase::supportsParameters, "Flag whether model supports parameters") + .def_property_readonly("has_parameters", &storm::models::ModelBase::hasParameters, "Flag whether model has parameters") + .def_property_readonly("is_exact", &storm::models::ModelBase::isExact, "Flag whether model is exact") .def("as_dtmc", &storm::models::ModelBase::as>, "Get model as DTMC") .def("as_pdtmc", &storm::models::ModelBase::as>, "Get model as pDTMC") .def("as_mdp", &storm::models::ModelBase::as>, "Get model as MDP") @@ -49,12 +49,12 @@ void define_model(py::module& m) { // Models py::class_, std::shared_ptr>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base()) - .def("labels", [](storm::models::sparse::Model& model) { + .def_property_readonly("labels", [](storm::models::sparse::Model& model) { return model.getStateLabeling().getLabels(); - }, "Get labels") - .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, "Get labels") - .def("initial_states", &getInitialStates, "Get initial states") - .def("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix") + }, "Labels") + .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") + .def_property_readonly("initial_states", &getInitialStates, "Initial states") + .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") ; py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", py::base>()) ; @@ -63,12 +63,12 @@ void define_model(py::module& m) { py::class_, std::shared_ptr>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base()) .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters") - .def("labels", [](storm::models::sparse::Model& model) { + .def_property_readonly("labels", [](storm::models::sparse::Model& model) { return model.getStateLabeling().getLabels(); - }, "Get labels") - .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, "Get labels") - .def("initial_states", &getInitialStates, "Get initial states") - .def("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix") + }, "Labels") + .def("labels_state", &storm::models::sparse::Model::getLabelsOfState, py::arg("state"), "Get labels of state") + .def_property_readonly("initial_states", &getInitialStates, "Initial states") + .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") ; py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base>()) ; diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py index 0edb49ffc..017436584 100644 --- a/stormpy/tests/core/test_bisimulation.py +++ b/stormpy/tests/core/test_bisimulation.py @@ -5,35 +5,35 @@ from helpers.helper import get_example_path class TestBisimulation: def test_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds", "crowds5_5.pm")) - assert program.nr_modules() == 1 - assert program.model_type() == stormpy.PrismModelType.DTMC + assert program.nr_modules == 1 + assert program.model_type == stormpy.PrismModelType.DTMC prop = "P=? [F \"observe0Greater1\"]" formulas = stormpy.parse_formulas_for_prism_program(prop, program) model = stormpy.build_model_from_prism_program(program, formulas) - assert model.nr_states() == 7403 - assert model.nr_transitions() == 13041 - assert model.model_type() == stormpy.ModelType.DTMC - assert not model.supports_parameters() + assert model.nr_states == 7403 + assert model.nr_transitions == 13041 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) - assert model_bisim.nr_states() == 64 - assert model_bisim.nr_transitions() == 104 - assert model_bisim.model_type() == stormpy.ModelType.DTMC - assert not model_bisim.supports_parameters() + assert model_bisim.nr_states == 64 + assert model_bisim.nr_transitions == 104 + assert model_bisim.model_type == stormpy.ModelType.DTMC + assert not model_bisim.supports_parameters def test_parametric_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "crowds", "crowds3_5.pm")) - assert program.nr_modules() == 1 - assert program.model_type() == stormpy.PrismModelType.DTMC - assert program.has_undefined_constants() + assert program.nr_modules == 1 + assert program.model_type == stormpy.PrismModelType.DTMC + assert program.has_undefined_constants prop = "P=? [F \"observe0Greater1\"]" formulas = stormpy.parse_formulas_for_prism_program(prop, program) model = stormpy.build_parametric_model_from_prism_program(program, formulas) - assert model.nr_states() == 1367 - assert model.nr_transitions() == 2027 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.has_parameters() + assert model.nr_states == 1367 + assert model.nr_transitions == 2027 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters model_bisim = stormpy.perform_bisimulation(model, formulas[0], stormpy.BisimulationType.STRONG) - assert model_bisim.nr_states() == 80 - assert model_bisim.nr_transitions() == 120 - assert model_bisim.model_type() == stormpy.ModelType.DTMC - assert model_bisim.has_parameters() + assert model_bisim.nr_states == 80 + assert model_bisim.nr_transitions == 120 + assert model_bisim.model_type == stormpy.ModelType.DTMC + assert model_bisim.has_parameters diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py index 0b692df69..503788a26 100644 --- a/stormpy/tests/core/test_modelchecking.py +++ b/stormpy/tests/core/test_modelchecking.py @@ -7,8 +7,8 @@ class TestModelChecking: program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas[0]) - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 + assert model.nr_states == 13 + assert model.nr_transitions == 20 result = stormpy.model_checking(model, formulas[0]) assert result == 0.16666666666666663 @@ -16,8 +16,8 @@ class TestModelChecking: program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas[0]) - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 + assert model.nr_states == 13 + assert model.nr_transitions == 20 results = stormpy.model_checking_all(model, formulas[0]) results_orig = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] assert results == results_orig @@ -29,17 +29,17 @@ class TestModelChecking: prop = "P=? [F s=5]" formulas = stormpy.parse_formulas_for_prism_program(prop, program) model = stormpy.build_parametric_model_from_prism_program(program, formulas) - assert model.nr_states() == 613 - assert model.nr_transitions() == 803 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.has_parameters() + 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/core/test_parse.py b/stormpy/tests/core/test_parse.py index a8f41f4e1..e9a18a0b9 100644 --- a/stormpy/tests/core/test_parse.py +++ b/stormpy/tests/core/test_parse.py @@ -5,9 +5,9 @@ from helpers.helper import get_example_path class TestParse: def test_parse_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) - assert program.nr_modules() == 1 - assert program.model_type() == stormpy.PrismModelType.DTMC - assert not program.has_undefined_constants() + assert program.nr_modules == 1 + assert program.model_type == stormpy.PrismModelType.DTMC + assert not program.has_undefined_constants def test_parse_formula(self): prop = "P=? [F \"one\"]" @@ -17,16 +17,16 @@ class TestParse: def test_parse_explicit_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab")) - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 - assert model.model_type() == stormpy.ModelType.DTMC - assert not model.supports_parameters() + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc def test_parse_explicit_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab")) - assert model.nr_states() == 169 - assert model.nr_transitions() == 436 - assert model.model_type() == stormpy.ModelType.MDP - assert not model.supports_parameters() + assert model.nr_states == 169 + assert model.nr_transitions == 436 + assert model.model_type == stormpy.ModelType.MDP + assert not model.supports_parameters assert type(model) is stormpy.SparseMdp diff --git a/stormpy/tests/info/test_info.py b/stormpy/tests/info/test_info.py index 133ae36d2..fd91d68d7 100644 --- a/stormpy/tests/info/test_info.py +++ b/stormpy/tests/info/test_info.py @@ -3,6 +3,6 @@ from stormpy.info import info class TestInfo: def test_version(self): - s = info.Version.short() - s = info.Version.long() - s = info.Version.build_info() + s = info.Version.short + s = info.Version.long + s = info.Version.build_info diff --git a/stormpy/tests/logic/test_formulas.py b/stormpy/tests/logic/test_formulas.py index 2ed5d756a..1bb697ce3 100644 --- a/stormpy/tests/logic/test_formulas.py +++ b/stormpy/tests/logic/test_formulas.py @@ -34,10 +34,10 @@ class TestFormulas: def test_bounds(self): prop = "P=? [F \"one\"]" formula = stormpy.parse_formulas(prop)[0] - assert not formula.has_bound() + assert not formula.has_bound prop = "P<0.4 [F \"one\"]" formula = stormpy.parse_formulas(prop)[0] - assert formula.has_bound() + assert formula.has_bound assert formula.threshold == pycarl.Rational("0.4") assert formula.comparison_type == stormpy.logic.ComparisonType.LESS diff --git a/stormpy/tests/storage/test_matrix.py b/stormpy/tests/storage/test_matrix.py index 8e8c98a47..0f13fbf9d 100644 --- a/stormpy/tests/storage/test_matrix.py +++ b/stormpy/tests/storage/test_matrix.py @@ -4,17 +4,17 @@ from helpers.helper import get_example_path class TestMatrix: def test_sparse_matrix(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab")) - matrix = model.transition_matrix() + matrix = model.transition_matrix assert type(matrix) is stormpy.storage.SparseMatrix - assert matrix.nr_rows() == model.nr_states() - assert matrix.nr_columns() == model.nr_states() - assert matrix.nr_entries() == 27 #model.nr_transitions() + assert matrix.nr_rows == model.nr_states + assert matrix.nr_columns == model.nr_states + assert matrix.nr_entries == 27 #model.nr_transitions for e in matrix: - assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column() > 6) + assert e.value() == 0.5 or e.value() == 0 or (e.value() == 1 and e.column > 6) def test_change_sparse_matrix(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab")) - matrix = model.transition_matrix() + matrix = model.transition_matrix for e in matrix: assert e.value() == 0.5 or e.value() == 0 or e.value() == 1 i = 0 @@ -29,7 +29,7 @@ class TestMatrix: def test_change_sparse_matrix_modelchecking(self): import stormpy.logic model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab")) - matrix = model.transition_matrix() + matrix = model.transition_matrix # Check matrix for e in matrix: assert e.value() == 0.5 or e.value() == 0 or e.value() == 1 @@ -71,7 +71,7 @@ class TestMatrix: program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) model = stormpy.build_parametric_model(program, formulas[0]) - matrix = model.transition_matrix() + matrix = model.transition_matrix # Check matrix one_pol = pycarl.Rational(1) one_pol = pycarl.FactorizedPolynomial(one_pol) @@ -80,7 +80,7 @@ class TestMatrix: assert e.value() == one or len(e.value().gather_variables()) > 0 # First model checking result = stormpy.model_checking(model, formulas[0]) - assert len(result.result_function().gather_variables()) > 0 + assert len(result.result_function.gather_variables()) > 0 # Change probabilities two_pol = pycarl.Rational(2) @@ -93,4 +93,4 @@ class TestMatrix: assert e.value() == new_val or e.value() == one # Second model checking result = stormpy.model_checking(model, formulas[0]) - assert len(result.result_function().gather_variables()) == 0 + assert len(result.result_function.gather_variables()) == 0 diff --git a/stormpy/tests/storage/test_model.py b/stormpy/tests/storage/test_model.py index 493e21e5e..823c0c506 100644 --- a/stormpy/tests/storage/test_model.py +++ b/stormpy/tests/storage/test_model.py @@ -8,64 +8,64 @@ class TestModel: prop = "P=? [F \"one\"]" formulas = stormpy.parse_formulas_for_prism_program(prop, program) model = stormpy.build_model_from_prism_program(program, formulas) - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 - assert model.model_type() == stormpy.ModelType.DTMC - assert not model.supports_parameters() + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc def test_build_parametric_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) - assert program.nr_modules() == 5 - assert program.model_type() == stormpy.PrismModelType.DTMC - assert program.has_undefined_constants() + assert program.nr_modules == 5 + assert program.model_type == stormpy.PrismModelType.DTMC + assert program.has_undefined_constants prop = "P=? [F s=5]" formulas = stormpy.parse_formulas_for_prism_program(prop, program) model = stormpy.build_parametric_model_from_prism_program(program, formulas) - assert model.nr_states() == 613 - assert model.nr_transitions() == 803 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.supports_parameters() - assert model.has_parameters() + assert model.nr_states == 613 + assert model.nr_transitions == 803 + assert model.model_type == stormpy.ModelType.DTMC + assert model.supports_parameters + assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc def test_build_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas[0]) - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 - assert model.model_type() == stormpy.ModelType.DTMC - assert not model.supports_parameters() + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc def test_build_parametric_dtmc(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) model = stormpy.build_parametric_model(program, formulas[0]) - assert model.nr_states() == 613 - assert model.nr_transitions() == 803 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.supports_parameters() - assert model.has_parameters() + assert model.nr_states == 613 + assert model.nr_transitions == 803 + assert model.model_type == stormpy.ModelType.DTMC + assert model.supports_parameters + assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc def test_build_dtmc_supporting_parameters(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_parametric_model(program, formulas[0]) - assert model.nr_states() == 13 - assert model.nr_transitions() == 20 - assert model.model_type() == stormpy.ModelType.DTMC - assert model.supports_parameters() - assert not model.has_parameters() + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert model.supports_parameters + assert not model.has_parameters assert type(model) is stormpy.SparseParametricDtmc def test_label(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas[0]) - labels = model.labels() + labels = model.labels assert len(labels) == 3 assert "init" in labels assert "one" in labels @@ -76,7 +76,7 @@ class TestModel: program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas[0]) - initial_states = model.initial_states() + initial_states = model.initial_states assert len(initial_states) == 1 assert 0 in initial_states @@ -84,13 +84,13 @@ class TestModel: program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp16_2.pm")) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) model = stormpy.build_parametric_model(program, formulas[0]) - labels = model.labels() + labels = model.labels assert len(labels) == 3 assert "init" in labels assert "(s = 5)" in labels assert "init" in model.labels_state(0) assert "(s = 5)" in model.labels_state(28) assert "(s = 5)" in model.labels_state(611) - initial_states = model.initial_states() + initial_states = model.initial_states assert len(initial_states) == 1 assert 0 in initial_states diff --git a/stormpy/tests/storage/test_model_iterators.py b/stormpy/tests/storage/test_model_iterators.py index 04a8fadc4..52a76736a 100644 --- a/stormpy/tests/storage/test_model_iterators.py +++ b/stormpy/tests/storage/test_model_iterators.py @@ -9,7 +9,7 @@ class TestModelIterators: for state in stormpy.state.State(0, model): assert state.id == i i += 1 - assert i == model.nr_states() + assert i == model.nr_states def test_states_mdp(self): model = stormpy.parse_explicit_model(get_example_path("mdp", "two_dice", "two_dice.tra"), get_example_path("mdp", "two_dice", "two_dice.lab")) @@ -18,7 +18,7 @@ class TestModelIterators: for state in stormpy.state.State(0, model): assert state.id == i i += 1 - assert i == model.nr_states() + assert i == model.nr_states def test_actions_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab")) @@ -50,7 +50,7 @@ class TestModelIterators: transition_orig = transitions_orig[i] i += 1 assert state.id == transition_orig[0] - assert transition.column() == transition_orig[1] + assert transition.column == transition_orig[1] assert transition.value() == transition_orig[2] def test_transitions_mdp(self): @@ -74,9 +74,9 @@ class TestModelIterators: model = stormpy.parse_explicit_model(get_example_path("dtmc", "die", "die.tra"), get_example_path("dtmc", "die", "die.lab")) i = 0 for state in stormpy.state.State(0, model): - for transition in model.transition_matrix().row_iter(state.id, state.id): + for transition in model.transition_matrix.row_iter(state.id, state.id): transition_orig = transitions_orig[i] i += 1 assert state.id == transition_orig[0] - assert transition.column() == transition_orig[1] + assert transition.column == transition_orig[1] assert transition.value() == transition_orig[2]