From 219b342da52ebc4ed8e29db343471192401c4c30 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 3 Aug 2017 17:39:24 +0200
Subject: [PATCH] Test for jani property

---
 CHANGELOG.md                 | 1 +
 tests/logic/test_formulas.py | 7 +++++++
 2 files changed, 8 insertions(+)

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