diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index d03e356ac..f4c8a0f2f 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -74,7 +74,7 @@ namespace storm { bool IterativeMinMaxLinearEquationSolverSettings::getRelativeTerminationCriterion() const { return relative; } - + template IterativeMinMaxLinearEquationSolver::IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings) : StandardMinMaxLinearEquationSolver(A, std::move(linearEquationSolverFactory)), settings(settings) { // Intentionally left empty. @@ -103,18 +103,18 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { // Create the initial scheduler. - std::vector scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector(this->A.getRowGroupCount()); + std::vector scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector(this->A->getRowGroupCount()); // Get a vector for storing the right-hand side of the inner equation system. if(!auxiliaryRowGroupVector) { - auxiliaryRowGroupVector = std::make_unique>(this->A.getRowGroupCount()); + auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } std::vector& subB = *auxiliaryRowGroupVector; // Resolve the nondeterminism according to the current scheduler. - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(scheduler, true); + storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(scheduler, true); submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(subB, scheduler, this->A->getRowGroupIndices(), b); // Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration. auto solver = this->linearEquationSolverFactory->create(std::move(submatrix)); @@ -137,17 +137,17 @@ namespace storm { // Go through the multiplication result and see whether we can improve any of the choices. bool schedulerImproved = false; - for (uint_fast64_t group = 0; group < this->A.getRowGroupCount(); ++group) { + for (uint_fast64_t group = 0; group < this->A->getRowGroupCount(); ++group) { uint_fast64_t currentChoice = scheduler[group]; - for (uint_fast64_t choice = this->A.getRowGroupIndices()[group]; choice < this->A.getRowGroupIndices()[group + 1]; ++choice) { + for (uint_fast64_t choice = this->A->getRowGroupIndices()[group]; choice < this->A->getRowGroupIndices()[group + 1]; ++choice) { // If the choice is the currently selected one, we can skip it. - if (choice - this->A.getRowGroupIndices()[group] == currentChoice) { + if (choice - this->A->getRowGroupIndices()[group] == currentChoice) { continue; } // Create the value of the choice. ValueType choiceValue = storm::utility::zero(); - for (auto const& entry : this->A.getRow(choice)) { + for (auto const& entry : this->A->getRow(choice)) { choiceValue += entry.getValue() * x[entry.getColumn()]; } choiceValue += b[choice]; @@ -157,7 +157,7 @@ namespace storm { // only changing the scheduler if the values are not equal (modulo precision) would make this unsound. if (valueImproved(dir, x[group], choiceValue)) { schedulerImproved = true; - scheduler[group] = choice - this->A.getRowGroupIndices()[group]; + scheduler[group] = choice - this->A->getRowGroupIndices()[group]; x[group] = std::move(choiceValue); } } @@ -168,9 +168,9 @@ namespace storm { status = Status::Converged; } else { // Update the scheduler and the solver. - submatrix = this->A.selectRowsFromRowGroups(scheduler, true); + submatrix = this->A->selectRowsFromRowGroups(scheduler, true); submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(subB, scheduler, this->A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(subB, scheduler, this->A->getRowGroupIndices(), b); solver->setMatrix(std::move(submatrix)); } @@ -215,24 +215,24 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::solveEquationsValueIteration(OptimizationDirection dir, std::vector& x, std::vector const& b) const { if(!this->linEqSolverA) { - this->linEqSolverA = this->linearEquationSolverFactory->create(this->A); + this->linEqSolverA = this->linearEquationSolverFactory->create(*this->A); this->linEqSolverA->setCachingEnabled(true); } if (!this->auxiliaryRowVector) { - this->auxiliaryRowVector = std::make_unique>(this->A.getRowCount()); + this->auxiliaryRowVector = std::make_unique>(this->A->getRowCount()); } std::vector& multiplyResult = *this->auxiliaryRowVector; if (!auxiliaryRowGroupVector) { - auxiliaryRowGroupVector = std::make_unique>(this->A.getRowGroupCount()); + auxiliaryRowGroupVector = std::make_unique>(this->A->getRowGroupCount()); } if (this->hasSchedulerHint()) { // Resolve the nondeterminism according to the scheduler hint - storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->choicesHint.get(), true); + storm::storage::SparseMatrix submatrix = this->A->selectRowsFromRowGroups(this->choicesHint.get(), true); submatrix.convertToEquationSystem(); - storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A->getRowGroupIndices(), b); // Solve the resulting equation system. // Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision. @@ -256,7 +256,7 @@ namespace storm { this->linEqSolverA->multiply(*currentX, &b, multiplyResult); // Reduce the vector x' by applying min/max for all non-deterministic choices. - storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A.getRowGroupIndices()); + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, *newX, this->A->getRowGroupIndices()); // Determine whether the method converged. if (storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion())) { @@ -284,9 +284,9 @@ namespace storm { if (iterations==0) { this->linEqSolverA->multiply(x, &b, multiplyResult); } - this->schedulerChoices = std::vector(this->A.getRowGroupCount()); + this->schedulerChoices = std::vector(this->A->getRowGroupCount()); // Reduce the multiplyResult and keep track of the choices made - storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices(), &this->schedulerChoices.get()); + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A->getRowGroupIndices(), &this->schedulerChoices.get()); } if (!this->isCachingEnabled()) { @@ -298,7 +298,7 @@ namespace storm { template bool IterativeMinMaxLinearEquationSolver::solveEquationsAcyclic(OptimizationDirection dir, std::vector& x, std::vector const& b) const { - uint64_t numGroups = this->A.getRowGroupCount(); + uint64_t numGroups = this->A->getRowGroupCount(); // Allocate memory for the scheduler (if required) if (this->isTrackSchedulerSet()) { @@ -323,7 +323,7 @@ namespace storm { } } - auto transposedMatrix = this->A.transpose(true); + auto transposedMatrix = this->A->transpose(true); // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value. storm::storage::BitVector processedGroups(numGroups, false); @@ -338,7 +338,7 @@ namespace storm { // Check if the candidate row group has an unprocessed successor bool hasUnprocessedSuccessor = false; - for (auto const& entry : this->A.getRowGroup(candidate)) { + for (auto const& entry : this->A->getRowGroup(candidate)) { if (!processedGroups.get(entry.getColumn())) { hasUnprocessedSuccessor = true; break; @@ -375,17 +375,17 @@ namespace storm { template void IterativeMinMaxLinearEquationSolver::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector& x, std::vector const& b, uint_fast64_t* choice) const { - uint64_t row = this->A.getRowGroupIndices()[group]; - uint64_t groupEnd = this->A.getRowGroupIndices()[group + 1]; + uint64_t row = this->A->getRowGroupIndices()[group]; + uint64_t groupEnd = this->A->getRowGroupIndices()[group + 1]; assert(row != groupEnd); auto bIt = b.begin() + row; ValueType& xi = x[group]; - xi = this->A.multiplyRowWithVector(row, x) + *bIt; + xi = this->A->multiplyRowWithVector(row, x) + *bIt; uint64_t optimalRow = row; for (++row, ++bIt; row < groupEnd; ++row, ++bIt) { - ValueType choiceVal = this->A.multiplyRowWithVector(row, x) + *bIt; + ValueType choiceVal = this->A->multiplyRowWithVector(row, x) + *bIt; if (minimize(dir)) { if (choiceVal < xi) { xi = choiceVal; @@ -399,7 +399,7 @@ namespace storm { } } if (choice != nullptr) { - *choice = optimalRow - this->A.getRowGroupIndices()[group]; + *choice = optimalRow - this->A->getRowGroupIndices()[group]; } } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h index e197f88b0..23d34cd7c 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.h +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.h @@ -36,6 +36,7 @@ namespace storm { template class IterativeMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { public: + IterativeMinMaxLinearEquationSolver() = default; IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings = IterativeMinMaxLinearEquationSolverSettings()); IterativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, IterativeMinMaxLinearEquationSolverSettings const& settings = IterativeMinMaxLinearEquationSolverSettings()); diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 35de0902d..9b52a1fa9 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -28,8 +28,8 @@ namespace storm { // Create a variable for each row group std::vector variables; - variables.reserve(this->A.getRowGroupCount()); - for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { + variables.reserve(this->A->getRowGroupCount()); + for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) { if (this->lowerBound) { if (this->upperBound) { variables.push_back(solver->addBoundedContinuousVariable("x" + std::to_string(rowGroup), this->lowerBound.get(), this->upperBound.get(), storm::utility::one())); @@ -47,10 +47,10 @@ namespace storm { solver->update(); // Add a constraint for each row - for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { - for (uint64_t row = this->A.getRowGroupIndices()[rowGroup]; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row) { + for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) { + for (uint64_t row = this->A->getRowGroupIndices()[rowGroup]; row < this->A->getRowGroupIndices()[rowGroup + 1]; ++row) { storm::expressions::Expression rowConstraint = solver->getConstant(b[row]); - for (auto const& entry : this->A.getRow(row)) { + for (auto const& entry : this->A->getRow(row)) { rowConstraint = rowConstraint + (solver->getConstant(entry.getValue()) * variables[entry.getColumn()].getExpression()); } if (minimize(dir)) { @@ -78,14 +78,14 @@ namespace storm { // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { - this->schedulerChoices = std::vector(this->A.getRowGroupCount()); - for (uint64_t rowGroup = 0; rowGroup < this->A.getRowGroupCount(); ++rowGroup) { - uint64_t row = this->A.getRowGroupIndices()[rowGroup]; + this->schedulerChoices = std::vector(this->A->getRowGroupCount()); + for (uint64_t rowGroup = 0; rowGroup < this->A->getRowGroupCount(); ++rowGroup) { + uint64_t row = this->A->getRowGroupIndices()[rowGroup]; uint64_t optimalChoiceIndex = 0; uint64_t currChoice = 0; - ValueType optimalGroupValue = this->A.multiplyRowWithVector(row, x) + b[row]; - for (++row, ++currChoice; row < this->A.getRowGroupIndices()[rowGroup + 1]; ++row, ++currChoice) { - ValueType rowValue = this->A.multiplyRowWithVector(row, x) + b[row]; + ValueType optimalGroupValue = this->A->multiplyRowWithVector(row, x) + b[row]; + for (++row, ++currChoice; row < this->A->getRowGroupIndices()[rowGroup + 1]; ++row, ++currChoice) { + ValueType rowValue = this->A->multiplyRowWithVector(row, x) + b[row]; if ((minimize(dir) && rowValue < optimalGroupValue) || (maximize(dir) && rowValue > optimalGroupValue)) { optimalGroupValue = rowValue; optimalChoiceIndex = currChoice; diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.h b/src/storm/solver/LpMinMaxLinearEquationSolver.h index 540fe89c1..84d744c39 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.h +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.h @@ -10,6 +10,7 @@ namespace storm { template class LpMinMaxLinearEquationSolver : public StandardMinMaxLinearEquationSolver { public: + LpMinMaxLinearEquationSolver() = default; LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); LpMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory, std::unique_ptr>&& lpSolverFactory); @@ -21,7 +22,7 @@ namespace storm { std::unique_ptr> lpSolverFactory; }; - template + template class LpMinMaxLinearEquationSolverFactory : public StandardMinMaxLinearEquationSolverFactory { public: LpMinMaxLinearEquationSolverFactory(bool trackScheduler = false); diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp index 6b0f140ce..5fedfced4 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp @@ -15,24 +15,29 @@ namespace storm { namespace solver { template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(A) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver() : A(nullptr) { // Intentionally left empty. } template - StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique>(std::move(A))), A(*localA) { + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(nullptr), A(&A) { + // Intentionally left empty. + } + + template + StandardMinMaxLinearEquationSolver::StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory) : linearEquationSolverFactory(std::move(linearEquationSolverFactory)), localA(std::make_unique>(std::move(A))), A(localA.get()) { // Intentionally left empty. } template void StandardMinMaxLinearEquationSolver::repeatedMultiply(OptimizationDirection dir, std::vector& x, std::vector const* b, uint_fast64_t n) const { if (!linEqSolverA) { - linEqSolverA = linearEquationSolverFactory->create(A); + linEqSolverA = linearEquationSolverFactory->create(*A); linEqSolverA->setCachingEnabled(true); } if (!auxiliaryRowVector) { - auxiliaryRowVector = std::make_unique>(A.getRowCount()); + auxiliaryRowVector = std::make_unique>(A->getRowCount()); } std::vector& multiplyResult = *auxiliaryRowVector; @@ -41,7 +46,7 @@ namespace storm { // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. - storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A.getRowGroupIndices()); + storm::utility::vector::reduceVectorMinOrMax(dir, multiplyResult, x, this->A->getRowGroupIndices()); } if (!this->isCachingEnabled()) { diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.h b/src/storm/solver/StandardMinMaxLinearEquationSolver.h index 1305f3e26..b122489c8 100644 --- a/src/storm/solver/StandardMinMaxLinearEquationSolver.h +++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.h @@ -9,6 +9,8 @@ namespace storm { template class StandardMinMaxLinearEquationSolver : public MinMaxLinearEquationSolver { public: + StandardMinMaxLinearEquationSolver(); + StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, std::unique_ptr>&& linearEquationSolverFactory); StandardMinMaxLinearEquationSolver(storm::storage::SparseMatrix&& A, std::unique_ptr>&& linearEquationSolverFactory); @@ -33,7 +35,7 @@ namespace storm { // A reference to the original sparse matrix given to this solver. If the solver takes posession of the matrix // the reference refers to localA. - storm::storage::SparseMatrix const& A; + storm::storage::SparseMatrix const* A; };