From b73e2e5d1cb6c6731d62321b173d22591fc26df5 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Fri, 11 Dec 2020 18:48:23 +0100
Subject: [PATCH] Fixing steady state distribution computation.

---
 .../SparseDeterministicInfiniteHorizonHelper.cpp   | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
index a1db02872..96c642116 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
@@ -522,21 +522,25 @@ namespace storm {
                     storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
                     bool isEqSysFormat = linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem;
                     auto eqSysMatrix = this->_transitionMatrix.getSubmatrix(false, statesNotInComponent, statesNotInComponent, isEqSysFormat);
-                    std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, eqSysMatrix);
-                    solver->setLowerBound(storm::utility::zero<ValueType>());
+                    boost::optional<std::vector<ValueType>> upperBounds;
                     // Check solver requirements
-                    auto requirements = solver->getRequirements(env);
+                    auto requirements = linearEquationSolverFactory.getRequirements(env);
                     requirements.clearLowerBounds();
                     if (requirements.upperBounds()) {
                         auto toBsccProbabilities = this->_transitionMatrix.getConstrainedRowSumVector(statesNotInComponent, ~statesNotInComponent);
-                        solver->setUpperBounds(computeUpperBoundsForExpectedVisitingTimes(eqSysMatrix, toBsccProbabilities));
+                        upperBounds = computeUpperBoundsForExpectedVisitingTimes(eqSysMatrix, toBsccProbabilities);
                         requirements.clearUpperBounds();
                     }
                     STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UnmetRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
-                    eqSysMatrix.transpose(false, true); // Transpose so that each row considers the predecessors
+                    eqSysMatrix = eqSysMatrix.transpose(false, true); // Transpose so that each row considers the predecessors
                     if (isEqSysFormat) {
                         eqSysMatrix.convertToEquationSystem();
                     }
+                    std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, eqSysMatrix);
+                    solver->setLowerBound(storm::utility::zero<ValueType>());
+                    if (upperBounds) {
+                        solver->setUpperBounds(std::move(upperBounds.get()));
+                    }
                     std::vector<ValueType> eqSysRhs;
                     eqSysRhs.reserve(eqSysMatrix.getRowCount());
                     for (auto state : statesNotInComponent) {