fixes for arrays

src/storm-parsers/parser/JaniParser.cpp

@@ -788,12 +788,17 @@ namespace storm {
                 if (setInitValFromDefault) {
                     initVal = storm::expressions::ValueArrayExpression(*expressionManager, exprVariableType, {}).toExpression();
                 }
+                std::shared_ptr<storm::jani::ArrayVariable> 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<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType, initVal.get(), transientVar);
+                    result = std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType, initVal.get(), transientVar);
                 } else {
-                    return std::make_shared<storm::jani::ArrayVariable>(name, expressionManager->declareArrayVariable(exprManagerName, exprVariableType.getElementType()), elementType);
+                    result = std::make_shared<storm::jani::ArrayVariable>(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 << ")");

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<ValueType> stateActionRewards(rewardVariables.size(), storm::utility::zero<ValueType>());
-
+                currentDistribution.clear();
                 currentDistribution.add(state, storm::utility::one<ValueType>());
+                nextDistribution.clear();
                 
                 EdgeIndexSet edgeIndices;
                 uint64_t assignmentLevel = std::numeric_limits<uint64_t>::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<storm::expressions::Variable, storm::expressions::Expression> 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);
                     }
                 }
             }

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));
             }
         }

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<storm::expressions::Variable, std::size_t> 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;
         }
+        
     }
 }
 

src/storm/storage/jani/ArrayEliminator.h

@@ -11,12 +11,19 @@ namespace storm {
         struct ArrayEliminatorData {
             std::vector<std::shared_ptr<ArrayVariable>> eliminatedArrayVariables;
             std::unordered_map<storm::expressions::Variable, std::vector<storm::jani::Variable const*>> 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: