diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 2868953..485767b 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -31,8 +31,7 @@ class TestModelChecking: assert math.isclose(result.at(initial_state), 49 / 128, rel_tol=1e-5) def test_model_checking_jani_dtmc(self): - jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) - formulas = [properties["Probability to throw a six"], properties["Expected number of coin flips"]] + jani_model, formulas = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) formulas = stormpy.eliminate_reward_accumulations(jani_model, formulas) assert len(formulas) == 2 model = stormpy.build_model(jani_model, formulas) diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index 5a71c22..73b9368 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -32,10 +32,14 @@ class TestFormulas: assert str(formulas[1]) == "R[exp]" + prop def test_jani_formula(self): - _, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) - for name, prop in properties.items(): - assert "Property_brp_" in name - assert isinstance(prop, stormpy.Property) + _, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) + assert len(properties) == 2 + prop = properties[0] + assert isinstance(prop, stormpy.Property) + assert prop.name == "Probability to throw a six" + prop = properties[1] + assert isinstance(prop, stormpy.Property) + assert prop.name == "Expected number of coin flips" def test_bounds(self): prop = "P=? [F \"one\"]"