From 5b103579f2afa5225591d1a426ff21a29a157782 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 29 May 2020 09:09:31 +0200
Subject: [PATCH] Fixed building state valuations for transient variables of a
 jani model.

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

diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index 0506629f1..8592cd834 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -503,9 +503,11 @@ namespace storm {
             auto transientVariableValuation = getTransientVariableValuationAtLocations(getLocations(*this->state));
             {
                 auto varIt = transientVariableValuation.booleanValues.begin();
+                auto varIte = transientVariableValuation.booleanValues.end();
                 for (auto const& varInfo : transientVariableInformation.booleanVariableInformation) {
-                    if (varIt->first->variable == varInfo.variable) {
+                    if (varIt != varIte && varIt->first->variable == varInfo.variable) {
                         booleanValues.push_back(varIt->second);
+                        ++varIt;
                     } else {
                         booleanValues.push_back(varInfo.defaultValue);
                     }
@@ -513,9 +515,11 @@ namespace storm {
             }
             {
                 auto varIt = transientVariableValuation.integerValues.begin();
+                auto varIte = transientVariableValuation.integerValues.end();
                 for (auto const& varInfo : transientVariableInformation.integerVariableInformation) {
-                    if (varIt->first->variable == varInfo.variable) {
+                    if (varIt != varIte && varIt->first->variable == varInfo.variable) {
                         integerValues.push_back(varIt->second);
+                        ++varIt;
                     } else {
                         integerValues.push_back(varInfo.defaultValue);
                     }
@@ -523,9 +527,11 @@ namespace storm {
             }
             {
                 auto varIt = transientVariableValuation.rationalValues.begin();
+                auto varIte = transientVariableValuation.rationalValues.end();
                 for (auto const& varInfo : transientVariableInformation.rationalVariableInformation) {
-                    if (varIt->first->variable == varInfo.variable) {
+                    if (varIt != varIte && varIt->first->variable == varInfo.variable) {
                         rationalValues.push_back(storm::utility::convertNumber<storm::RationalNumber>(varIt->second));
+                        ++varIt;
                     } else {
                         rationalValues.push_back(storm::utility::convertNumber<storm::RationalNumber>(varInfo.defaultValue));
                     }