From 9da3bc8053aef4deede09663e51a772e5fdf8501 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 28 Mar 2018 17:01:44 +0200 Subject: [PATCH] Test case for MDP model checking --- tests/core/test_modelchecking.py | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 70b6ae5..fef445d 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -18,6 +18,18 @@ class TestModelChecking: result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 0.16666666666666663) + def test_model_checking_prism_mdp(self): + program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm")) + formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program) + model = stormpy.build_model(program, formulas) + assert model.nr_states == 272 + assert model.nr_transitions == 492 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0]) + assert math.isclose(result.at(initial_state), 0.3828117384) + def test_model_checking_jani_dtmc(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) formula = properties["Probability to throw a six"]