Adapted state space sizes in tests as Storm improvements lead to smaller models

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;

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

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