From 0a689d232ed2da52bb528c512a7f46f02e67edfc Mon Sep 17 00:00:00 2001
From: Stefan Pranger <stefan.pranger@student.tugraz.at>
Date: Wed, 16 Dec 2020 12:15:16 +0100
Subject: [PATCH] init helper for games

---
 ...deterministicGameInfiniteHorizonHelper.cpp | 56 ++++++++++++++++
 ...ondeterministicGameInfiniteHorizonHelper.h | 66 +++++++++++++++++++
 2 files changed, 122 insertions(+)
 create mode 100644 src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
 create mode 100644 src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h

diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
new file mode 100644
index 000000000..baaa3782d
--- /dev/null
+++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.cpp
@@ -0,0 +1,56 @@
+#include "SparseNondeterministicGameInfiniteHorizonHelper.h"
+
+#include "storm/modelchecker/helper/infinitehorizon/internal/LraViHelper.h"
+
+#include "storm/storage/SparseMatrix.h"
+#include "storm/storage/Scheduler.h"
+
+#include "storm/solver/MinMaxLinearEquationSolver.h"
+#include "storm/solver/Multiplier.h"
+
+#include "storm/utility/solver.h"
+#include "storm/utility/vector.h"
+
+#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
+
+#include "storm/exceptions/UnmetRequirementException.h"
+#include "storm/exceptions/InternalException.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+
+            template <typename ValueType>
+            SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& coalitionIndices) : SparseInfiniteHorizonHelper<ValueType, true>(transitionMatrix), coalitionIndices(coalitionIndices) {
+                // Intentionally left empty.
+            }
+
+            template <typename ValueType>
+            void SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::createDecomposition() {
+                STORM_LOG_THROW(false, storm::exceptions::InternalException, "Creating Decompositions of SMGs is currently not possible.");
+            }
+
+            template <typename ValueType>
+            ValueType SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLraForComponent(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter, storm::storage::MaximalEndComponent const& component) {
+
+                STORM_LOG_THROW(false, storm::exceptions::InternalException, "Computing values for LRA for SMGs components is currently not possible.");
+            }
+
+            template <typename ValueType>
+            std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& componentLraValues) {
+                STORM_LOG_THROW(false, storm::exceptions::InternalException, "buildAndSolveSsp not available for SMGs");
+            }
+
+            template <typename ValueType>
+            std::vector<ValueType> SparseNondeterministicGameInfiniteHorizonHelper<ValueType>::computeLongRunAverageValues(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter) {
+                STORM_LOG_THROW(false, storm::exceptions::InternalException, "computeLongRunAverageValues not possible yet.");
+            }
+
+
+            template class SparseNondeterministicGameInfiniteHorizonHelper<double>;
+            template class SparseNondeterministicGameInfiniteHorizonHelper<storm::RationalNumber>;
+
+        }
+    }
+}
diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h
new file mode 100644
index 000000000..550d12a47
--- /dev/null
+++ b/src/storm/modelchecker/helper/infinitehorizon/SparseNondeterministicGameInfiniteHorizonHelper.h
@@ -0,0 +1,66 @@
+#pragma once
+#include "storm/modelchecker/helper/infinitehorizon/SparseInfiniteHorizonHelper.h"
+
+namespace storm {
+
+    namespace storage {
+        template <typename VT> class Scheduler;
+    }
+
+    namespace modelchecker {
+        namespace helper {
+
+            /*!
+             * Helper class for model checking queries that depend on the long run behavior of the (nondeterministic) system with different players choices.
+             * @tparam ValueType the type a value can have
+             */
+            template <typename ValueType>
+            class SparseNondeterministicGameInfiniteHorizonHelper : public SparseInfiniteHorizonHelper<ValueType, true> {
+
+            public:
+
+                /*!
+                 * Function mapping from indices to values
+                 */
+                typedef typename SparseInfiniteHorizonHelper<ValueType, true>::ValueGetter ValueGetter;
+
+                /*!
+                 * Initializes the helper for a discrete time model with different players (i.e. SMG)
+                 */
+                SparseNondeterministicGameInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& coalitionIndices);
+
+                /*!
+                 * TODO
+                 */
+                std::vector<ValueType> computeLongRunAverageValues(Environment const& env, ValueGetter const& stateRewardsGetter, ValueGetter const& actionRewardsGetter);
+
+                /*!
+                 * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+                 * @return the produced scheduler of the most recent call.
+                 */
+                //std::vector<uint64_t> const& getProducedOptimalChoices() const;
+
+                /*!
+                 * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+                 * @return the produced scheduler of the most recent call.
+                 */
+                //std::vector<uint64_t>& getProducedOptimalChoices();
+
+                /*!
+                 * @pre before calling this, a computation call should have been performed during which scheduler production was enabled.
+                 * @return a new scheduler containing optimal choices for each state that yield the long run average values of the most recent call.
+                 */
+                //storm::storage::Scheduler<ValueType> extractScheduler() const;
+
+                void createDecomposition();
+                ValueType computeLraForComponent(Environment const& env, ValueGetter const& stateValuesGetter,  ValueGetter const& actionValuesGetter, storm::storage::MaximalEndComponent const& component);
+                std::vector<ValueType> buildAndSolveSsp(Environment const& env, std::vector<ValueType> const& mecLraValues);
+
+            private:
+                std::vector<uint64_t> coalitionIndices;
+            };
+
+
+        }
+    }
+}