From 21aabc5b05d281fb14453eaea897a24634e5d130 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 10 Sep 2018 12:44:56 +0200 Subject: [PATCH] fixing treatment of zero-states in game solver causing problems in policy iteration and non-unique solutions --- src/storm/solver/StandardGameSolver.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp index 7661392ca..f0ef60564 100644 --- a/src/storm/solver/StandardGameSolver.cpp +++ b/src/storm/solver/StandardGameSolver.cpp @@ -159,14 +159,16 @@ namespace storm { targetStates = storm::utility::vector::filterGreaterZero(subB); zeroStates = ~storm::utility::graph::performProbGreater0(submatrix.transpose(), storm::storage::BitVector(targetStates.size(), true), targetStates); } + bool asEquationSystem = false; if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) { submatrix.convertToEquationSystem(); + asEquationSystem = true; } if (!this->hasUniqueSolution()) { for (auto state : zeroStates) { for (auto& element : submatrix.getRow(state)) { if (element.getColumn() == state) { - element.setValue(storm::utility::one()); + element.setValue(asEquationSystem ? storm::utility::one() : storm::utility::zero()); } else { element.setValue(storm::utility::zero()); } @@ -177,7 +179,6 @@ namespace storm { auto submatrixSolver = linearEquationSolverFactory->create(environmentOfSolver, std::move(submatrix)); if (this->lowerBound) { submatrixSolver->setLowerBound(this->lowerBound.get()); - } if (this->upperBound) { submatrixSolver->setUpperBound(this->upperBound.get()); @@ -211,7 +212,7 @@ namespace storm { for (auto state : zeroStates) { for (auto& element : submatrix.getRow(state)) { if (element.getColumn() == state) { - element.setValue(storm::utility::one()); + element.setValue(asEquationSystem ? storm::utility::one() : storm::utility::zero()); } else { element.setValue(storm::utility::zero()); }