From ba6856274017f3c7da7f4e6f68555c9c1ec6dc98 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 11 Sep 2018 18:38:32 +0200 Subject: [PATCH] moved array variable replacement information into VariableInformation --- .../generator/JaniNextStateGenerator.cpp | 39 ++-------------- src/storm/generator/JaniNextStateGenerator.h | 5 +- src/storm/generator/VariableInformation.cpp | 46 +++++++++++++++++++ src/storm/generator/VariableInformation.h | 9 ++++ 4 files changed, 61 insertions(+), 38 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 8f68f4c1c..9af945704 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -68,34 +68,7 @@ namespace storm { // Now we are ready to initialize the variable information. this->checkValid(); this->variableInformation = VariableInformation(model, this->parallelAutomata, options.isAddOutOfBoundsStateSet()); - - // Find for each replaced array variable the corresponding references in the variable information - for (auto const& arrayReplacements : arrayEliminatorData.replacements) { - std::vector varInfoIndices; - for (auto const& replacedVar : arrayReplacements.second) { - if (replacedVar->getExpressionVariable().hasIntegerType()) { - uint64_t index = 0; - for (auto const& intInfo : this->variableInformation.integerVariables) { - if (intInfo.variable == replacedVar->getExpressionVariable()) { - varInfoIndices.push_back(index); - break; - } - ++index; - } - } else if (replacedVar->getExpressionVariable().hasBooleanType()) { - uint64_t index = 0; - for (auto const& boolInfo : this->variableInformation.booleanVariables) { - if (boolInfo.variable == replacedVar->getExpressionVariable()) { - varInfoIndices.push_back(index); - } - ++index; - } - } else { - STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled type of base variable."); - } - } - arrayVariableToElementInformations.emplace(arrayReplacements.first, std::move(varInfoIndices)); - } + this->variableInformation.registerArrayVariableReplacements(arrayEliminatorData); // Create a proper evalator. this->evaluator = std::make_unique>(model.getManager()); @@ -321,9 +294,7 @@ namespace storm { for (; assignmentIt != assignmentIte && assignmentIt->getLValue().isArrayAccess() && assignmentIt->getLevel() == assignmentLevel; ++assignmentIt) { int_fast64_t arrayIndex = expressionEvaluator.asInt(assignmentIt->getLValue().getArrayIndex()); if (assignmentIt->getAssignedExpression().hasIntegerType()) { - std::vector const& intInfoIndices = arrayVariableToElementInformations.at(assignmentIt->getLValue().getArray().getExpressionVariable()); - STORM_LOG_THROW(arrayIndex < intInfoIndices.size(), storm::exceptions::WrongFormatException, "Array access " << assignmentIt->getLValue() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << intInfoIndices.size()); - IntegerVariableInformation const& intInfo = this->variableInformation.integerVariables[intInfoIndices[arrayIndex]]; + IntegerVariableInformation const& intInfo = this->variableInformation.getIntegerArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex); int_fast64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression()); if (this->options.isAddOutOfBoundsStateSet()) { if (assignedValue < intInfo.lowerBound || assignedValue > intInfo.upperBound) { @@ -336,9 +307,7 @@ namespace storm { 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 << ")."); } else if (assignmentIt->getAssignedExpression().hasBooleanType()) { - std::vector const& boolInfoIndices = arrayVariableToElementInformations.at(assignmentIt->getLValue().getArray().getExpressionVariable()); - STORM_LOG_THROW(arrayIndex < boolInfoIndices.size(), storm::exceptions::WrongFormatException, "Array access " << assignmentIt->getLValue() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << boolInfoIndices.size()); - BooleanVariableInformation const& boolInfo = this->variableInformation.booleanVariables[boolInfoIndices[arrayIndex]]; + BooleanVariableInformation const& boolInfo = this->variableInformation.getBooleanArrayVariableReplacement(assignmentIt->getLValue().getArray().getExpressionVariable(), arrayIndex); newState.set(boolInfo.bitOffset, expressionEvaluator.asBool(assignmentIt->getAssignedExpression())); } else { STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled type of base variable."); @@ -612,6 +581,7 @@ namespace storm { storm::jani::Edge const& edge = *iteratorList[i]->second; destinations.push_back(&edge.getDestination(destinationIndex % edge.getNumberOfDestinations())); locationVars.push_back(&this->variableInformation.locationVariables[edgeCombination[i].first]); + STORM_LOG_ASSERT(edge.getNumberOfDestinations() > 0, "Found an edge with zero destinations. This is not expected."); std::cout << destinationIndex % edge.getNumberOfDestinations(); if (i == iteratorList.size() - 1 && (destinationIndex % edge.getNumberOfDestinations()) == edge.getNumberOfDestinations() - 1) { lastDestinationId = true; @@ -653,6 +623,7 @@ namespace storm { storm::utility::vector::addScaledVector(stateActionRewards, destinationRewards, successorProbability); } ++destinationId; + std::cout << "\t"; } while (!lastDestinationId); std::cout << std::endl; } diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index bec4112cd..e9bd01a07 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -140,11 +140,8 @@ namespace storm { /// A flag that stores whether at least one of the selected reward models has state-action rewards. bool hasStateActionRewards; - /// Data from eliminating arrays + /// Data from eliminated array expressions. These are required to keep references to array variables in LValues alive. storm::jani::ArrayEliminatorData arrayEliminatorData; - - /// Maps each array variable to the index of the base variable in this->variableInformation - std::unordered_map> arrayVariableToElementInformations; }; diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index e4befba41..36134c182 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -4,6 +4,7 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/ArrayEliminator.h" #include "storm/storage/jani/AutomatonComposition.h" #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -109,6 +110,51 @@ namespace storm { sortVariables(); } + void VariableInformation::registerArrayVariableReplacements(storm::jani::ArrayEliminatorData const& arrayEliminatorData) { + arrayVariableToElementInformations.clear(); + // Find for each replaced array variable the corresponding references in this variable information + for (auto const& arrayReplacements : arrayEliminatorData.replacements) { + std::vector varInfoIndices; + for (auto const& replacedVar : arrayReplacements.second) { + if (replacedVar->getExpressionVariable().hasIntegerType()) { + uint64_t index = 0; + for (auto const& intInfo : integerVariables) { + if (intInfo.variable == replacedVar->getExpressionVariable()) { + varInfoIndices.push_back(index); + break; + } + ++index; + } + } else if (replacedVar->getExpressionVariable().hasBooleanType()) { + uint64_t index = 0; + for (auto const& boolInfo : booleanVariables) { + if (boolInfo.variable == replacedVar->getExpressionVariable()) { + varInfoIndices.push_back(index); + break; + } + ++index; + } + } else { + STORM_LOG_ASSERT(false, "Unhandled type of base variable."); + } + } + STORM_LOG_ASSERT(arrayReplacements.second.size() == varInfoIndices.size(), "Could not find a basic variable for every array variable replacement."); + this->arrayVariableToElementInformations.emplace(arrayReplacements.first, std::move(varInfoIndices)); + } + } + + BooleanVariableInformation const& VariableInformation::getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) { + std::vector const& boolInfoIndices = arrayVariableToElementInformations.at(arrayVariable); + STORM_LOG_THROW(arrayIndex < boolInfoIndices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << boolInfoIndices.size()); + return booleanVariables[boolInfoIndices[arrayIndex]]; + } + + IntegerVariableInformation const& VariableInformation::getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t arrayIndex) { + std::vector const& intInfoIndices = arrayVariableToElementInformations.at(arrayVariable); + STORM_LOG_THROW(arrayIndex < intInfoIndices.size(), storm::exceptions::WrongFormatException, "Array access at array " << arrayVariable.getName() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << intInfoIndices.size()); + return integerVariables[intInfoIndices[arrayIndex]]; + } + void VariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton) { uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index fac200d1a..a8d53090e 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -2,6 +2,7 @@ #define STORM_GENERATOR_VARIABLEINFORMATION_H_ #include +#include #include #include @@ -15,6 +16,7 @@ namespace storm { namespace jani { class Model; class Automaton; + class ArrayEliminatorData; } namespace generator { @@ -81,6 +83,10 @@ namespace storm { VariableInformation() = default; uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const; + void registerArrayVariableReplacements(storm::jani::ArrayEliminatorData const& arrayEliminatorData); + BooleanVariableInformation const& getBooleanArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index); + IntegerVariableInformation const& getIntegerArrayVariableReplacement(storm::expressions::Variable const& arrayVariable, uint64_t index); + /// The total bit offset over all variables. uint_fast64_t totalBitOffset; @@ -92,6 +98,9 @@ namespace storm { /// The integer variables. std::vector integerVariables; + + /// Replacements for each array variable + std::unordered_map> arrayVariableToElementInformations; bool hasOutOfBoundsBit() const;