From 4aaea6b5b08f916e5cbc221c1872583576d5c59d Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 5 Feb 2025 23:56:47 +0100 Subject: [PATCH] Fixes for transient variables in JANI When building JANI models with rewards, we employ an optimization that lifts similar transient edge destination assignments to the edge, so that they only have to be evaluated once for a given edge (and not for each destination). This previously would yield incorrect rewards when the initial (default) value of a transient variable is not zero. We make the decision when to apply the optimization more conservative to avoid such cases. Also fixes a minor issue in a sanity check --- src/storm/generator/JaniNextStateGenerator.cpp | 13 +++++++++++++ src/storm/generator/TransientVariableInformation.h | 2 +- 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index a269f260c..e025cd470 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -84,6 +84,19 @@ JaniNextStateGenerator::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. diff --git a/src/storm/generator/TransientVariableInformation.h b/src/storm/generator/TransientVariableInformation.h index 9b4910354..4aaf4d0e6 100644 --- a/src/storm/generator/TransientVariableInformation.h +++ b/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."); }