From ddae1c8c8009b95a4087e83d2c2e870487d15991 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 4 Aug 2017 10:34:40 +0200 Subject: [PATCH] Test (currently) unsupported jani property --- tests/core/test_modelchecking.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 6685214..676b95f 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -30,6 +30,19 @@ class TestModelChecking: result = stormpy.model_checking(model, formula) assert math.isclose(result.at(initial_state), 0.16666666666666663) + def test_model_checking_jani_dtmc(self): + jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) + formula = properties["Expected number of coin flips"] + model = stormpy.build_model(jani_model, [formula]) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + # Unsupported formula yields None result + result = stormpy.model_checking(model, formula) + assert result is None + def test_model_checking_all_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program)