diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 588d0d330..131c6931e 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -644,7 +644,10 @@ namespace storm { template void processInputWithValueType(SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); + auto generalSettings = storm::settings::getModule(); + 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(input); } else { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 437631a3a..14da77296 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/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."); } diff --git a/src/storm/solver/GmmxxMultiplier.cpp b/src/storm/solver/GmmxxMultiplier.cpp index c652a136b..706ad795e 100644 --- a/src/storm/solver/GmmxxMultiplier.cpp +++ b/src/storm/solver/GmmxxMultiplier.cpp @@ -81,35 +81,39 @@ 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(); - currentValue += vect_sp(gmm::linalg_traits::row(itr), x); + --add_it; - if (choices) { - choice = *(row_group_it + 1) - 1 - *row_group_it; - *choice_it = choice; - } - - --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(); - newValue += vect_sp(gmm::linalg_traits::row(itr), x); + // 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::row(itr), x); if (choices) { - --choice; + choice = *(row_group_it + 1) - 1 - *row_group_it; + *choice_it = choice; } - if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { - currentValue = newValue; + --itr; + + 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(); + newValue += vect_sp(gmm::linalg_traits::row(itr), x); + if (choices) { - *choice_it = choice; + --choice; + } + + if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { + currentValue = newValue; + if (choices) { + *choice_it = choice; + } + } + if (b) { + --add_it; } } - if (b) { - --add_it; - } + } else if (choices) { + *choice_it = 0; } // Write back final value. @@ -161,28 +165,28 @@ namespace storm { auto resultIt = result.begin() + range.begin(); for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) { - T currentValue = vect_sp(gmm::linalg_traits>::row(itr), x, typename gmm::linalg_traits>::storage_type(), typename gmm::linalg_traits>::storage_type()); - if (b) { - currentValue += *bIt; - ++bIt; - } + T currentValue = b ? *bIt : storm::utility::zero(); + ++bIt; if (choices) { *choiceIt = 0; } - ++itr; - - for (auto itre = mat_row_const_begin(matrix) + *(groupIt + 1); itr != itre; ++itr) { - T newValue = vect_sp(gmm::linalg_traits>::row(itr), x, typename gmm::linalg_traits>::storage_type(), typename gmm::linalg_traits>::storage_type()); - if (b) { - newValue += *bIt; - ++bIt; - } + // Only multiply and reduce if the row group is not empty. + if (*groupIt != *(groupIt + 1)) { + ++itr; - if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { - currentValue = newValue; - if (choices) { - *choiceIt = std::distance(mat_row_const_begin(matrix), itr) - *groupIt; + for (auto itre = mat_row_const_begin(matrix) + *(groupIt + 1); itr != itre; ++itr) { + T newValue = vect_sp(gmm::linalg_traits>::row(itr), x, typename gmm::linalg_traits>::storage_type(), typename gmm::linalg_traits>::storage_type()); + if (b) { + newValue += *bIt; + ++bIt; + } + + if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { + currentValue = newValue; + if (choices) { + *choiceIt = std::distance(mat_row_const_begin(matrix), itr) - *groupIt; + } } } } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 99561bcfd..7acc811de 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/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::SolutionMethod::ValueIteration && this->getSettings().getForceSoundness()) { - requirements.requireNoEndComponents(); + 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 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* lowerX = &x; std::vector* upperX = this->auxiliaryRowGroupVector.get(); std::vector* tmp; diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index 30fe62228..6402f6046 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -436,6 +436,10 @@ namespace storm { std::vector* lowerX = &x; if (!this->cachedRowVector) { this->cachedRowVector = std::make_unique>(getMatrixRowCount(), this->getUpperBound()); + } else { + for (auto& e : *this->cachedRowVector) { + e = this->getUpperBound(); + } } std::vector* upperX = this->cachedRowVector.get(); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index e2e15b7bc..119d54bf5 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1523,33 +1523,37 @@ namespace storm { for (auto resultIt = result.begin(), resultIte = result.end(); resultIt != resultIte; ++resultIt, ++choiceIt, ++rowGroupIt) { ValueType currentValue = summand ? *summandIt : storm::utility::zero(); - - for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { - currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; - } + ++summandIt; if (choices) { *choiceIt = 0; } - ++rowIt; - if (summand) { - ++summandIt; - } - - for (; static_cast(std::distance(rowIndications.begin(), rowIt)) < *(rowGroupIt + 1); ++rowIt) { - ValueType newValue = summand ? *summandIt : storm::utility::zero(); + // 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) { - newValue += elementIt->getValue() * vector[elementIt->getColumn()]; + currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; + } + if (choices) { + *choiceIt = 0; } - if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { - currentValue = newValue; - if (choices) { - *choiceIt = std::distance(rowIndications.begin(), rowIt) - *rowGroupIt; + ++rowIt; + + for (; static_cast(std::distance(rowIndications.begin(), rowIt)) < *(rowGroupIt + 1); ++rowIt) { + ValueType newValue = summand ? *summandIt : storm::utility::zero(); + for (auto elementIte = this->begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { + newValue += elementIt->getValue() * vector[elementIt->getColumn()]; + } + + if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { + currentValue = newValue; + if (choices) { + *choiceIt = std::distance(rowIndications.begin(), rowIt) - *rowGroupIt; + } + } + if (summand) { + ++summandIt; } - } - if (summand) { - ++summandIt; } } @@ -1581,34 +1585,37 @@ namespace storm { for (auto resultIt = result.end() - 1, resultIte = result.begin() - 1; resultIt != resultIte; --resultIt, --choiceIt, --rowGroupIt) { ValueType currentValue = summand ? *summandIt : storm::utility::zero(); + --summandIt; - for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) { - currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; - } - if (choices) { - *choiceIt = std::distance(rowIndications.begin(), rowIt) - *rowGroupIt; - } - - --rowIt; - if (summand) { - --summandIt; - } - - for (uint64_t i = *rowGroupIt + 1, end = *(rowGroupIt + 1); i < end; --rowIt, ++i) { - ValueType newValue = summand ? *summandIt : storm::utility::zero(); + // 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) { - newValue += elementIt->getValue() * vector[elementIt->getColumn()]; + currentValue += elementIt->getValue() * vector[elementIt->getColumn()]; } - - if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { - currentValue = newValue; - if (choices) { - *choiceIt = std::distance(rowIndications.begin(), rowIt) - *rowGroupIt; - } + if (choices) { + *choiceIt = std::distance(rowIndications.begin(), rowIt) - *rowGroupIt; } - if (summand) { - --summandIt; + + --rowIt; + + for (uint64_t i = *rowGroupIt + 1, end = *(rowGroupIt + 1); i < end; --rowIt, ++i) { + ValueType newValue = summand ? *summandIt : storm::utility::zero(); + for (auto elementIte = this->begin() + *rowIt - 1; elementIt != elementIte; --elementIt) { + newValue += elementIt->getValue() * vector[elementIt->getColumn()]; + } + + if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { + currentValue = newValue; + if (choices) { + *choiceIt = std::distance(rowIndications.begin(), rowIt) - *rowGroupIt; + } + } + if (summand) { + --summandIt; + } } + } else if (choices) { + *choiceIt = 0; } // Finally write value to target vector. @@ -1654,27 +1661,30 @@ namespace storm { for (; groupIt != groupIte; ++groupIt, ++resultIt, ++choiceIt) { ValueType currentValue = summand ? *summandIt : storm::utility::zero(); - - for (auto elementIte = columnsAndEntries.begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { - currentValue += elementIt->getValue() * x[elementIt->getColumn()]; - } + ++summandIt; if (choices) { *choiceIt = 0; } - ++rowIt; - ++summandIt; - - for (; static_cast(std::distance(rowIndications.begin(), rowIt)) < *(groupIt + 1); ++rowIt, ++summandIt) { - ValueType newValue = summand ? *summandIt : storm::utility::zero(); + // 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) { - newValue += elementIt->getValue() * x[elementIt->getColumn()]; + currentValue += elementIt->getValue() * x[elementIt->getColumn()]; } - if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { - currentValue = newValue; - if (choices) { - *choiceIt = std::distance(rowIndications.begin(), rowIt) - *groupIt; + ++rowIt; + + for (; static_cast(std::distance(rowIndications.begin(), rowIt)) < *(groupIt + 1); ++rowIt, ++summandIt) { + ValueType newValue = summand ? *summandIt : storm::utility::zero(); + for (auto elementIte = columnsAndEntries.begin() + *(rowIt + 1); elementIt != elementIte; ++elementIt) { + newValue += elementIt->getValue() * x[elementIt->getColumn()]; + } + + if ((dir == OptimizationDirection::Minimize && newValue < currentValue) || (dir == OptimizationDirection::Maximize && newValue > currentValue)) { + currentValue = newValue; + if (choices) { + *choiceIt = std::distance(rowIndications.begin(), rowIt) - *groupIt; + } } } } diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 88860c072..4aa684557 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -627,36 +627,24 @@ 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; - if (choices != nullptr) { - *choiceIt = 0; - } - - for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) { - if (f(*sourceIt, *targetIt)) { - *targetIt = *sourceIt; - if (choices != nullptr) { - *choiceIt = localChoice; - } + *targetIt = *sourceIt; + ++sourceIt; + localChoice = 1; + if (choices != nullptr) { + *choiceIt = 0; + } + + for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) { + if (f(*sourceIt, *targetIt)) { + *targetIt = *sourceIt; + if (choices != nullptr) { + *choiceIt = localChoice; } } - - 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; - } + } + + if (choices != nullptr) { + ++choiceIt; } } } @@ -695,34 +683,22 @@ 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; - if (choices != nullptr) { - *choiceIt = 0; - } - for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) { - if (f(*sourceIt, *targetIt)) { - *targetIt = *sourceIt; - if (choices != nullptr) { - *choiceIt = localChoice; - } + *targetIt = *sourceIt; + ++sourceIt; + localChoice = 1; + if (choices != nullptr) { + *choiceIt = 0; + } + for (sourceIte = source.begin() + *(rowGroupingIt + 1); sourceIt != sourceIte; ++sourceIt, ++localChoice) { + if (f(*sourceIt, *targetIt)) { + *targetIt = *sourceIt; + if (choices != nullptr) { + *choiceIt = localChoice; } } - 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; - } + } + if (choices != nullptr) { + ++choiceIt; } } }