Made python bindings more pythony

Former-commit-id: 41d9f4d7fd

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)

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)

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)

stormpy/src/core/core.cpp

@@ -16,10 +16,10 @@ void define_parse(py::module& m) {
 
     // Pair <Model,Formulas>
     py::class_<storm::storage::ModelFormulasPair>(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<storm::models::ModelBase> buildModel(storm::prism::Program const
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::ModelBase> buildSparseModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula const> const& formula,
-    bool onlyInitialStatesRelevant = false) {
+std::shared_ptr<storm::models::ModelBase> buildSparseModel(storm::prism::Program const& program, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant = false) {
     return storm::buildSparseModel<ValueType>(program, std::vector<std::shared_ptr<storm::logic::Formula const>>(1,formula), onlyInitialStatesRelevant);
 }
 

stormpy/src/core/modelchecking.cpp

@@ -68,9 +68,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("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")
     ;
 
 }

stormpy/src/core/prism.cpp

@@ -18,9 +18,9 @@ void define_prism(py::module& m) {
     
     // PrismProgram
     py::class_<storm::prism::Program>(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")
     ;
     
 }

stormpy/src/logic/formulae.cpp

@@ -46,7 +46,7 @@ void define_formulae(py::module& m) {
     py::class_<storm::logic::UnaryStateFormula, std::shared_ptr<storm::logic::UnaryStateFormula const>>(m, "UnaryStateFormula", "State formula with one operand", py::base<storm::logic::StateFormula>());
     py::class_<storm::logic::UnaryBooleanStateFormula, std::shared_ptr<storm::logic::UnaryBooleanStateFormula const>>(m, "UnaryBooleanStateFormula", "Unary boolean state formula", py::base<storm::logic::UnaryStateFormula>());
     py::class_<storm::logic::OperatorFormula, std::shared_ptr<storm::logic::OperatorFormula const>>(m, "OperatorFormula", "Operator formula", py::base<storm::logic::UnaryStateFormula>())
-        .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")
     ;

stormpy/src/mod_info.cpp

@@ -6,9 +6,9 @@
 PYBIND11_PLUGIN(info) {
 	py::module m("info", "Storm information");
     py::class_<storm::utility::StormVersion>(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();
 }

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<entry_index, double>::getValue, "Value")
         .def("set_value", &storm::storage::MatrixEntry<entry_index, double>::setValue, py::arg("value"), "Set value")
-        .def("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
+        .def_property_readonly("column", &storm::storage::MatrixEntry<entry_index, double>::getColumn, "Column")
     ;
  
     py::class_<storm::storage::MatrixEntry<parametric_entry_index, storm::RationalFunction>>(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<parametric_entry_index, storm::RationalFunction>::getValue, "Value")
         .def("set_value", &storm::storage::MatrixEntry<parametric_entry_index, storm::RationalFunction>::setValue, py::arg("value"), "Set value")
-        .def("column", &storm::storage::MatrixEntry<parametric_entry_index, storm::RationalFunction>::getColumn, "Column")
+        .def_property_readonly("column", &storm::storage::MatrixEntry<parametric_entry_index, storm::RationalFunction>::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<double>::getRowCount, "Number of rows")
-        .def("nr_columns", &storm::storage::SparseMatrix<double>::getColumnCount, "Number of columns")
-        .def("nr_entries", &storm::storage::SparseMatrix<double>::getEntryCount, "Number of non-zero entries")
-        .def("_row_group_indices", &storm::storage::SparseMatrix<double>::getRowGroupIndices, "Get starting rows of row groups")
+        .def_property_readonly("nr_rows", &storm::storage::SparseMatrix<double>::getRowCount, "Number of rows")
+        .def_property_readonly("nr_columns", &storm::storage::SparseMatrix<double>::getColumnCount, "Number of columns")
+        .def_property_readonly("nr_entries", &storm::storage::SparseMatrix<double>::getEntryCount, "Number of non-zero entries")
+        .def_property_readonly("_row_group_indices", &storm::storage::SparseMatrix<double>::getRowGroupIndices, "Starting rows of row groups")
         .def("get_row", [](storm::storage::SparseMatrix<double>& 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<double>& 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<storm::RationalFunction>::getRowCount, "Number of rows")
-        .def("nr_columns", &storm::storage::SparseMatrix<storm::RationalFunction>::getColumnCount, "Number of columns")
-        .def("nr_entries", &storm::storage::SparseMatrix<storm::RationalFunction>::getEntryCount, "Number of non-zero entries")
-        .def("_row_group_indices", &storm::storage::SparseMatrix<storm::RationalFunction>::getRowGroupIndices, "Get starting rows of row groups")
+        .def_property_readonly("nr_rows", &storm::storage::SparseMatrix<storm::RationalFunction>::getRowCount, "Number of rows")
+        .def_property_readonly("nr_columns", &storm::storage::SparseMatrix<storm::RationalFunction>::getColumnCount, "Number of columns")
+        .def_property_readonly("nr_entries", &storm::storage::SparseMatrix<storm::RationalFunction>::getEntryCount, "Number of non-zero entries")
+        .def_property_readonly("_row_group_indices", &storm::storage::SparseMatrix<storm::RationalFunction>::getRowGroupIndices, "Starting rows of row groups")
         .def("get_row", [](storm::storage::SparseMatrix<storm::RationalFunction>& 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<storm::RationalFunction>& 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")

stormpy/src/storage/model.cpp

@@ -35,12 +35,12 @@ void define_model(py::module& m) {
 
     // ModelBase
     py::class_<storm::models::ModelBase, std::shared_ptr<storm::models::ModelBase>>(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<storm::models::sparse::Dtmc<double>>, "Get model as DTMC")
         .def("as_pdtmc", &storm::models::ModelBase::as<storm::models::sparse::Dtmc<storm::RationalFunction>>, "Get model as pDTMC")
         .def("as_mdp", &storm::models::ModelBase::as<storm::models::sparse::Mdp<double>>, "Get model as MDP")
@@ -49,12 +49,12 @@ void define_model(py::module& m) {
 
     // Models
     py::class_<storm::models::sparse::Model<double>, std::shared_ptr<storm::models::sparse::Model<double>>>(m, "SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix", py::base<storm::models::ModelBase>())
-        .def("labels", [](storm::models::sparse::Model<double>& model) {
+        .def_property_readonly("labels", [](storm::models::sparse::Model<double>& model) {
                 return model.getStateLabeling().getLabels();
-            }, "Get labels")
-        .def("labels_state", &storm::models::sparse::Model<double>::getLabelsOfState, "Get labels")
-        .def("initial_states", &getInitialStates<double>, "Get initial states")
-        .def("transition_matrix", &getTransitionMatrix<double>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix")
+            }, "Labels")
+        .def("labels_state", &storm::models::sparse::Model<double>::getLabelsOfState, py::arg("state"), "Get labels of state")
+        .def_property_readonly("initial_states", &getInitialStates<double>, "Initial states")
+        .def_property_readonly("transition_matrix", &getTransitionMatrix<double>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix")
     ;    
     py::class_<storm::models::sparse::Dtmc<double>, std::shared_ptr<storm::models::sparse::Dtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", py::base<storm::models::sparse::Model<double>>())
     ;
@@ -63,12 +63,12 @@ void define_model(py::module& m) {
 
     py::class_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>>(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", py::base<storm::models::ModelBase>())
         .def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters")
-        .def("labels", [](storm::models::sparse::Model<storm::RationalFunction>& model) {
+        .def_property_readonly("labels", [](storm::models::sparse::Model<storm::RationalFunction>& model) {
                 return model.getStateLabeling().getLabels();
-            }, "Get labels")
-        .def("labels_state", &storm::models::sparse::Model<storm::RationalFunction>::getLabelsOfState, "Get labels")
-        .def("initial_states", &getInitialStates<storm::RationalFunction>, "Get initial states")
-        .def("transition_matrix", &getTransitionMatrix<storm::RationalFunction>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Get transition matrix")
+            }, "Labels")
+        .def("labels_state", &storm::models::sparse::Model<storm::RationalFunction>::getLabelsOfState, py::arg("state"), "Get labels of state")
+        .def_property_readonly("initial_states", &getInitialStates<storm::RationalFunction>, "Initial states")
+        .def_property_readonly("transition_matrix", &getTransitionMatrix<storm::RationalFunction>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix")
     ;
     py::class_<storm::models::sparse::Dtmc<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", py::base<storm::models::sparse::Model<storm::RationalFunction>>())
     ;

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

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

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

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

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
 

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

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

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]