From db6f43ed9d0a39bc7d8d03be6473ce3aa9950c3c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 30 Jun 2018 11:04:22 +0200
Subject: [PATCH] made LRA computation for deterministic systems able to
 respect that the underlying solver requires a fixed-point formulation

---
 .../csl/helper/SparseCtmcCslHelper.cpp        | 26 +++++++++++--------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index f888ed1b6..f9e6da475 100644
--- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -478,6 +478,17 @@ namespace storm {
                         }
                     }
                     
+                    // Build a different system depending on the problem format of the equation solver.
+                    // Check solver requirements.
+                    storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
+                    auto requirements = linearEquationSolverFactory.getRequirements(env);
+                    STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
+                    
+                    bool fixedPointSystem = false;
+                    if (linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::FixedPointSystem) {
+                        fixedPointSystem = true;
+                    }
+                    
                     // Now build the final equation system matrix, the initial guess and the right-hand side in one go.
                     std::vector<ValueType> bsccEquationSystemRightSide(bsccEquationSystem.getColumnCount(), zero);
                     storm::storage::SparseMatrixBuilder<ValueType> builder;
@@ -486,7 +497,7 @@ namespace storm {
                         // If the current row is the first one belonging to a BSCC, we substitute it by the constraint that the
                         // values for states of this BSCC must sum to one. However, in order to have a non-zero value on the
                         // diagonal, we add the constraint of the BSCC that produces a 1 on the diagonal.
-                        if (firstStatesInBsccs.get(row)) {
+                        if (!fixedPointSystem && firstStatesInBsccs.get(row)) {
                             uint_fast64_t requiredBscc = stateToBsccIndexMap[row];
                             storm::storage::StronglyConnectedComponent const& bscc = bsccDecomposition[requiredBscc];
                             
@@ -499,14 +510,13 @@ namespace storm {
                         } else {
                             // Otherwise, we copy the row, and subtract 1 from the diagonal.
                             for (auto& entry : bsccEquationSystem.getRow(row)) {
-                                if (entry.getColumn() == row) {
-                                    builder.addNextValue(row, entry.getColumn(), entry.getValue() - one);
-                                } else {
+                                if (fixedPointSystem || entry.getColumn() != row) {
                                     builder.addNextValue(row, entry.getColumn(), entry.getValue());
+                                } else {
+                                    builder.addNextValue(row, entry.getColumn(), entry.getValue() - one);
                                 }
                             }
                         }
-                        
                     }
                     
                     // Create the initial guess for the LRAs. We take a uniform distribution over all states in a BSCC.
@@ -522,12 +532,6 @@ namespace storm {
                     bsccEquationSystem = builder.build();
                     
                     {
-                        // Check solver requirements
-                        storm::solver::GeneralLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
-                        auto requirements = linearEquationSolverFactory.getRequirements(env);
-                        STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
-                        // Check whether we have the right input format for the solver.
-                        STORM_LOG_THROW(linearEquationSolverFactory.getEquationProblemFormat(env) == storm::solver::LinearEquationSolverProblemFormat::EquationSystem, storm::exceptions::FormatUnsupportedBySolverException, "The selected solver does not support the required format.");
                         std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(bsccEquationSystem));
                         solver->solveEquations(env, bsccEquationSystemSolution, bsccEquationSystemRightSide);
                     }