From f0c451aae9353d0694a610740e32af786d44229b Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 12 Jul 2018 18:17:25 +0200
Subject: [PATCH] fixed a case where time path propreties were not identified
 as such, and ensured for debugging that time operators now get a time path
 formula

---
 CHANGELOG.md                            | 1 +
 src/storm/logic/EventuallyFormula.cpp   | 2 +-
 src/storm/logic/TimeOperatorFormula.cpp | 3 ++-
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b75150e65..a77718885 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,7 @@ Version 1.2.x
 - `storm-counterexamples` extracted to reduce linking time
 - Improved export for jani models
 - Several extensions to high-level counterexamples
+- A fix in parsing jani properties
 
 ### Version 1.2.1 (2018/02)
 - Multi-dimensional reward bounded reachability properties for DTMCs.
diff --git a/src/storm/logic/EventuallyFormula.cpp b/src/storm/logic/EventuallyFormula.cpp
index 5b7a2cdac..2f1243f8a 100644
--- a/src/storm/logic/EventuallyFormula.cpp
+++ b/src/storm/logic/EventuallyFormula.cpp
@@ -31,7 +31,7 @@ namespace storm {
         }
         
         bool EventuallyFormula::isProbabilityPathFormula() const {
-            return this->isEventuallyFormula();
+            return this->isReachabilityProbabilityFormula();
         }
         
         bool EventuallyFormula::isRewardPathFormula() const {
diff --git a/src/storm/logic/TimeOperatorFormula.cpp b/src/storm/logic/TimeOperatorFormula.cpp
index 7ae4b7fea..f32568cdc 100644
--- a/src/storm/logic/TimeOperatorFormula.cpp
+++ b/src/storm/logic/TimeOperatorFormula.cpp
@@ -1,5 +1,5 @@
 #include "storm/logic/TimeOperatorFormula.h"
-
+#include "storm/logic/EventuallyFormula.h"
 #include "storm/logic/FormulaVisitor.h"
 
 #include "storm/utility/macros.h"
@@ -8,6 +8,7 @@
 namespace storm {
     namespace logic {
         TimeOperatorFormula::TimeOperatorFormula(std::shared_ptr<Formula const> const& subformula, OperatorInformation const& operatorInformation, RewardMeasureType rewardMeasureType) : OperatorFormula(subformula, operatorInformation), rewardMeasureType(rewardMeasureType) {
+            assert(subformula->isTimePathFormula());
             // Intentionally left empty.
         }