From 37cd2ad6824b5e790ef0f6bd38f27bdbba72d0f8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 10 Jun 2015 16:22:29 +0200
Subject: [PATCH] started working on game solver

Former-commit-id: 59c3528d237a7b91ff2acae5d2426955840d1c05
---
 src/models/ModelType.h                        |  2 +-
 .../symbolic/StochasticTwoPlayerGame.cpp      |  0
 src/models/symbolic/StochasticTwoPlayerGame.h | 69 +++++++++++++++++++
 3 files changed, 70 insertions(+), 1 deletion(-)
 create mode 100644 src/models/symbolic/StochasticTwoPlayerGame.cpp
 create mode 100644 src/models/symbolic/StochasticTwoPlayerGame.h

diff --git a/src/models/ModelType.h b/src/models/ModelType.h
index b67a03685..1c386030f 100644
--- a/src/models/ModelType.h
+++ b/src/models/ModelType.h
@@ -7,7 +7,7 @@ namespace storm {
     namespace models {
         // All supported model types.
         enum class ModelType {
-            Dtmc, Ctmc, Mdp, MarkovAutomaton
+            Dtmc, Ctmc, Mdp, MarkovAutomaton, S2pg
         };
         
         std::ostream& operator<<(std::ostream& os, ModelType const& type);
diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/models/symbolic/StochasticTwoPlayerGame.h b/src/models/symbolic/StochasticTwoPlayerGame.h
new file mode 100644
index 000000000..45d1e378a
--- /dev/null
+++ b/src/models/symbolic/StochasticTwoPlayerGame.h
@@ -0,0 +1,69 @@
+#ifndef STORM_MODELS_SYMBOLIC_STOCHASTICTWOPLAYERGAME_H_
+#define STORM_MODELS_SYMBOLIC_STOCHASTICTWOPLAYERGAME_H_
+
+#include "src/models/symbolic/NondeterministicModel.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace models {
+        namespace symbolic {
+            
+            /*!
+             * This class represents a discrete-time Markov decision process.
+             */
+            template<storm::dd::DdType Type>
+            class StochasticTwoPlayerGame : public NondeterministicModel<Type> {
+            public:
+                StochasticTwoPlayerGame(Mdp<Type> const& other) = default;
+                StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame<Type> const& other) = default;
+                
+#ifndef WINDOWS
+                StochasticTwoPlayerGame(StochasticTwoPlayerGame<Type>&& other) = default;
+                StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame<Type>&& other) = default;
+#endif
+                
+                /*!
+                 * Constructs a model from the given data.
+                 *
+                 * @param modelType The type of the model.
+                 * @param manager The manager responsible for the decision diagrams.
+                 * @param reachableStates A DD representing the reachable states.
+                 * @param initialStates A DD representing the initial states of the model.
+                 * @param transitionMatrix The matrix representing the transitions in the model.
+                 * @param rowVariables The set of row meta variables used in the DDs.
+                 * @param rowExpressionAdapter An object that can be used to translate expressions in terms of the row
+                 * meta variables.
+                 * @param columVariables The set of column meta variables used in the DDs.
+                 * @param columnExpressionAdapter An object that can be used to translate expressions in terms of the
+                 * column meta variables.
+                 * @param rowColumnMetaVariablePairs All pairs of row/column meta variables.
+                 * @param player1Variables The meta variables used to encode the nondeterministic choices of player 1.
+                 * @param player2Variables The meta variables used to encode the nondeterministic choices of player 2.
+                 * @param allNondeterminismVariables The meta variables used to encode the nondeterminism in the model.
+                 * @param labelToExpressionMap A mapping from label names to their defining expressions.
+                 * @param optionalStateRewardVector The reward values associated with the states.
+                 * @param optionalTransitionRewardMatrix The reward values associated with the transitions of the model.
+                 */
+                StochasticTwoPlayerGame(std::shared_ptr<storm::dd::DdManager<Type>> manager,
+                                        storm::dd::Bdd<Type> reachableStates,
+                                        storm::dd::Bdd<Type> initialStates,
+                                        storm::dd::Add<Type> transitionMatrix,
+                                        std::set<storm::expressions::Variable> const& rowVariables,
+                                        std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter,
+                                        std::set<storm::expressions::Variable> const& columnVariables,
+                                        std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter,
+                                        std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
+                                        std::set<storm::expressions::Variable> const& player1Variables,
+                                        std::set<storm::expressions::Variable> const& player2Variables,
+                                        std::set<storm::expressions::Variable> const& allNondeterminismVariables,
+                                        std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
+                                        boost::optional<storm::dd::Add<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(),
+                                        boost::optional<storm::dd::Add<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>());
+                
+            };
+            
+        } // namespace symbolic
+    } // namespace models
+} // namespace storm
+
+#endif /* STORM_MODELS_SYMBOLIC_STOCHASTICTWOPLAYERGAME_H_ */