diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index 6c5756c1a..ce25ecc50 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -95,10 +95,10 @@ namespace storm { } } else { // We will use Policy Iteration to solve the given system. - // We first define an initial choice resolution which will be refined after each iteration. + // We first guess an initial choice resolution which will be refined after each iteration. std::vector::index_type> choiceVector(rowGroupIndices.size() - 1); - // Create our own multiplyResult for solving the deterministic instances. + // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(rowGroupIndices.size() - 1); std::vector subB(rowGroupIndices.size() - 1); @@ -142,6 +142,7 @@ namespace storm { gmm::add(b, *multiplyResult); // Reduce the vector x by applying min/max over all nondeterministic choices. + // Here, we capture which choice was taken in each state, thereby refining our initial guess. if (minimize) { storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, rowGroupIndices, &choiceVector); } else { diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index a33b7e869..b741a1836 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -93,13 +93,14 @@ namespace storm { } } else { // We will use Policy Iteration to solve the given system. - // We first define an initial choice resolution which will be refined after each iteration. + // We first guess an initial choice resolution which will be refined after each iteration. std::vector::index_type> choiceVector(A.getRowGroupIndices().size() - 1); - // Create our own multiplyResult for solving the deterministic instances. + // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(A.getRowGroupIndices().size() - 1); std::vector subB(A.getRowGroupIndices().size() - 1); + // Check whether intermediate storage was provided and create it otherwise. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { multiplyResult = new std::vector(b.size()); @@ -132,7 +133,7 @@ namespace storm { // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); - // Solve the resulting linear equation system + // Solve the resulting linear equation system of the sub-instance for x under the current choices nativeLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult); // Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration. @@ -140,6 +141,7 @@ namespace storm { storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); // Reduce the vector x by applying min/max over all nondeterministic choices. + // Here, we capture which choice was taken in each state, thereby refining our initial guess. if (minimize) { storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, A.getRowGroupIndices(), &choiceVector); } else {