Browse Source

Respected whether the linear equation solver wants the fix point or eq sys formulation

tempestpy_adaptions
TimQu 7 years ago
parent
commit
fb21ffca63
  1. 7
      src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp
  2. 7
      src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp
  3. 11
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp
  4. 1
      src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp

7
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<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true);
linEqMatrix.convertToEquationSystem();
bool needEquationSystem = linEq.factory->getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, needEquationSystem);
if (needEquationSystem) {
linEqMatrix.convertToEquationSystem();
}
linEq.solver = linEq.factory->create(std::move(linEqMatrix));
linEq.solver->setCachingEnabled(true);
}

7
src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@ -133,9 +133,12 @@ namespace storm {
swAux2.start();
++numSchedChanges;
cachedData.schedulerChoices = choices;
storm::storage::SparseMatrix<ValueType> subMatrix = epochModel.epochMatrix.selectRowsFromRowGroups(choices, true);
subMatrix.convertToEquationSystem();
storm::solver::GeneralLinearEquationSolverFactory<ValueType> linEqSolverFactory;
bool needEquationSystem = linEqSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> subMatrix = epochModel.epochMatrix.selectRowsFromRowGroups(choices, needEquationSystem);
if (needEquationSystem) {
subMatrix.convertToEquationSystem();
}
cachedData.linEqSolver = linEqSolverFactory.create(std::move(subMatrix));
cachedData.linEqSolver->setCachingEnabled(true);
swAux2.stop();

11
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@ -248,11 +248,14 @@ namespace storm {
objectiveResults[objIndex].resize(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
if (!maybeStates.empty()) {
bool needEquationSystem = linearEquationSolverFactory.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
storm::storage::SparseMatrix<ValueType> 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<ValueType> x = storm::utility::vector::filterVector(objectiveResults[objIndex], maybeStates);

1
src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp

@ -333,6 +333,7 @@ namespace storm {
}
}
}
assert(!firstSuccessor);
*stepSolIt = std::move(choiceSolution);
++stepSolIt;
}

Loading…
Cancel
Save