From 415e806531933576e00223863196abab10b24da9 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 4 Apr 2019 21:43:38 +0200
Subject: [PATCH] RewardModelInformation: Fixed getting wrong reward
 informations in case of non-transient variables in reward expression.

---
 src/storm/storage/jani/traverser/RewardModelInformation.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/storm/storage/jani/traverser/RewardModelInformation.cpp b/src/storm/storage/jani/traverser/RewardModelInformation.cpp
index 908802742..d3c63aeeb 100644
--- a/src/storm/storage/jani/traverser/RewardModelInformation.cpp
+++ b/src/storm/storage/jani/traverser/RewardModelInformation.cpp
@@ -19,15 +19,19 @@ namespace storm {
         RewardModelInformation::RewardModelInformation(Model const& model, storm::expressions::Expression const& rewardModelExpression) : stateRewards(false), actionRewards(false), transitionRewards(false) {
             auto variablesInRewardExpression = rewardModelExpression.getVariables();
             std::map<storm::expressions::Variable, storm::expressions::Expression> initialSubstitution;
+            bool containsNonTransientVariable = false;
             for (auto const& v : variablesInRewardExpression) {
                 STORM_LOG_ASSERT(model.hasGlobalVariable(v.getName()), "Unable to find global variable " << v.getName() << " occurring in a reward expression.");
                 auto const& janiVar = model.getGlobalVariable(v.getName());
                 if (janiVar.hasInitExpression()) {
                     initialSubstitution.emplace(v, janiVar.getInitExpression());
                 }
+                if (!janiVar.isTransient()) {
+                    containsNonTransientVariable = true;
+                }
             }
             auto initExpr = storm::jani::substituteJaniExpression(rewardModelExpression, initialSubstitution);
-            if (initExpr.containsVariables() || !storm::utility::isZero(initExpr.evaluateAsRational())) {
+            if (containsNonTransientVariable || initExpr.containsVariables() || !storm::utility::isZero(initExpr.evaluateAsRational())) {
                 stateRewards = true;
                 actionRewards = true;
                 transitionRewards = true;