diff --git a/src/storm-parsers/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp index 16bf04056..c21add9e7 100644 --- a/src/storm-parsers/parser/JaniParser.cpp +++ b/src/storm-parsers/parser/JaniParser.cpp @@ -788,12 +788,17 @@ namespace storm { if (setInitValFromDefault) { initVal = storm::expressions::ValueArrayExpression(*expressionManager, exprVariableType, {}).toExpression(); } + std::shared_ptr result; if (initVal) { STORM_LOG_THROW(initVal->getType().isArrayType(), storm::exceptions::InvalidJaniException, "Initial value for array variable " + name + "(scope " + scopeDescription + ") should be an Array"); - return std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType, initVal.get(), transientVar); + result = std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType, initVal.get(), transientVar); } else { - return std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType); + result = std::make_shared(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType); } + if (type.arrayBase->bounds) { + result->setElementTypeBounds(type.arrayBase->bounds->first, type.arrayBase->bounds->second); + } + return result; } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scopeDescription << ")"); diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 9af945704..7801db91d 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -46,7 +46,7 @@ namespace storm { if (this->model.containsArrayVariables()) { arrayEliminatorData = this->model.eliminateArrays(true); } - + // Lift the transient edge destinations of the first assignment level. uint64_t lowestAssignmentLevel = storm::jani::AssignmentLevelFinder().getLowestAssignmentLevel(this->model); if (this->model.hasTransientEdgeDestinationAssignments()) { @@ -67,7 +67,7 @@ namespace storm { // Now we are ready to initialize the variable information. this->checkValid(); - this->variableInformation = VariableInformation(model, this->parallelAutomata, options.isAddOutOfBoundsStateSet()); + this->variableInformation = VariableInformation(this->model, this->parallelAutomata, options.isAddOutOfBoundsStateSet()); this->variableInformation.registerArrayVariableReplacements(arrayEliminatorData); // Create a proper evalator. @@ -504,8 +504,9 @@ namespace storm { bool done = false; while (!done) { std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); - + currentDistribution.clear(); currentDistribution.add(state, storm::utility::one()); + nextDistribution.clear(); EdgeIndexSet edgeIndices; uint64_t assignmentLevel = std::numeric_limits::max(); @@ -549,12 +550,12 @@ namespace storm { } } } - nextDistribution.compress(); - + // If there is one more command to come, shift the target states one time step back. if (i < iteratorList.size() - 1) { currentDistribution = std::move(nextDistribution); + nextDistribution.clear(); } } } else { @@ -582,7 +583,6 @@ namespace storm { 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; } @@ -623,10 +623,9 @@ namespace storm { storm::utility::vector::addScaledVector(stateActionRewards, destinationRewards, successorProbability); } ++destinationId; - std::cout << "\t"; } while (!lastDestinationId); - std::cout << std::endl; } + nextDistribution.compress(); for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { storm::jani::Edge const& edge = *iteratorList[i]->second; @@ -793,10 +792,15 @@ namespace storm { // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. std::unordered_map transientVariableToExpressionMap; + bool translateArrays = !this->arrayEliminatorData.replacements.empty(); for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { if (variable.isBooleanVariable()) { if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) { - transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata); + storm::expressions::Expression labelExpression = model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata); + if (translateArrays) { + labelExpression = this->arrayEliminatorData.transformExpression(labelExpression); + } + transientVariableToExpressionMap[variable.getExpressionVariable()] = std::move(labelExpression); } } } diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 36134c182..8c710f504 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -125,6 +125,7 @@ namespace storm { } ++index; } + STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); } else if (replacedVar->getExpressionVariable().hasBooleanType()) { uint64_t index = 0; for (auto const& boolInfo : booleanVariables) { @@ -134,11 +135,11 @@ namespace storm { } ++index; } + STORM_LOG_ASSERT(!varInfoIndices.empty() && varInfoIndices.back() == index, "Could not find a basic variable for replacement of array variable " << replacedVar->getExpressionVariable().getName() << " ."); } 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)); } } diff --git a/src/storm/storage/jani/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp index 114e8ef3a..d3d7d47fb 100644 --- a/src/storm/storage/jani/ArrayEliminator.cpp +++ b/src/storm/storage/jani/ArrayEliminator.cpp @@ -569,6 +569,15 @@ namespace storm { }; } // namespace detail + storm::expressions::Expression ArrayEliminatorData::transformExpression(storm::expressions::Expression const& arrayExpression) const { + std::unordered_map arraySizes; + for (auto const& r : replacements) { + arraySizes.emplace(r.first, r.second.size()); + } + detail::ArrayExpressionEliminationVisitor eliminator(replacements, arraySizes); + return eliminator.eliminate(arrayExpression); + } + ArrayEliminatorData ArrayEliminator::eliminate(Model& model, bool keepNonTrivialArrayAccess) { auto sizes = detail::MaxArraySizeDeterminer().getMaxSizes(model); ArrayEliminatorData result = detail::ArrayVariableReplacer(model.getExpressionManager(), keepNonTrivialArrayAccess, sizes).replace(model); @@ -577,6 +586,7 @@ namespace storm { STORM_LOG_ASSERT(!containsArrayExpression(model), "the model still contains array expressions."); return result; } + } } diff --git a/src/storm/storage/jani/ArrayEliminator.h b/src/storm/storage/jani/ArrayEliminator.h index 4193d96fc..860aa37ea 100644 --- a/src/storm/storage/jani/ArrayEliminator.h +++ b/src/storm/storage/jani/ArrayEliminator.h @@ -11,12 +11,19 @@ namespace storm { struct ArrayEliminatorData { std::vector> eliminatedArrayVariables; std::unordered_map> replacements; + + // Transforms the given expression (which might contain array expressions) to an equivalent expression without array variables. + storm::expressions::Expression transformExpression(storm::expressions::Expression const& arrayExpression) const; }; class ArrayEliminator { public: ArrayEliminator() = default; + /*! + * Eliminates all array references in the given model by replacing them with basic variables. + */ + ArrayEliminatorData eliminate(Model& model, bool keepNonTrivialArrayAccess = false); private: