Moved some parametric tests into tests/pars/ dir

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]

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():

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

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)