From acde9f571fa476e365c95419dd5af4d58c4eeb3c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 16 Nov 2017 16:34:45 +0100
Subject: [PATCH] fixed policy iteration on MTBDDs

---
 .../solver/SymbolicMinMaxLinearEquationSolver.cpp    | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
index 86c9b2b4d..b2e39ac0a 100644
--- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
@@ -320,6 +320,7 @@ namespace storm {
             if (solver.getEquationProblemFormat() == storm::solver::LinearEquationSolverProblemFormat::EquationSystem) {
                 schedulerA = diagonal - schedulerA;
             }
+
             storm::dd::Add<DdType, ValueType> schedulerB = scheduler.ite(b, scheduler.getDdManager().template getAddZero<ValueType>()).sumAbstract(this->choiceVariables);
 
             // Set the matrix for the solver.
@@ -356,9 +357,16 @@ namespace storm {
                 storm::dd::Bdd<DdType> nextScheduler;
                 if (dir == storm::solver::OptimizationDirection::Minimize) {
                     choiceValues += illegalMaskAdd;
-                    nextScheduler = choiceValues.minAbstractRepresentative(this->choiceVariables);
+                    
+                    storm::dd::Add<DdType, ValueType> newStateValues = choiceValues.minAbstract(this->choiceVariables);
+                    storm::dd::Bdd<DdType> improvedStates = newStateValues.less(schedulerX);
+                    
+                    nextScheduler = improvedStates.ite(choiceValues.minAbstractRepresentative(this->choiceVariables), scheduler);
                 } else {
-                    nextScheduler = choiceValues.maxAbstractRepresentative(this->choiceVariables);
+                    storm::dd::Add<DdType, ValueType> newStateValues = choiceValues.maxAbstract(this->choiceVariables);
+                    storm::dd::Bdd<DdType> improvedStates = newStateValues.greater(schedulerX);
+
+                    nextScheduler = improvedStates.ite(choiceValues.maxAbstractRepresentative(this->choiceVariables), scheduler);
                 }
                 
                 // Check for convergence.