diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index a17ea85..b0c1c1b 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -69,22 +69,6 @@ class TestModelChecking: reference = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] assert all(map(math.isclose, result.get_values(), reference)) - def test_parametric_state_elimination(self): - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - prop = "P=? [F s=5]" - formulas = stormpy.parse_properties_for_prism_program(prop, program) - model = stormpy.build_parametric_model(program, formulas) - assert model.nr_states == 613 - assert model.nr_transitions == 803 - assert model.model_type == stormpy.ModelType.DTMC - assert model.has_parameters - initial_state = model.initial_states[0] - assert initial_state == 0 - result = stormpy.model_checking(model, formulas[0]) - func = result.at(initial_state) - one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) - assert func.denominator == one - def test_model_checking_prob01(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulaPhi = stormpy.parse_properties("true")[0] diff --git a/tests/pars/test_parametric.py b/tests/pars/test_parametric.py index 4b74b3a..71944e4 100644 --- a/tests/pars/test_parametric.py +++ b/tests/pars/test_parametric.py @@ -8,6 +8,22 @@ from configurations import pars @pars class TestParametric: + def test_parametric_state_elimination(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.nr_states == 613 + assert model.nr_transitions == 803 + assert model.model_type == stormpy.ModelType.DTMC + assert model.has_parameters + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + func = result.at(initial_state) + one = stormpy.FactorizedPolynomial(stormpy.RationalRF(1)) + assert func.denominator == one + def test_constraints_collector(self): from pycarl.formula import FormulaType, Relation if stormpy.info.storm_ratfunc_use_cln(): diff --git a/tests/pars/test_parametric_model.py b/tests/pars/test_parametric_model.py new file mode 100644 index 0000000..d71886a --- /dev/null +++ b/tests/pars/test_parametric_model.py @@ -0,0 +1,41 @@ +import stormpy +import stormpy.info +import stormpy.logic +from helpers.helper import get_example_path + +from configurations import pars + + +@pars +class TestParametricModel: + def test_build_parametric_dtmc(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) + model = stormpy.build_parametric_model(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 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) + model = stormpy.build_parametric_model(program, formulas) + 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_build_parametric_mdp(self): + program = stormpy.parse_prism_program(get_example_path("pmdp", "two_dice.nm")) + formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program) + model = stormpy.build_parametric_model(program, formulas) + assert model.nr_states == 169 + assert model.nr_transitions == 435 + assert model.model_type == stormpy.ModelType.MDP + assert model.supports_parameters + assert type(model) is stormpy.SparseParametricMdp diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 80016e4..d3c4b90 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -56,18 +56,6 @@ class TestModel: assert reward == 1.0 or reward == 0.0 assert not model.reward_models["coin_flips"].has_transition_rewards - def test_build_parametric_dtmc_from_prism_program(self): - program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) - prop = "P=? [F s=5]" - formulas = stormpy.parse_properties_for_prism_program(prop, program) - model = stormpy.build_parametric_model(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 type(model) is stormpy.SparseParametricDtmc - def test_build_dtmc_from_jani_model(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) model = stormpy.build_model(jani_model) @@ -108,28 +96,6 @@ class TestModel: 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", "brp16_2.pm")) - formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program) - model = stormpy.build_parametric_model(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 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) - model = stormpy.build_parametric_model(program, formulas) - 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_build_mdp(self): program = stormpy.parse_prism_program(get_example_path("mdp", "two_dice.nm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"two\" ]", program)