fixed multiply-reduce operations in the presence of empty row groups

src/storm-cli-utilities/model-handling.h

@@ -644,6 +644,9 @@ namespace storm {
         template <typename ValueType>
         void processInputWithValueType(SymbolicInput const& input) {
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+            auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+
+            STORM_LOG_THROW(!generalSettings.isSoundSet() || coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::NotSupportedException, "Forcing soundness is not supported for engines other than the sparse engine.");
             
             if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) {
                 processInputWithValueTypeAndDdlib<storm::dd::DdType::CUDD, ValueType>(input);

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -209,6 +209,9 @@ namespace storm {
                         result.schedulerHint = computeValidSchedulerHint(type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates);
                         requirements.clearValidInitialScheduler();
                     }
+                    if (type == storm::solver::EquationSystemType::UntilProbabilities) {
+                        requirements.clearGlobalUpperBound();
+                    }
                     STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver.");
                 }
 

src/storm/solver/GmmxxMultiplier.cpp

@@ -81,6 +81,10 @@ namespace storm {
             uint64_t choice;
             for (auto row_group_it = rowGroupIndices.end() - 2, row_group_ite = rowGroupIndices.begin() - 1; row_group_it != row_group_ite; --row_group_it, --choice_it, --target_it) {
                 T currentValue = b ? *add_it : storm::utility::zero<T>();
+                --add_it;
+                
+                // Only multiply and reduce if the row group is not empty.
+                if (*row_group_it != *(row_group_it + 1)) {
                     currentValue += vect_sp(gmm::linalg_traits<MatrixType>::row(itr), x);
                     
                     if (choices) {
@@ -89,9 +93,6 @@ namespace storm {
                     }
                     
                     --itr;
-                if (b) {
-                    --add_it;
-                }
                     
                     for (uint64_t row = *row_group_it + 1, rowEnd = *(row_group_it + 1); row < rowEnd; ++row, --itr) {
                         T newValue = b ? *add_it : storm::utility::zero<T>();
@@ -111,6 +112,9 @@ namespace storm {
                             --add_it;
                         }
                     }
+                } else if (choices) {
+                    *choice_it = 0;
+                }
                 
                 // Write back final value.
                 *target_it = currentValue;
@@ -161,15 +165,14 @@ namespace storm {
                 auto resultIt = result.begin() + range.begin();
 
                 for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) {
-                    T currentValue = vect_sp(gmm::linalg_traits<gmm::csr_matrix<T>>::row(itr), x, typename gmm::linalg_traits<gmm::csr_matrix<T>>::storage_type(), typename gmm::linalg_traits<std::vector<T>>::storage_type());
-                    if (b) {
-                        currentValue += *bIt;
+                    T currentValue = b ? *bIt : storm::utility::zero<T>();
                     ++bIt;
-                    }
                     if (choices) {
                         *choiceIt = 0;
                     }
                     
+                    // Only multiply and reduce if the row group is not empty.
+                    if (*groupIt != *(groupIt + 1)) {
                         ++itr;
                         
                         for (auto itre = mat_row_const_begin(matrix) + *(groupIt + 1); itr != itre; ++itr) {
@@ -186,6 +189,7 @@ namespace storm {
                                 }
                             }
                         }
+                    }
                     
                     *resultIt = currentValue;
                 }

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -253,7 +253,9 @@ namespace storm {
             
             // If we will use sound value iteration, we require no ECs and an upper bound.
             if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->getSettings().getForceSoundness()) {
+                if (!direction || direction.get() == OptimizationDirection::Maximize) {
                     requirements.requireNoEndComponents();
+                }
                 requirements.requireGlobalUpperBound();
             }
             
@@ -375,6 +377,7 @@ namespace storm {
             }
             
             if (this->hasInitialScheduler()) {
+                STORM_LOG_TRACE("Solving initial scheduler hint.");
                 // Resolve the nondeterminism according to the initial scheduler.
                 bool convertToEquationSystem = this->linearEquationSolverFactory->getEquationProblemFormat() == LinearEquationSolverProblemFormat::EquationSystem;
                 storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), convertToEquationSystem);
@@ -398,6 +401,11 @@ namespace storm {
             // Allow aliased multiplications.
             bool useGaussSeidelMultiplication = this->linEqSolverA->supportsGaussSeidelMultiplication() && settings.getValueIterationMultiplicationStyle() == storm::solver::MultiplicationStyle::GaussSeidel;
             
+            // Initialize upper bound vector.
+            for (auto& e : *this->auxiliaryRowGroupVector) {
+                e = this->getUpperBound();
+            }
+            
             std::vector<ValueType>* lowerX = &x;
             std::vector<ValueType>* upperX = this->auxiliaryRowGroupVector.get();
             std::vector<ValueType>* tmp;

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -436,6 +436,10 @@ namespace storm {
             std::vector<ValueType>* lowerX = &x;
             if (!this->cachedRowVector) {
                 this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount(), this->getUpperBound());
+            } else {
+                for (auto& e : *this->cachedRowVector) {
+                    e = this->getUpperBound();
+                }
             }
             std::vector<ValueType>* upperX = this->cachedRowVector.get();
             

src/storm/storage/SparseMatrix.cpp

@@ -1523,7 +1523,13 @@ namespace storm {
             
             for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++choiceIt, ++rowGroupIt) {
                 ValueType currentValue = summand ? *summandIt : storm::utility::zero<ValueType>();
+                ++summandIt;
+                if (choices) {
+                    *choiceIt = 0;
+                }
                 
+                // Only multiply and reduce if there is at least one row in the group.
+                if (*rowGroupIt < *(rowGroupIt + 1)) {
                     for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) {
                         currentValue += elementIt->getValue() * vector[elementIt->getColumn()];
                     }
@@ -1532,9 +1538,6 @@ namespace storm {
                     }
                     
                     ++rowIt;
-                if (summand) {
-                    ++summandIt;
-                }
                     
                     for (; static_cast<uint_fast64_t>(std::distance(rowIndications.begin(), rowIt)) < *(rowGroupIt + 1); ++rowIt) {
                         ValueType newValue = summand ? *summandIt : storm::utility::zero<ValueType>();
@@ -1552,6 +1555,7 @@ namespace storm {
                             ++summandIt;
                         }
                     }
+                }
                 
                 // Finally write value to target vector.
                 *resultIt = currentValue;
@@ -1581,7 +1585,10 @@ namespace storm {
             
             for (auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt) {
                 ValueType currentValue = summand ? *summandIt : storm::utility::zero<ValueType>();
+                --summandIt;
 
+                // Only multiply and reduce if there is at least one row in the group.
+                if (*rowGroupIt < *(rowGroupIt + 1)) {
                     for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) {
                         currentValue += elementIt->getValue() * vector[elementIt->getColumn()];
                     }
@@ -1590,9 +1597,6 @@ namespace storm {
                     }
                     
                     --rowIt;
-                if (summand) {
-                    --summandIt;
-                }
                     
                     for (uint64_t i = *rowGroupIt + 1, end = *(rowGroupIt + 1); i < end; --rowIt, ++i) {
                         ValueType newValue = summand ? *summandIt : storm::utility::zero<ValueType>();
@@ -1610,6 +1614,9 @@ namespace storm {
                             --summandIt;
                         }
                     }
+                } else if (choices) {
+                    *choiceIt = 0;
+                }
                 
                 // Finally write value to target vector.
                 *resultIt = currentValue;
@@ -1654,16 +1661,18 @@ namespace storm {
                 
                 for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) {
                     ValueType currentValue = summand ? *summandIt : storm::utility::zero<ValueType>();
+                    ++summandIt;
+                    if (choices) {
+                        *choiceIt = 0;
+                    }
                     
+                    // Only multiply and reduce if there is at least one row in the group.
+                    if (*groupIt < *(groupIt + 1)) {
                         for (auto elementIte = columnsAndEntries.begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) {
                             currentValue += elementIt->getValue() * x[elementIt->getColumn()];
                         }
-                    if (choices) {
-                        *choiceIt = 0;
-                    }
                         
                         ++rowIt;
-                    ++summandIt;
                         
                         for (; static_cast<uint_fast64_t>(std::distance(rowIndications.begin(), rowIt)) < *(groupIt + 1); ++rowIt, ++summandIt) {
                             ValueType newValue = summand ? *summandIt : storm::utility::zero<ValueType>();
@@ -1678,6 +1687,7 @@ namespace storm {
                                 }
                             }
                         }
+                    }
                     
                     // Finally write value to target vector.
                     *resultIt = currentValue;

src/storm/utility/vector.h

@@ -627,8 +627,6 @@ namespace storm {
                     }
                     
                     for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt) {
-                        // Only do work if the row group is not empty.
-                        if (*rowGroupingIt != *(rowGroupingIt + 1)) {
                         *targetIt = *sourceIt;
                         ++sourceIt;
                         localChoice = 1;
@@ -648,16 +646,6 @@ namespace storm {
                         if (choices != nullptr) {
                             ++choiceIt;
                         }
-                        } else {
-                            // Compensate for the 'wrong' move forward in the loop header.
-                            --targetIt;
-                            
-                            // Record dummy choice.
-                            if (choices != nullptr) {
-                                *choiceIt = 0;
-                                ++choiceIt;
-                            }
-                        }
                     }
                 }
                 
@@ -695,8 +683,6 @@ namespace storm {
                 }
                 
                 for (; targetIt != targetIte; ++targetIt, ++rowGroupingIt) {
-                    // Only do work if the row group is not empty.
-                    if (*rowGroupingIt != *(rowGroupingIt + 1)) {
                     *targetIt = *sourceIt;
                     ++sourceIt;
                     localChoice = 1;
@@ -714,16 +700,6 @@ namespace storm {
                     if (choices != nullptr) {
                         ++choiceIt;
                     }
-                    } else {
-                        // Compensate for the 'wrong' move forward in the loop header.
-                        --targetIt;
-                        
-                        // Record dummy choice.
-                        if (choices != nullptr) {
-                            *choiceIt = 0;
-                            ++choiceIt;
-                        }
-                    }
                 }
             }