From d5c6a509a2f214b604c60becc4611fe6415a6789 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 6 Apr 2021 06:54:33 +0200
Subject: [PATCH] JaniNextStateGenerator: Fixed evaluation of terminal states
 using expressions over transient variables

---
 src/storm/generator/JaniNextStateGenerator.cpp | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 9e53c7076..d97ed6c3d 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -98,10 +98,9 @@ namespace storm {
             if (this->options.hasTerminalStates()) {
                 for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
                     if (expressionOrLabelAndBool.first.isExpression()) {
-                        this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
+                        this->terminalStates.emplace_back(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second);
                     } else {
-                        // If it's a label, i.e. refers to a transient boolean variable we need to derive the expression
-                        // for the label so we can cut off the exploration there.
+                        // If it's a label, i.e. refers to a transient boolean variable we do some sanity checks first
                         if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") {
                             STORM_LOG_THROW(this->model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             
@@ -109,7 +108,7 @@ namespace storm {
                             STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
                             
-                            this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata), expressionOrLabelAndBool.second));
+                            this->terminalStates.emplace_back(variable.getExpressionVariable().getExpression(), expressionOrLabelAndBool.second);
                         }
                     }
                 }
@@ -563,19 +562,22 @@ 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) {
+                        // Set back transient variables to default values so we are ready to process the next state
+                        this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
                         return result;
                     }
                 }
             }
             
+            // Set back transient variables to default values so we are ready to process the transition assignments
+            this->transientVariableInformation.setDefaultValuesInEvaluator(*this->evaluator);
+            
             // Get all choices for the state.
             result.setExpanded();
             std::vector<Choice<ValueType>> allChoices;