From 32f468e92caf625bd01071ac57e72c6873278680 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 18 May 2018 13:45:52 +0200
Subject: [PATCH] Added tests for symbolic parametric models

---
 tests/pars/test_parametric_model.py | 37 ++++++++++++++++++++++++++++-
 1 file changed, 36 insertions(+), 1 deletion(-)

diff --git a/tests/pars/test_parametric_model.py b/tests/pars/test_parametric_model.py
index d71886a..76e18c2 100644
--- a/tests/pars/test_parametric_model.py
+++ b/tests/pars/test_parametric_model.py
@@ -7,7 +7,7 @@ from configurations import pars
 
 
 @pars
-class TestParametricModel:
+class TestSparseParametricModel:
     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)
@@ -39,3 +39,38 @@ class TestParametricModel:
         assert model.model_type == stormpy.ModelType.MDP
         assert model.supports_parameters
         assert type(model) is stormpy.SparseParametricMdp
+
+
+@pars
+class TestSymbolicParametricModel:
+    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_symbolic_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.SymbolicSylvanParametricDtmc
+
+    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_symbolic_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.SymbolicSylvanParametricDtmc
+
+    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_symbolic_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.SymbolicSylvanParametricMdp