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

@@ -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.

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 {

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.
         }