From 20f07bf291caa13066382e342f09920e8cacb789 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 26 Aug 2016 19:04:35 +0200
Subject: [PATCH] added incremental strategy generation to symbolic game solver
 and removed some debug output

Former-commit-id: 96af928d00f806372842703cf3176c21b42c7746
---
 src/solver/SymbolicGameSolver.cpp | 26 +++++++++++++++++---------
 src/solver/SymbolicGameSolver.h   |  6 +++++-
 2 files changed, 22 insertions(+), 10 deletions(-)

diff --git a/src/solver/SymbolicGameSolver.cpp b/src/solver/SymbolicGameSolver.cpp
index 8788ce122..962cd540a 100644
--- a/src/solver/SymbolicGameSolver.cpp
+++ b/src/solver/SymbolicGameSolver.cpp
@@ -25,7 +25,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        storm::dd::Add<Type, ValueType> SymbolicGameSolver<Type, ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b) {
+        storm::dd::Add<Type, ValueType> SymbolicGameSolver<Type, ValueType>::solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b, boost::optional<storm::dd::Bdd<Type>> const& basePlayer1Strategy, boost::optional<storm::dd::Bdd<Type>> const& basePlayer2Strategy) {
             // Set up the environment.
             storm::dd::Add<Type, ValueType> xCopy = x;
             uint_fast64_t iterations = 0;
@@ -33,12 +33,24 @@ namespace storm {
 
             // Prepare some data storage in case we need to generate strategies.
             if (generatePlayer1Strategy) {
-                player1Strategy = A.getDdManager().getBddZero();
+                if (basePlayer1Strategy) {
+                    player1Strategy = basePlayer1Strategy.get();
+                } else {
+                    player1Strategy = A.getDdManager().getBddZero();
+                }
             }
             boost::optional<storm::dd::Add<Type, ValueType>> previousPlayer2Values;
             if (generatePlayer2Strategy) {
-                previousPlayer2Values = A.getDdManager().template getAddZero<ValueType>();
-                player2Strategy = A.getDdManager().getBddZero();
+                if (basePlayer2Strategy) {
+                    player2Strategy = basePlayer2Strategy.get();
+
+                    // If we are required to generate a player 2 strategy based on another one that is not the zero strategy,
+                    // we need to determine the values, because only then we can update the strategy only if necessary.
+                    previousPlayer2Values = ((this->A * player2Strategy.get().template toAdd<ValueType>()).multiplyMatrix(x.swapVariables(this->rowColumnMetaVariablePairs), this->columnMetaVariables) + b).sumAbstract(this->player2Variables);
+                } else {
+                    player2Strategy = A.getDdManager().getBddZero();
+                    previousPlayer2Values = A.getDdManager().template getAddZero<ValueType>();
+                }
             }
             
             do {
@@ -54,7 +66,7 @@ namespace storm {
                     if (generatePlayer2Strategy) {
                         // Update only the choices that strictly improved the value.
                         storm::dd::Bdd<Type> maxChoices = tmp.maxAbstractRepresentative(this->player2Variables);
-                        player2Strategy = newValues.greater(previousPlayer2Values.get()).ite(maxChoices, player2Strategy.get());
+                        player2Strategy.get() = newValues.greater(previousPlayer2Values.get()).ite(maxChoices, player2Strategy.get());
                         previousPlayer2Values = newValues;
                     }
                     
@@ -71,16 +83,12 @@ namespace storm {
                 }
 
                 if (player1Goal == storm::OptimizationDirection::Maximize) {
-                    tmp.exportToDot("pl1_val_" + std::to_string(iterations) + ".dot");
                     storm::dd::Add<Type, ValueType> newValues = tmp.maxAbstract(this->player1Variables);
                     
-                    newValues.exportToDot("pl1_valabs_" + std::to_string(iterations) + ".dot");
                     if (generatePlayer1Strategy) {
                         // Update only the choices that strictly improved the value.
                         storm::dd::Bdd<Type> maxChoices = tmp.maxAbstractRepresentative(this->player1Variables);
-                        maxChoices.template toAdd<ValueType>().exportToDot("pl1_choices_" + std::to_string(iterations) + ".dot");
                         player1Strategy = newValues.greater(xCopy).ite(maxChoices, player1Strategy.get());
-                        player1Strategy.get().template toAdd<ValueType>().exportToDot("pl1_" + std::to_string(iterations) + ".dot");
                     }
                     
                     tmp = newValues;
diff --git a/src/solver/SymbolicGameSolver.h b/src/solver/SymbolicGameSolver.h
index 6ebe5d052..318eac12e 100644
--- a/src/solver/SymbolicGameSolver.h
+++ b/src/solver/SymbolicGameSolver.h
@@ -64,9 +64,13 @@ namespace storm {
              * @param player2Goal Sets whether player 2 wants to minimize or maximize.
              * @param x The initial guess of the solution.
              * @param b The vector to add after matrix-vector multiplication.
+             * @param basePlayer1Strategy If the vector x is not the zero vector and a strategy for player 1 is generated,
+             * then this strategy can be used to generate a strategy that only differs from the given one if it has to.
+             * @param basePlayer2Strategy If the vector x is not the zero vector and a strategy for player 1 is generated,
+             * then this strategy can be used to generate a strategy that only differs from the given one if it has to.
              * @return The solution vector.
              */
-            virtual storm::dd::Add<Type, ValueType> solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b);
+            virtual storm::dd::Add<Type, ValueType> solveGame(OptimizationDirection player1Goal, OptimizationDirection player2Goal, storm::dd::Add<Type, ValueType> const& x, storm::dd::Add<Type, ValueType> const& b, boost::optional<storm::dd::Bdd<Type>> const& basePlayer1Strategy = boost::none, boost::optional<storm::dd::Bdd<Type>> const& basePlayer2Strategy = boost::none);
         
             // Setters that enable the generation of the players' strategies.
             void setGeneratePlayer1Strategy(bool value);