Browse Source

Tests running again

Former-commit-id: eee3ef32f5
tempestpy_adaptions
Mavo 8 years ago
committed by Matthias Volk
parent
commit
714f89542d
  1. 2
      .gitignore
  2. 4
      stormpy/src/core/core.cpp
  3. 6
      stormpy/tests/core/test_bisimulation.py
  4. 4
      stormpy/tests/core/test_core.py
  5. 3
      stormpy/tests/core/test_modelchecking.py
  6. 10
      stormpy/tests/storage/test_model.py

2
.gitignore

@ -51,3 +51,5 @@ nbproject/
.DS_Store .DS_Store
.idea .idea
*.out *.out
# Python config
stormpy/setup.cfg

4
stormpy/src/core/core.cpp

@ -42,9 +42,9 @@ std::shared_ptr<storm::models::ModelBase> buildSparseModel(storm::prism::Program
void define_build(py::module& m) { void define_build(py::module& m) {
// Build model // Build model
m.def("_build_model", &buildModel<double>, "Build the model", py::arg("program"), py::arg("formula"));
m.def("_build_model", &buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false);
m.def("_build_parametric_model", &buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false); m.def("_build_parametric_model", &buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formula"), py::arg("onlyInitialRelevant") = false);
m.def("build_model_from_prism_program", &storm::buildSymbolicModel<double>, "Build the model", py::arg("program"), py::arg("formulas"));
m.def("build_model_from_prism_program", &storm::buildSparseModel<double>, "Build the model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false);
m.def("build_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false); m.def("build_parametric_model_from_prism_program", &storm::buildSparseModel<storm::RationalFunction>, "Build the parametric model", py::arg("program"), py::arg("formulas"), py::arg("onlyInitialRelevant") = false);
} }

6
stormpy/tests/core/test_bisimulation.py

@ -9,8 +9,7 @@ class TestBisimulation:
assert program.model_type() == stormpy.PrismModelType.DTMC assert program.model_type() == stormpy.PrismModelType.DTMC
prop = "P=? [F \"observe0Greater1\"]" prop = "P=? [F \"observe0Greater1\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program) 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_states() == 7403
assert model.nr_transitions() == 13041 assert model.nr_transitions() == 13041
assert model.model_type() == stormpy.ModelType.DTMC assert model.model_type() == stormpy.ModelType.DTMC
@ -28,8 +27,7 @@ class TestBisimulation:
assert program.has_undefined_constants() assert program.has_undefined_constants()
prop = "P=? [F \"observe0Greater1\"]" prop = "P=? [F \"observe0Greater1\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program) 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_states() == 1367
assert model.nr_transitions() == 2027 assert model.nr_transitions() == 2027
assert model.model_type() == stormpy.ModelType.DTMC assert model.model_type() == stormpy.ModelType.DTMC

4
stormpy/tests/core/test_core.py

@ -8,3 +8,7 @@ class TestCore:
import pycarl import pycarl
import pycarl.formula import pycarl.formula
import pycarl.parse import pycarl.parse
pol1 = pycarl.FactorizedPolynomial(32)
pol2 = pycarl.FactorizedPolynomial(2)
rat = pycarl.FactorizedRationalFunction(pol1, pol2)
assert str(rat) == "16"

3
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")) program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp", "brp_16_2.pm"))
prop = "P=? [F \"target\"]" prop = "P=? [F \"target\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program) 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_states() == 613
assert model.nr_transitions() == 803 assert model.nr_transitions() == 803
assert model.model_type() == stormpy.ModelType.DTMC assert model.model_type() == stormpy.ModelType.DTMC

10
stormpy/tests/storage/test_model.py

@ -7,8 +7,7 @@ class TestModel:
program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm")) program = stormpy.parse_prism_program(get_example_path("dtmc", "die", "die.pm"))
prop = "P=? [F \"one\"]" prop = "P=? [F \"one\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program) 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_states() == 13
assert model.nr_transitions() == 20 assert model.nr_transitions() == 20
assert model.model_type() == stormpy.ModelType.DTMC assert model.model_type() == stormpy.ModelType.DTMC
@ -22,8 +21,7 @@ class TestModel:
assert program.has_undefined_constants() assert program.has_undefined_constants()
prop = "P=? [F \"target\"]" prop = "P=? [F \"target\"]"
formulas = stormpy.parse_formulas_for_prism_program(prop, program) 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_states() == 613
assert model.nr_transitions() == 803 assert model.nr_transitions() == 803
assert model.model_type() == stormpy.ModelType.DTMC assert model.model_type() == stormpy.ModelType.DTMC
@ -68,7 +66,7 @@ class TestModel:
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"one\" ]", program)
model = stormpy.build_model(program, formulas[0]) model = stormpy.build_model(program, formulas[0])
labels = model.labels() labels = model.labels()
assert len(labels) == 2
assert len(labels) == 3
assert "init" in labels assert "init" in labels
assert "one" in labels assert "one" in labels
assert "init" in model.labels_state(0) assert "init" in model.labels_state(0)
@ -87,7 +85,7 @@ class TestModel:
formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program) formulas = stormpy.parse_formulas_for_prism_program("P=? [ F \"target\" ]", program)
model = stormpy.build_parametric_model(program, formulas[0]) model = stormpy.build_parametric_model(program, formulas[0])
labels = model.labels() labels = model.labels()
assert len(labels) == 2
assert len(labels) == 3
assert "init" in labels assert "init" in labels
assert "target" in labels assert "target" in labels
assert "init" in model.labels_state(0) assert "init" in model.labels_state(0)

Loading…
Cancel
Save