From 858de4bf4865223daeeede0a80d2446e0bb526ae Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 26 Sep 2018 20:49:54 +0200 Subject: [PATCH] 'applyUpdate' in jani next state generator now works in-place --- .../generator/JaniNextStateGenerator.cpp | 31 +++++++++---------- src/storm/generator/JaniNextStateGenerator.h | 2 +- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 1d74a59b5..4499b5db4 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -287,11 +287,10 @@ namespace storm { } template - CompressedState JaniNextStateGenerator::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentLevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator) { - CompressedState newState(state); + void JaniNextStateGenerator::applyUpdate(CompressedState& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentLevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator) { // Update the location of the state. - setLocation(newState, locationVariable, destination.getLocationIndex()); + setLocation(state, locationVariable, destination.getLocationIndex()); // Then perform the assignments. auto const& assignments = destination.getOrderedAssignments().getNonTransientAssignments(assignmentLevel); @@ -304,7 +303,7 @@ namespace storm { while (assignmentIt->getExpressionVariable() != boolIt->variable) { ++boolIt; } - newState.set(boolIt->bitOffset, expressionEvaluator.asBool(assignmentIt->getAssignedExpression())); + state.set(boolIt->bitOffset, expressionEvaluator.asBool(assignmentIt->getAssignedExpression())); } // Iterate over all integer assignments and carry them out. @@ -316,14 +315,14 @@ namespace storm { int_fast64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression()); if (this->options.isAddOutOfBoundsStateSet()) { if (assignedValue < integerIt->lowerBound || assignedValue > integerIt->upperBound) { - return this->outOfBoundsState; + state = this->outOfBoundsState; } } else if (integerIt->forceOutOfBoundsCheck || this->options.isExplorationChecksSet()) { STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); } - newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); - STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); + state.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); + STORM_LOG_ASSERT(static_cast(state.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << state.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); } // Iterate over all array access assignments and carry them out. for (; assignmentIt != assignmentIte && assignmentIt->lValueIsArrayAccess(); ++assignmentIt) { @@ -333,17 +332,17 @@ namespace storm { int_fast64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression()); if (this->options.isAddOutOfBoundsStateSet()) { if (assignedValue < intInfo.lowerBound || assignedValue > intInfo.upperBound) { - return this->outOfBoundsState; + state = this->outOfBoundsState; } } else if (this->options.isExplorationChecksSet()) { STORM_LOG_THROW(assignedValue >= intInfo.lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getLValue() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); STORM_LOG_THROW(assignedValue <= intInfo.upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getLValue() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'."); } - newState.setFromInt(intInfo.bitOffset, intInfo.bitWidth, assignedValue - intInfo.lowerBound); - STORM_LOG_ASSERT(static_cast(newState.getAsInt(intInfo.bitOffset, intInfo.bitWidth)) + intInfo.lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(intInfo.bitOffset, intInfo.bitWidth) << " but wrote " << assignedValue << ")."); + state.setFromInt(intInfo.bitOffset, intInfo.bitWidth, assignedValue - intInfo.lowerBound); + STORM_LOG_ASSERT(static_cast(state.getAsInt(intInfo.bitOffset, intInfo.bitWidth)) + intInfo.lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << state.getAsInt(intInfo.bitOffset, intInfo.bitWidth) << " but wrote " << assignedValue << ")."); } else if (assignmentIt->getAssignedExpression().hasBooleanType()) { BooleanVariableInformation const& boolInfo = this->variableInformation.getBooleanArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex); - newState.set(boolInfo.bitOffset, expressionEvaluator.asBool(assignmentIt->getAssignedExpression())); + state.set(boolInfo.bitOffset, expressionEvaluator.asBool(assignmentIt->getAssignedExpression())); } else { STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled type of base variable."); } @@ -351,7 +350,6 @@ namespace storm { // Check that we processed all assignments. STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); - return newState; } template @@ -552,7 +550,8 @@ namespace storm { int64_t assignmentLevel = edge.getLowestAssignmentLevel(); // Might be the largest possible integer, if there is no assignment int64_t const& highestLevel = edge.getHighestAssignmentLevel(); bool hasTransientAssignments = destination.hasTransientAssignment(); - CompressedState newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); + CompressedState newState = state; + applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); if (hasTransientAssignments) { STORM_LOG_ASSERT(this->options.isScaleAndLiftTransitionRewardsSet(), "Transition rewards are not supported and scaling to action rewards is disabled."); transientVariableValuation.clear(); @@ -565,7 +564,7 @@ namespace storm { ++assignmentLevel; unpackStateIntoEvaluator(newState, this->variableInformation, *this->evaluator); evaluatorChanged = true; - newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); + applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); if (hasTransientAssignments) { transientVariableValuation.clear(); applyTransientUpdate(transientVariableValuation, destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator); @@ -677,7 +676,7 @@ namespace storm { break; } - successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), lowestDestinationAssignmentLevel, *this->evaluator); + applyUpdate(successorState, *destinations.back(), *locationVars.back(), lowestDestinationAssignmentLevel, *this->evaluator); applyTransientUpdate(transientVariableValuation, destinations.back()->getOrderedAssignments().getTransientAssignments(lowestDestinationAssignmentLevel), *this->evaluator); } @@ -692,7 +691,7 @@ namespace storm { evaluatorChanged = true; auto locationVarIt = locationVars.begin(); for (auto const& destPtr : destinations) { - successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, *this->evaluator); + applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, *this->evaluator); applyTransientUpdate(transientVariableValuation, destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator); ++locationVarIt; } diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 290ea3cdd..cdcc07cf1 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -78,7 +78,7 @@ namespace storm { * @params assignmentLevel The assignmentLevel that is to be considered for the update. * @return The resulting state. */ - CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator); + void applyUpdate(CompressedState& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, int64_t assignmentlevel, storm::expressions::ExpressionEvaluator const& expressionEvaluator); /*! * Applies an update to the state currently loaded into the evaluator and applies the resulting values to