From ae036cfad59b468ef4fc150a555dbf84f0d38556 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 20 Feb 2020 16:14:29 +0100 Subject: [PATCH] Adapted state space sizes in tests as Storm improvements lead to smaller models --- lib/stormpy/examples/files/ctmc/polling2.sm | 2 +- tests/pars/test_parametric_model.py | 15 ++++++++++++++- tests/storage/test_model.py | 6 +++--- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/lib/stormpy/examples/files/ctmc/polling2.sm b/lib/stormpy/examples/files/ctmc/polling2.sm index 8fdc2f7..3e7a0ae 100644 --- a/lib/stormpy/examples/files/ctmc/polling2.sm +++ b/lib/stormpy/examples/files/ctmc/polling2.sm @@ -50,4 +50,4 @@ rewards "served" [serve1] true : 1; endrewards -label "target" = s=1&a=0; +label "target" = s=1&a=1; diff --git a/tests/pars/test_parametric_model.py b/tests/pars/test_parametric_model.py index f3631f6..b0fc8da 100644 --- a/tests/pars/test_parametric_model.py +++ b/tests/pars/test_parametric_model.py @@ -19,6 +19,19 @@ class TestSparseParametricModel: assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc + def test_build_parametric_dtmc_preprocess(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "herman5.pm")) + formulas = stormpy.parse_properties_for_prism_program("R=? [ F \"stable\" ]", program) + trans_program, trans_formulas = stormpy.preprocess_prism_program(program, formulas, "") + trans_prism = trans_program.as_prism_program() + model = stormpy.build_parametric_model(trans_prism, trans_formulas) + assert model.nr_states == 33 + assert model.nr_transitions == 266 + 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.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -61,7 +74,7 @@ class TestSymbolicParametricModel: trans_prism = trans_program.as_prism_program() model = stormpy.build_symbolic_parametric_model(trans_prism, trans_formulas) assert model.nr_states == 33 - assert model.nr_transitions == 276 + assert model.nr_transitions == 266 assert model.model_type == stormpy.ModelType.DTMC assert model.supports_parameters assert model.has_parameters diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 6345e05..3adfb98 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -106,8 +106,8 @@ class TestSparseModel: assert not model.supports_parameters assert type(model) is stormpy.SparseCtmc model_for_formula = stormpy.build_model(program, formulas) - assert model_for_formula.nr_states == 1 - assert model_for_formula.nr_transitions == 1 + assert model_for_formula.nr_states == 12 + assert model_for_formula.nr_transitions == 21 assert model_for_formula.model_type == stormpy.ModelType.CTMC assert not model_for_formula.supports_parameters assert type(model_for_formula) is stormpy.SparseCtmc @@ -229,7 +229,7 @@ class TestSymbolicSylvanModel: formulas = stormpy.parse_properties_for_prism_program("P=? [ F<=3 \"target\" ]", program) model = stormpy.build_symbolic_model(program, formulas) assert model.nr_states == 12 - assert model.nr_transitions == 22 + assert model.nr_transitions == 21 assert model.model_type == stormpy.ModelType.CTMC assert not model.supports_parameters assert type(model) is stormpy.SymbolicSylvanCtmc