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 schedulerB = scheduler.ite(b, scheduler.getDdManager().template getAddZero()).sumAbstract(this->choiceVariables); // Set the matrix for the solver. @@ -356,9 +357,16 @@ namespace storm { storm::dd::Bdd nextScheduler; if (dir == storm::solver::OptimizationDirection::Minimize) { choiceValues += illegalMaskAdd; - nextScheduler = choiceValues.minAbstractRepresentative(this->choiceVariables); + + storm::dd::Add newStateValues = choiceValues.minAbstract(this->choiceVariables); + storm::dd::Bdd improvedStates = newStateValues.less(schedulerX); + + nextScheduler = improvedStates.ite(choiceValues.minAbstractRepresentative(this->choiceVariables), scheduler); } else { - nextScheduler = choiceValues.maxAbstractRepresentative(this->choiceVariables); + storm::dd::Add newStateValues = choiceValues.maxAbstract(this->choiceVariables); + storm::dd::Bdd improvedStates = newStateValues.greater(schedulerX); + + nextScheduler = improvedStates.ite(choiceValues.maxAbstractRepresentative(this->choiceVariables), scheduler); } // Check for convergence.