From 93da59fa04424a8f209c7fba810706d430f70e21 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 12 Jul 2018 18:16:26 +0200
Subject: [PATCH] fixed an issue with jani properties for expected time not
 being parsed as requested

---
 src/storm-parsers/parser/JaniParser.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp
index 725ab0a9d..aa97e38f7 100644
--- a/src/storm-parsers/parser/JaniParser.cpp
+++ b/src/storm-parsers/parser/JaniParser.cpp
@@ -230,7 +230,8 @@ namespace storm {
                     }
                     std::shared_ptr<storm::logic::Formula const> reach;
                     if (propertyStructure.count("reach") > 0) {
-                        reach = std::make_shared<storm::logic::EventuallyFormula>(parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, globalVars, constants, "Reach-expression of operator " + opString));
+                        auto context = time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward;
+                        reach = std::make_shared<storm::logic::EventuallyFormula>(parseFormula(propertyStructure.at("reach"), context, globalVars, constants, "Reach-expression of operator " + opString), context);
                     } else {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Total reward is currently not supported");
                     }
@@ -304,9 +305,12 @@ namespace storm {
                     //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given.");
                     
                     if (rewExpr.isVariable()) {
+                        assert(!time);
                         std::string rewardName = rewExpr.getVariables().begin()->getName();
                         return std::make_shared<storm::logic::RewardOperatorFormula>(reach, rewardName, opInfo);
                     } else if (!rewExpr.containsVariables()) {
+                        assert(time);
+                        assert(reach->isTimePathFormula());
                         if(rewExpr.hasIntegerType()) {
                             if (rewExpr.evaluateAsInt() == 1) {
                                 
@@ -480,6 +484,7 @@ namespace storm {
             STORM_LOG_THROW(propertyStructure.count("name") ==  1, storm::exceptions::InvalidJaniException, "Property must have a name");
             // TODO check unique name
             std::string name = getString(propertyStructure.at("name"), "property-name");
+            STORM_LOG_TRACE("Parsing property named: " << name);
             std::string comment = "";
             if (propertyStructure.count("comment") > 0) {
                 comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'.");