From fb21ffca6344f4e88137e0838f5a0cde857329c7 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 6 Oct 2017 15:08:50 +0200 Subject: [PATCH] Respected whether the linear equation solver wants the fix point or eq sys formulation --- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 7 +++++-- .../SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp | 7 +++++-- .../pcaa/SparsePcaaWeightVectorChecker.cpp | 11 +++++++---- .../rewardbounded/MultiDimensionalRewardUnfolding.cpp | 1 + 4 files changed, 18 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 61f995939..69ab6cb23 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -376,8 +376,11 @@ namespace storm { if (linEq.solver == nullptr || newChoices != optimalChoicesAtCurrentEpoch) { optimalChoicesAtCurrentEpoch = newChoices; linEq.solver = nullptr; - storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); - linEqMatrix.convertToEquationSystem(); + bool needEquationSystem = linEq.factory->getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, needEquationSystem); + if (needEquationSystem) { + linEqMatrix.convertToEquationSystem(); + } linEq.solver = linEq.factory->create(std::move(linEqMatrix)); linEq.solver->setCachingEnabled(true); } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 3b46b28b3..59e6a1ff1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -133,9 +133,12 @@ namespace storm { swAux2.start(); ++numSchedChanges; cachedData.schedulerChoices = choices; - storm::storage::SparseMatrix subMatrix = epochModel.epochMatrix.selectRowsFromRowGroups(choices, true); - subMatrix.convertToEquationSystem(); storm::solver::GeneralLinearEquationSolverFactory linEqSolverFactory; + bool needEquationSystem = linEqSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; + storm::storage::SparseMatrix subMatrix = epochModel.epochMatrix.selectRowsFromRowGroups(choices, needEquationSystem); + if (needEquationSystem) { + subMatrix.convertToEquationSystem(); + } cachedData.linEqSolver = linEqSolverFactory.create(std::move(subMatrix)); cachedData.linEqSolver->setCachingEnabled(true); swAux2.stop(); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 1b5b51937..bd9045794 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -248,11 +248,14 @@ namespace storm { objectiveResults[objIndex].resize(transitionMatrix.getRowGroupCount(), storm::utility::zero()); if (!maybeStates.empty()) { + bool needEquationSystem = linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem; storm::storage::SparseMatrix submatrix = deterministicMatrix.getSubmatrix( - true, maybeStates, maybeStates, true); - // Converting the matrix from the fixpoint notation to the form needed for the equation - // system. That is, we go from x = A*x + b to (I-A)x = b. - submatrix.convertToEquationSystem(); + true, maybeStates, maybeStates, needEquationSystem); + if (needEquationSystem) { + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. + submatrix.convertToEquationSystem(); + } // Prepare solution vector and rhs of the equation system. std::vector x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates); diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 98f71093e..2925c33d4 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -333,6 +333,7 @@ namespace storm { } } } + assert(!firstSuccessor); *stepSolIt = std::move(choiceSolution); ++stepSolIt; }