diff --git a/CHANGELOG.md b/CHANGELOG.md index d55b93c..75f2ae4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ Version 0.9 - Bindings for storm-pars - Bindings for graph constraints +- Bindings for parsing JANI files - Moved expressions from own module into storage module - Travis support for build process - Tests for documentation diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index dca2d12..5a71c22 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -1,5 +1,6 @@ import stormpy import stormpy.logic +from helpers.helper import get_example_path class TestFormulas: @@ -30,6 +31,12 @@ class TestFormulas: assert str(formulas[0]) == "P" + prop 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) + def test_bounds(self): prop = "P=? [F \"one\"]" formula = stormpy.parse_properties(prop)[0].raw_formula