From 6110a677f5796f32db182051fb251918de83d38a Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Tue, 3 Dec 2019 13:46:24 +0100
Subject: [PATCH] More environments checked in Lra Dtmc test.

---
 .../dtmc/LraDtmcPrctlModelCheckerTest.cpp     | 91 +++++++++++++++++--
 1 file changed, 81 insertions(+), 10 deletions(-)

diff --git a/src/test/storm/modelchecker/prctl/dtmc/LraDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/LraDtmcPrctlModelCheckerTest.cpp
index 6c63a1d21..3282607d4 100755
--- a/src/test/storm/modelchecker/prctl/dtmc/LraDtmcPrctlModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/prctl/dtmc/LraDtmcPrctlModelCheckerTest.cpp
@@ -16,80 +16,147 @@
 #include "storm/environment/solver/NativeSolverEnvironment.h"
 #include "storm/environment/solver/EigenSolverEnvironment.h"
 #include "storm/environment/solver/GmmxxSolverEnvironment.h"
+#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
 
 #include "storm-parsers/parser/AutoParser.h"
 #include "storm/builder/ExplicitModelBuilder.h"
 
 namespace {
     
-    class GmmxxDoubleGmresEnvironment {
+    class GBGmmxxDoubleGmresEnvironment {
     public:
         typedef double ValueType;
         static const bool isExact = false;
         static storm::Environment createEnvironment() {
             storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
             env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
             env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
             env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
             env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
             return env;
         }
     };
     
-    class EigenDoubleDGmresEnvironment {
+    class GBEigenDoubleDGmresEnvironment {
     public:
         typedef double ValueType;
         static const bool isExact = false;
         static storm::Environment createEnvironment() {
             storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
             env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
             env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
             env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
+            env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
             env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
             return env;
         }
     };
     
-    class EigenRationalLUEnvironment {
+    class GBEigenRationalLUEnvironment {
     public:
         typedef storm::RationalNumber ValueType;
         static const bool isExact = true;
         static storm::Environment createEnvironment() {
             storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
             env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
             env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
             return env;
         }
     };
     
-    class NativeSorEnvironment {
+    class GBNativeSorEnvironment {
     public:
         typedef double ValueType;
         static const bool isExact = false;
         static storm::Environment createEnvironment() {
             storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
             env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
             env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
             env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.8)); // A test fails if this is set to 0.9...
             env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
             return env;
         }
     };
     
-    class NativeWalkerChaeEnvironment {
+    class GBNativeWalkerChaeEnvironment {
     public:
         typedef double ValueType;
         static const bool isExact = false;
         static storm::Environment createEnvironment() {
             storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
             env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
             env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
             env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
             env.solver().native().setMaximalNumberOfIterations(50000);
             return env;
         }
     };
     
+    class DistrGmmxxDoubleGmresEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations);
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
+            env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
+            env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
+            env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
+    class DistrEigenRationalLUEnvironment {
+    public:
+        typedef storm::RationalNumber ValueType;
+        static const bool isExact = true;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::LraDistributionEquations);
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
+            env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
+            return env;
+        }
+    };
+    
+    class DistrNativeWalkerChaeEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::GainBiasEquations);
+            env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
+            env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
+            env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            env.solver().native().setMaximalNumberOfIterations(50000);
+            return env;
+        }
+    };
+    
+    class ValueIterationEnvironment {
+    public:
+        typedef double ValueType;
+        static const bool isExact = false;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().lra().setDetLraMethod(storm::solver::LraMethod::ValueIteration);
+            env.solver().lra().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
+            return env;
+        }
+    };
+    
     template<typename TestType>
     class LraDtmcPrctlModelCheckerTest : public ::testing::Test {
     public:
@@ -104,11 +171,15 @@ namespace {
     };
   
     typedef ::testing::Types<
-            GmmxxDoubleGmresEnvironment,
-            EigenDoubleDGmresEnvironment,
-            EigenRationalLUEnvironment,
-            NativeSorEnvironment,
-            NativeWalkerChaeEnvironment
+            GBGmmxxDoubleGmresEnvironment,
+            GBEigenDoubleDGmresEnvironment,
+            GBEigenRationalLUEnvironment,
+            GBNativeSorEnvironment,
+            GBNativeWalkerChaeEnvironment,
+            DistrGmmxxDoubleGmresEnvironment,
+            DistrEigenRationalLUEnvironment,
+            DistrNativeWalkerChaeEnvironment,
+            ValueIterationEnvironment
     > TestingTypes;
     
    TYPED_TEST_SUITE(LraDtmcPrctlModelCheckerTest, TestingTypes,);