From 5a26d0e99f705eff9451ea0d9233f4a5f9101570 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Aug 2017 14:19:21 +0200 Subject: [PATCH] Test for building MDP --- tests/storage/test_model.py | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 8bec592..3e67c23 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -99,6 +99,16 @@ class TestModel: 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) + model = stormpy.build_model(program, formulas) + assert model.nr_states == 169 + assert model.nr_transitions == 435 + assert model.model_type == stormpy.ModelType.MDP + assert not model.supports_parameters + assert type(model) is stormpy.SparseMdp + def test_initial_states(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)