From c124ebcc932a0709814122405fd46e521b04bea2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 Aug 2018 15:44:54 +0200 Subject: [PATCH] Fixed a Jani-related issue when adding assignments to OrderedAssignments --- src/storm/storage/jani/OrderedAssignments.cpp | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp index 7d1967ff7..9c622fe2b 100644 --- a/src/storm/storage/jani/OrderedAssignments.cpp +++ b/src/storm/storage/jani/OrderedAssignments.cpp @@ -27,19 +27,17 @@ namespace storm { bool OrderedAssignments::add(Assignment const& assignment, bool addToExisting) { // If the element is contained in this set of assignment, nothing needs to be added. - if (this->contains(assignment)) { + if (!addToExisting && this->contains(assignment)) { return false; } // Otherwise, we find the spot to insert it. auto it = lowerBound(assignment, allAssignments); - - if (it != allAssignments.end()) { - if ((!addToExisting || !assignment.getExpressionVariable().hasNumericalType())) { - STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists."); - } else if (addToExisting && assignment.getExpressionVariable().hasNumericalType()) { - (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression()); - } + + // Check if an assignment to this variable is already present + if (it != allAssignments.end() && assignment.getExpressionVariable() == (*it)->getExpressionVariable()) { + STORM_LOG_THROW(addToExisting && assignment.getExpressionVariable().hasNumericalType(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists."); + (*it)->setAssignedExpression((*it)->getAssignedExpression() + assignment.getAssignedExpression()); } else { // Finally, insert the new element in the correct vectors. auto elementToInsert = std::make_shared(assignment);