From 32eae51b16f03a98751d2b06bdb979033ba29b77 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 3 Jan 2017 11:40:13 +0100 Subject: [PATCH] first working test for model instantiator --- tests/storage/test_model_instantiator.py | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/storage/test_model_instantiator.py diff --git a/tests/storage/test_model_instantiator.py b/tests/storage/test_model_instantiator.py new file mode 100644 index 0000000..867b3c8 --- /dev/null +++ b/tests/storage/test_model_instantiator.py @@ -0,0 +1,21 @@ +import pycarl +import stormpy +import stormpy.logic +from helpers.helper import get_example_path + +class TestModel: + def test_instantiate_dtmc(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program) + model = stormpy.build_parametric_model(program, formulas[0]) + parameters = model.collect_probability_parameters() + instantiator = stormpy.storage.PdtmcInstantiator(model) + point = dict() + for p in parameters: + point[p] = 0.4 + instantiated_model = instantiator.instantiate(point) + assert instantiated_model.nr_states == model.nr_states + assert not instantiated_model.has_parameters + for p in parameters: + point[p] = 0.5 + instatiated_model2 = instantiator.instantiate(point) \ No newline at end of file