From 250a4b9b9a5c46420c2c53518be17a415c38e8c3 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 9 Mar 2020 13:01:47 +0100
Subject: [PATCH] MdpModelChecheckerTest: added test cases for the different
 multiplication styles and multiplier types.

---
 .../prctl/mdp/MdpPrctlModelCheckerTest.cpp    | 61 ++++++++++++++++++-
 1 file changed, 59 insertions(+), 2 deletions(-)

diff --git a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp
index acc9f3679..0df0bea3f 100755
--- a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp
@@ -22,6 +22,7 @@
 #include "storm/modelchecker/results/QualitativeCheckResult.h"
 #include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/environment/solver/TopologicalSolverEnvironment.h"
+#include "storm/environment/solver/MultiplierEnvironment.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/logic/Formulas.h"
 #include "storm/storage/jani/Property.h"
@@ -31,7 +32,7 @@ namespace {
     
     enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd};
 
-    class SparseDoubleValueIterationEnvironment {
+    class SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment {
     public:
         static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
         static const MdpEngine engine = MdpEngine::PrismSparse;
@@ -42,6 +43,59 @@ namespace {
             storm::Environment env;
             env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
             env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel);
+            env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx);
+            return env;
+        }
+    };
+
+    class SparseDoubleValueIterationGmmxxRegularMultEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        static const MdpEngine engine = MdpEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular);
+            env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx);
+            return env;
+        }
+    };
+    
+    class SparseDoubleValueIterationNativeGaussSeidelMultEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        static const MdpEngine engine = MdpEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel);
+            env.solver().multiplier().setType(storm::solver::MultiplierType::Native);
+            return env;
+        }
+    };
+
+    class SparseDoubleValueIterationNativeRegularMultEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
+        static const MdpEngine engine = MdpEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
+            env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
+            env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular);
+            env.solver().multiplier().setType(storm::solver::MultiplierType::Native);
             return env;
         }
     };
@@ -447,7 +501,10 @@ namespace {
     };
   
     typedef ::testing::Types<
-            SparseDoubleValueIterationEnvironment,
+            SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment,
+            SparseDoubleValueIterationGmmxxRegularMultEnvironment,
+            SparseDoubleValueIterationNativeGaussSeidelMultEnvironment,
+            SparseDoubleValueIterationNativeRegularMultEnvironment,
             JaniSparseDoubleValueIterationEnvironment,
             JitSparseDoubleValueIterationEnvironment,
             SparseDoubleIntervalIterationEnvironment,