Fixes for transient variables in JANI

src/storm/generator/JaniNextStateGenerator.cpp

@@ -84,6 +84,19 @@ JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani
             hasNonTrivialRewardExpressions = hasNonTrivialRewardExpressions || this->model.isNonTrivialRewardModelExpression(rewardModelName);
         }
     }
+    // If a transient variable has a non-zero default value, we also consider that non-trivial.
+    // In those cases, lifting edge destination assignments to the edges would mean that reward is collected twice:
+    // once at the edge (assigned value), once at the edge destinations (default value).
+    if (!hasNonTrivialRewardExpressions) {
+        for (auto const& rewExpr : rewardExpressions) {
+            STORM_LOG_ASSERT(rewExpr.second.isVariable(), "Expected trivial reward expression to be a variable. Got " << rewExpr.second << " instead.");
+            auto const& var = this->model.getGlobalVariables().getVariable(rewExpr.second.getBaseExpression().asVariableExpression().getVariable());
+            if (var.isTransient() && var.hasInitExpression() && !storm::utility::isZero(var.getInitExpression().evaluateAsRational())) {
+                hasNonTrivialRewardExpressions = true;
+                break;
+            }
+        }
+    }
 
     // We try to lift the edge destination assignments to the edges as this reduces the number of evaluator calls.
     // However, this will only be helpful if there are no assignment levels and only trivial reward expressions.

src/storm/generator/TransientVariableInformation.h

@@ -77,7 +77,7 @@ struct TransientVariableValuation {
                 STORM_LOG_THROW(!varValue.first->lowerBound.is_initialized() || varValue.first->lowerBound.get() <= varValue.second,
                                 storm::exceptions::OutOfRangeException,
                                 "The assigned value for transient variable " << varValue.first->variable.getName() << " is smaller than its lower bound.");
-                STORM_LOG_THROW(varValue.first->upperBound.is_initialized() || varValue.second <= varValue.first->upperBound.get(),
+                STORM_LOG_THROW(!varValue.first->upperBound.is_initialized() || varValue.second <= varValue.first->upperBound.get(),
                                 storm::exceptions::OutOfRangeException,
                                 "The assigned value for transient variable " << varValue.first->variable.getName() << " is higher than its upper bound.");
             }