From d47189f93e7ea20617fc6661409741102d62cd5d Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 15 Sep 2018 11:29:25 +0200 Subject: [PATCH] fixes for array elimination --- .../generator/JaniNextStateGenerator.cpp | 49 ++++++++++--------- src/storm/storage/jani/ArrayEliminator.cpp | 48 +++++++++++++++--- src/storm/storage/jani/ArrayEliminator.h | 15 +++--- src/storm/storage/jani/Edge.cpp | 29 ++++++++++- src/storm/storage/jani/Edge.h | 4 ++ .../jani/traverser/ArrayExpressionFinder.cpp | 2 +- 6 files changed, 109 insertions(+), 38 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index bd034ece7..21b796683 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -301,8 +301,8 @@ namespace storm { return this->outOfBoundsState; } } else if (this->options.isExplorationChecksSet()) { - STORM_LOG_THROW(assignedValue >= intInfo.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 <= intInfo.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() << "'."); + 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 << ")."); @@ -444,16 +444,19 @@ namespace storm { auto valueIt = stateActionRewards.begin(); performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); } - while (assignmentLevel < highestLevel) { - ++assignmentLevel; - auto currentLevelEvaluator = storm::expressions::ExpressionEvaluator(model.getManager()); - unpackStateIntoEvaluator(newState, this->variableInformation, currentLevelEvaluator); - newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, currentLevelEvaluator); - if (hasTransientRewardAssignments) { - // update the rewards for this destination - auto valueIt = stateActionRewards.begin(); - performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), currentLevelEvaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); + if (assignmentLevel < highestLevel) { + while (assignmentLevel < highestLevel) { + ++assignmentLevel; + unpackStateIntoEvaluator(newState, this->variableInformation, *this->evaluator); + newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator); + if (hasTransientRewardAssignments) { + // update the rewards for this destination + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(destination.getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&] (ValueType const& value) { *valueIt += (value * probability); ++valueIt; } ); + } } + // Restore the old state information + unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator); } StateType stateIndex = stateToIdCallback(newState); @@ -509,17 +512,17 @@ namespace storm { nextDistribution.clear(); EdgeIndexSet edgeIndices; - int64_t assignmentLevel = std::numeric_limits::max(); - int64_t highestLevel = std::numeric_limits::min(); + int64_t lowestLevel = std::numeric_limits::max(); + int64_t highestLevel = std::numeric_limits::min(); for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { if (this->getOptions().isBuildChoiceOriginsSet()) { edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, iteratorList[i]->first)); } - assignmentLevel = std::min(assignmentLevel, iteratorList[i]->second->getLowestAssignmentLevel()); + lowestLevel = std::min(lowestLevel, iteratorList[i]->second->getLowestAssignmentLevel()); highestLevel = std::max(highestLevel, iteratorList[i]->second->getHighestAssignmentLevel()); } - if (assignmentLevel >= highestLevel) { + if (lowestLevel >= highestLevel) { // When all assignments have the same level, we can perform the assignments of the different automata sequentially for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { auto const& indexAndEdge = *iteratorList[i]; @@ -536,7 +539,7 @@ namespace storm { } for (auto const& stateProbability : currentDistribution) { // Compute the new state under the current update and add it to the set of new target states. - CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first], assignmentLevel, *this->evaluator); + CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first], lowestLevel, *this->evaluator); // If the new state was already found as a successor state, update the probability // and insert it. @@ -597,30 +600,32 @@ namespace storm { break; } - successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), assignmentLevel, *this->evaluator); + successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), lowestLevel, *this->evaluator); // add the reward for this destination to the destination rewards auto valueIt = destinationRewards.begin(); - performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); + performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(lowestLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); } if (!storm::utility::isZero(successorProbability)) { + int64_t assignmentLevel = lowestLevel; // remaining assignment levels while (assignmentLevel < highestLevel) { ++assignmentLevel; - auto currentLevelEvaluator = storm::expressions::ExpressionEvaluator(model.getManager()); - unpackStateIntoEvaluator(successorState, this->variableInformation, currentLevelEvaluator); + unpackStateIntoEvaluator(successorState, this->variableInformation, *this->evaluator); auto locationVarIt = locationVars.begin(); for (auto const& destPtr : destinations) { - successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, currentLevelEvaluator); + successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, *this->evaluator); // add the reward for this destination to the destination rewards auto valueIt = destinationRewards.begin(); - performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), currentLevelEvaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); + performTransientAssignments(destinations.back()->getOrderedAssignments().getTransientAssignments(assignmentLevel), *this->evaluator, [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); ++locationVarIt; } } nextDistribution.add(successorState, successorProbability); storm::utility::vector::addScaledVector(stateActionRewards, destinationRewards, successorProbability); + // Restore the old state information + unpackStateIntoEvaluator(state, this->variableInformation, *this->evaluator); } ++destinationId; } while (!lastDestinationId); diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp index e04d20d13..16e0c5671 100644 --- a/src/storm/storage/jani/ArrayEliminator.cpp +++ b/src/storm/storage/jani/ArrayEliminator.cpp @@ -5,6 +5,9 @@ #include "storm/storage/expressions/ExpressionVisitor.h" #include "storm/storage/jani/expressions/JaniExpressionVisitor.h" #include "storm/storage/jani/Variable.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" +#include "storm/storage/jani/traverser/JaniTraverser.h" #include "storm/storage/jani/traverser/ArrayExpressionFinder.h" #include "storm/storage/expressions/Expressions.h" @@ -13,8 +16,12 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/UnexpectedException.h" +#include "storm/exceptions/OutOfRangeException.h" namespace storm { + + + namespace jani { namespace detail { @@ -128,17 +135,42 @@ namespace storm { storm::expressions::Expression eliminate(storm::expressions::Expression const& expression) { // here, data is the accessed index of the most recent array access expression. Initially, there is none. - std::cout << "Eliminating arrays in expression " << expression << std::endl; auto res = storm::expressions::Expression(boost::any_cast(expression.accept(*this, boost::any()))); STORM_LOG_ASSERT(!containsArrayExpression(res), "Expression still contains array expressions. Before: " << std::endl << expression << std::endl << "After:" << std::endl << res); return res.simplify(); } virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override { + BaseExprPtr thenExpression, elseExpression; + + // We need to handle expressions of the kind '42(expression.getThenExpression()->accept(*this, data)); + } catch (storm::exceptions::OutOfRangeException const&) { + thenOutOfRange = true; + } + try { + elseExpression = boost::any_cast(expression.getElseExpression()->accept(*this, data)); + } catch (storm::exceptions::OutOfRangeException const& e) { + if (thenOutOfRange) { + throw e; + } else { + elseOutOfRange = true; + } + } + + if (thenOutOfRange) { + assert(!elseOutOfRange); + return elseExpression; + } else if (elseOutOfRange) { + return thenExpression; + } + // for the condition expression, outer array accesses should not matter. BaseExprPtr conditionExpression = boost::any_cast(expression.getCondition()->accept(*this, boost::any())); - BaseExprPtr thenExpression = boost::any_cast(expression.getThenExpression()->accept(*this, data)); - BaseExprPtr elseExpression = boost::any_cast(expression.getElseExpression()->accept(*this, data)); // If the arguments did not change, we simply push the expression itself. if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) { @@ -193,7 +225,8 @@ namespace storm { uint64_t index = boost::any_cast(data); STORM_LOG_ASSERT(replacements.find(expression.getVariable()) != replacements.end(), "Unable to find array variable " << expression << " in array replacements."); auto const& arrayVarReplacements = replacements.at(expression.getVariable()); - STORM_LOG_ASSERT(index < arrayVarReplacements.size(), "No replacement for array variable, since index " << index << " is out of bounds."); + if (index >= arrayVarReplacements.size()) throw storm::exceptions::OutOfRangeException(); + //STORM_LOG_THROW(index < arrayVarReplacements.size(), storm::exceptions::OutOfRangeException, "Array index " << index << " for variable " << expression << " is out of bounds."); return arrayVarReplacements[index]->getExpressionVariable().getExpression().getBaseExpressionPointer(); } else { STORM_LOG_ASSERT(data.empty(), "VariableExpression of non-array variable should not be a subexpressions of array access expressions. However, the expression " << expression << " is."); @@ -242,7 +275,8 @@ namespace storm { STORM_LOG_THROW(!data.empty(), storm::exceptions::NotSupportedException, "Unable to translate ValueArrayExpression to element expression since it does not seem to be within an array access expression."); uint64_t index = boost::any_cast(data); STORM_LOG_ASSERT(expression.size()->isIntegerLiteralExpression(), "unexpected kind of size expression of ValueArrayExpression (" << expression.size()->toExpression() << ")."); - STORM_LOG_THROW(index < static_cast(expression.size()->evaluateAsInt()), storm::exceptions::UnexpectedException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression); + if (index >= static_cast(expression.size()->evaluateAsInt())) throw storm::exceptions::OutOfRangeException(); + // STORM_LOG_THROW(index < static_cast(expression.size()->evaluateAsInt()), storm::exceptions::OutOfRangeException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression); return boost::any_cast(expression.at(index)->accept(*this, boost::any())); } @@ -252,7 +286,8 @@ namespace storm { if (expression.size()->containsVariables()) { STORM_LOG_WARN("Ignoring length of constructorArrayExpression " << expression << " as it still contains variables."); } else { - STORM_LOG_THROW(index < static_cast(expression.size()->evaluateAsInt()), storm::exceptions::UnexpectedException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression); + if (index >= static_cast(expression.size()->evaluateAsInt())) throw storm::exceptions::OutOfRangeException(); + // STORM_LOG_THROW(index < static_cast(expression.size()->evaluateAsInt()), storm::exceptions::OutOfRangeException, "Out of bounds array access occured while accessing index " << index << " of expression " << expression); } return boost::any_cast(expression.at(index)->accept(*this, boost::any())); } @@ -450,7 +485,6 @@ namespace storm { if (!insertionRes.second) { insertionRes.first->second.push_back(&assignment); } - continue; } else { // Keeping array access LValue LValue newLValue(LValue(assignment.getLValue().getArray()), arrayExprEliminator->eliminate(assignment.getLValue().getArrayIndex())); diff --git a/src/storm/storage/jani/ArrayEliminator.h b/src/storm/storage/jani/ArrayEliminator.h index 70d2fe897..26f4f3df8 100644 --- a/src/storm/storage/jani/ArrayEliminator.h +++ b/src/storm/storage/jani/ArrayEliminator.h @@ -1,13 +1,17 @@ #pragma once -#include - -#include "storm/storage/jani/traverser/JaniTraverser.h" -#include "storm/storage/jani/Property.h" +#include "storm/storage/jani/Variable.h" +#include "storm/storage/expressions/Variable.h" namespace storm { + namespace expressions { + class Expression; + } + namespace jani { + class Model; + class Property; struct ArrayEliminatorData { std::vector> eliminatedArrayVariables; @@ -29,9 +33,6 @@ namespace storm { ArrayEliminatorData eliminate(Model& model, bool keepNonTrivialArrayAccess = false); - private: - - }; } } diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index 240317817..301c695a0 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/src/storm/storage/jani/Edge.cpp @@ -147,6 +147,33 @@ namespace storm { return templateEdge; } - + std::ostream& operator<<(std::ostream& stream, Edge const& edge) { + stream << "[" << (edge.hasSilentAction() ? "" : ("action_id: " + std::to_string(edge.getActionIndex()))) << "]"; + stream << "guard: '" << edge.getGuard() << "'\t from_location_id: " << edge.getSourceLocationIndex(); + if (edge.hasRate()) { + stream << " with rate '" << edge.getRate() << "'"; + } + if (edge.getDestinations().empty()) { + stream << "without any destination"; + } else { + stream << " to ... [" << std::endl; + for (auto const& dest : edge.getDestinations()) { + stream << "\tlocation_id: " << dest.getLocationIndex() << " with probability '" << dest.getProbability() << "' and updates: "; + if (dest.getOrderedAssignments().empty()) { + stream << "none" << std::endl; + } + bool first = true; + for (auto const& a : dest.getOrderedAssignments()) { + if (first) { + first = false; + stream << a; + } + stream << ", " << a; + } + } + stream << "]"; + } + return stream; + } } } diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index c6ab6d28d..36abaa5f3 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -4,6 +4,7 @@ #include #include +#include #include "storm/storage/jani/EdgeDestination.h" #include "storm/storage/jani/OrderedAssignments.h" @@ -152,5 +153,8 @@ namespace storm { std::vector destinations; }; + std::ostream& operator<<(std::ostream& stream, Edge const& edge); + + } } diff --git a/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp b/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp index 8e5d11a92..8ade7df61 100644 --- a/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp +++ b/src/storm/storage/jani/traverser/ArrayExpressionFinder.cpp @@ -104,7 +104,7 @@ namespace storm { bool containsArrayExpression(storm::expressions::Expression const& expression) { detail::ArrayExpressionFinderExpressionVisitor v; - return boost::any_cast(expression.accept(v, boost::none)); + return boost::any_cast(expression.accept(v, boost::any())); } } }