diff --git a/.gitignore b/.gitignore index ac83173b8..d4d4d6429 100644 --- a/.gitignore +++ b/.gitignore @@ -51,3 +51,5 @@ nbproject/ .DS_Store .idea *.out +# Python config +stormpy/setup.cfg diff --git a/stormpy/src/core/core.cpp b/stormpy/src/core/core.cpp index 50b77c3f4..a217cea2c 100644 --- a/stormpy/src/core/core.cpp +++ b/stormpy/src/core/core.cpp @@ -42,9 +42,9 @@ std::shared_ptr buildSparseModel(storm::prism::Program void define_build(py::module& m) { // Build model - m.def("_build_model", &buildModel, "Build the model", py::arg("program"), py::arg("formula")); + m.def("_build_model", &buildSparseModel, "Build the model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false); m.def("_build_parametric_model", &buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false); - m.def("build_model_from_prism_program", &storm::buildSymbolicModel, "Build the model", py::arg("program"), py::arg("formulas")); + m.def("build_model_from_prism_program", &storm::buildSparseModel, "Build the model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false); m.def("build_parametric_model_from_prism_program", &storm::buildSparseModel, "Build the parametric model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false); } diff --git a/stormpy/tests/core/test_bisimulation.py b/stormpy/tests/core/test_bisimulation.py index 7e845ffce..1a8fb8fe4 100644 --- a/stormpy/tests/core/test_bisimulation.py +++ b/stormpy/tests/core/test_bisimulation.py @@ -9,8 +9,7 @@ class TestBisimulation: assert program.model_type() == stormpy.PrismModelType.DTMC 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 = 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 @@ -28,8 +27,7 @@ class TestBisimulation: assert program.has_undefined_constants() 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 = 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 diff --git a/stormpy/tests/core/test_core.py b/stormpy/tests/core/test_core.py index 421df1808..cedd750eb 100644 --- a/stormpy/tests/core/test_core.py +++ b/stormpy/tests/core/test_core.py @@ -8,3 +8,7 @@ class TestCore: import pycarl import pycarl.formula import pycarl.parse + pol1 = pycarl.FactorizedPolynomial(32) + pol2 = pycarl.FactorizedPolynomial(2) + rat = pycarl.FactorizedRationalFunction(pol1, pol2) + assert str(rat) == "16" diff --git a/stormpy/tests/core/test_modelchecking.py b/stormpy/tests/core/test_modelchecking.py index ba0b5f74a..d6033b1c3 100644 --- a/stormpy/tests/core/test_modelchecking.py +++ b/stormpy/tests/core/test_modelchecking.py @@ -28,8 +28,7 @@ class TestModelChecking: program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm")) 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 = 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 diff --git a/stormpy/tests/storage/test_model.py b/stormpy/tests/storage/test_model.py index 7fc4894dc..df50c6f31 100644 --- a/stormpy/tests/storage/test_model.py +++ b/stormpy/tests/storage/test_model.py @@ -7,8 +7,7 @@ class TestModel: program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) 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 = 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 @@ -22,8 +21,7 @@ class TestModel: assert program.has_undefined_constants() 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 = 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 @@ -68,7 +66,7 @@ class TestModel: formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas[0]) labels = model.labels() - assert len(labels) == 2 + assert len(labels) == 3 assert "init" in labels assert "one" in labels assert "init" in model.labels_state(0) @@ -87,7 +85,7 @@ class TestModel: formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program) model = stormpy.build_parametric_model(program, formulas[0]) labels = model.labels() - assert len(labels) == 2 + assert len(labels) == 3 assert "init" in labels assert "target" in labels assert "init" in model.labels_state(0)