From 66e6938d2037e07143c48365286d79944b641c23 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 30 Mar 2021 10:43:20 +0200 Subject: [PATCH] added a few clarifying comments in JaniNextStateGenerator --- src/storm/generator/JaniNextStateGenerator.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index cfe694c2b..9e53c7076 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -550,6 +550,8 @@ namespace storm { template StateBehavior JaniNextStateGenerator::expand(StateToIdCallback const& stateToIdCallback) { + // The evaluator should have the default values of the transient variables right now. + // Prepare the result, in case we return early. StateBehavior result; @@ -561,10 +563,11 @@ namespace storm { auto transientVariableValuation = getTransientVariableValuationAtLocations(locations, *this->evaluator); transientVariableValuation.setInEvaluator(*this->evaluator, this->getOptions().isExplorationChecksSet()); result.addStateRewards(evaluateRewardExpressions()); + // Set back transient variables to default values so we are ready to process the transition assignments this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator); - // If a terminal expression was set and we must not expand this state, return now. + // Terminal state expressions do not consider transient variables. if (!this->terminalStates.empty()) { for (auto const& expressionBool : this->terminalStates) { if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {