Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective

resources/3rdparty/carl/CMakeLists.txt

@@ -8,15 +8,15 @@ message(STORM_3RDPARTY_BINARY_DIR: ${STORM_3RDPARTY_BINARY_DIR})
 
 ExternalProject_Add(carl-config
 	GIT_REPOSITORY https://github.com/smtrat/carl
-        GIT_TAG 17.08
+	GIT_TAG 17.10
 	PREFIX here
 	SOURCE_DIR source_dir
 	BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
 	CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=ON -DEXPORT_TO_CMAKE=ON -DTHREAD_SAFE=ON -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=ON -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl
-        BUILD_IN_SOURCE 0
-        LOG_UPDATE OFF
-        LOG_CONFIGURE OFF
-        BUILD_COMMAND "" # Disable build step.
+	BUILD_IN_SOURCE 0
+	LOG_UPDATE OFF
+	LOG_CONFIGURE OFF
+	BUILD_COMMAND "" # Disable build step.
 	INSTALL_COMMAND "" # Disable install step too.
 )
 add_custom_target(build-carl)

src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp

@@ -146,9 +146,9 @@ namespace storm {
             lowerResultBound = storm::utility::zero<ConstantType>();
             upperResultBound = storm::utility::one<ConstantType>();
             
-            auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+            // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
+            auto req = solverFactory->getRequirements(true);
             req.clearBounds();
-            req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
             STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
             solverFactory->setRequirementsChecked(true);
         }
@@ -185,8 +185,8 @@ namespace storm {
             // We only know a lower bound for the result
             lowerResultBound = storm::utility::zero<ConstantType>();
         
-            auto req = solverFactory->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
-            req.clearNoEndComponents(); // We never have end components within the maybestates (assuming graph-preserving instantiations).
+            // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
+            auto req = solverFactory->getRequirements(true);
             req.clearLowerBounds();
             if (req.requiresUpperBounds()) {
                 solvingRequiresUpperRewardBounds = true;
@@ -253,6 +253,7 @@ namespace storm {
                 solverFactory->setMinMaxMethod(storm::solver::MinMaxMethod::PolicyIteration);
             }
             auto solver = solverFactory->create(parameterLifter->getMatrix());
+            solver->setHasUniqueSolution();
             if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
             if (upperResultBound) {
                 solver->setUpperBound(upperResultBound.get());

src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -89,10 +89,14 @@ namespace storm {
                 }
 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
+                // The solution is unique as we assume non-zeno MAs.
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir);
+                requirements.clearBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
 
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic);
+                solver->setHasUniqueSolution();
+                solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
                 solver->setRequirementsChecked();
                 solver->setCachingEnabled(true);
                 
@@ -376,10 +380,14 @@ namespace storm {
                 std::vector<ValueType> x(numberOfSspStates);
                 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir);
+                requirements.clearBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
 
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix);
+                solver->setHasUniqueSolution();
+                solver->setLowerBound(storm::utility::zero<ValueType>());
+                solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end()));
                 solver->setRequirementsChecked();
                 solver->solveEquations(dir, x, b);
                 
@@ -584,10 +592,14 @@ namespace storm {
                 std::vector<ValueType> b = probabilisticChoiceRewards;
                 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards);
+                // The solution is unique as we assume non-zeno MAs.
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, dir);
+                requirements.clearLowerBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
 
                 auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic));
+                solver->setLowerBound(storm::utility::zero<ValueType>());
+                solver->setHasUniqueSolution(true);
                 solver->setRequirementsChecked(true);
                 solver->setCachingEnabled(true);
                 

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp

@@ -299,10 +299,10 @@ namespace storm {
                 std::unique_ptr<MinMaxSolverData> result(new MinMaxSolverData());
                 storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
                 result->solver = minMaxSolverFactory.create(PS.toPS);
+                result->solver->setHasUniqueSolution(true);
                 result->solver->setTrackScheduler(true);
                 result->solver->setCachingEnabled(true);
-                auto req = result->solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
-                req.clearNoEndComponents();
+                auto req = result->solver->getRequirements(storm::solver::OptimizationDirection::Maximize);
                 boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true));
                 if (lowerBound) {
                     result->solver->setLowerBound(lowerBound.get());

src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp

@@ -278,10 +278,7 @@ namespace storm {
                             cachedData.linEqSolver->setUpperBound(*obj.upperResultBound);
                             req.clearUpperBounds();
                         }
-                        if (!req.empty()) {
-                            // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
-                            STORM_LOG_DEBUG("At least one requirement of the LinearEquationSolver was not met.");
-                        }
+                        STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
                         cachedData.linEqSolver->solveEquations(x, cachedData.bLinEq);
                         auto resultIt = result.begin();
                         for (auto const& state : epochModel.epochInStates) {
@@ -303,11 +300,11 @@ namespace storm {
                     cachedData.xMinMax.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                     storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
                     cachedData.minMaxSolver = minMaxSolverFactory.create(epochModel.epochMatrix);
+                    cachedData.minMaxSolver->setHasUniqueSolution();
                     cachedData.minMaxSolver->setPrecision(precision);
                     cachedData.minMaxSolver->setTrackScheduler(true);
                     cachedData.minMaxSolver->setCachingEnabled(true);
-                    auto req = cachedData.minMaxSolver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
-                    req.clearNoEndComponents();
+                    auto req = cachedData.minMaxSolver->getRequirements();
                     boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, storm::storage::BitVector(weightVector.size(), true));
                     if (lowerBound) {
                         cachedData.minMaxSolver->setLowerBound(lowerBound.get());
@@ -318,10 +315,7 @@ namespace storm {
                         cachedData.minMaxSolver->setUpperBound(upperBound.get());
                         req.clearUpperBounds();
                     }
-                    if (!req.empty()) {
-                        // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
-                        STORM_LOG_DEBUG("At least one requirement of the LinearEquationSolver was not met.");
-                    }
+                    STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
                     cachedData.minMaxSolver->setRequirementsChecked(true);
                     cachedData.minMaxSolver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@@ -174,8 +174,8 @@ namespace storm {
                 storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> solverFactory;
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(ecQuotient->matrix);
                 solver->setTrackScheduler(true);
-                auto req = solver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
-                req.clearNoEndComponents();
+                solver->setHasUniqueSolution(true);
+                auto req = solver->getRequirements();
                 boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound);
                 if (lowerBound) {
                     solver->setLowerBound(lowerBound.get());
@@ -186,10 +186,7 @@ namespace storm {
                     solver->setUpperBound(upperBound.get());
                     req.clearUpperBounds();
                 }
-                if (!req.empty()) {
-                    // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
-                    STORM_LOG_DEBUG("At least one requirement of the LinearEquationSolver was not met.");
-                }
+                STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
                 solver->setRequirementsChecked(true);
                 solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -67,7 +67,7 @@ namespace storm {
                 }
                 auto formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(checkTask.getFormula().asSharedPointer(), opInfo);
                 storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
-                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory, storm::utility::one<ValueType>());
+                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(helper::SolutionType::UntilProbabilities, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory);
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             } else {
                 STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
@@ -146,7 +146,7 @@ namespace storm {
                 }
                 auto formula = std::make_shared<storm::logic::RewardOperatorFormula>(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo);
                 storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
-                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory);
+                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(helper::SolutionType::ExpectedRewards, checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory);
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             } else {
                 

src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp

@@ -135,8 +135,10 @@ namespace storm {
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
+                        // If we minimize, we know that the solution to the equation system is unique.
+                        bool uniqueSolution = dir == storm::solver::OptimizationDirection::Minimize;
                         // Check for requirements of the solver early so we can adjust the maybe state computation accordingly.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir);
+                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir);
                         storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements;
                         SolverRequirementsData<ValueType> solverRequirementsData;
                         bool extendMaybeStates = false;
@@ -212,6 +214,10 @@ namespace storm {
                         std::vector<ValueType> x(explicitRepresentation.first.getRowGroupCount(), storm::utility::zero<ValueType>());
                         
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first));
+                        
+                        // Set whether the equation system will have a unique solution
+                        solver->setHasUniqueSolution(uniqueSolution);
+
                         if (solverRequirementsData.initialScheduler) {
                             solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get()));
                         }
@@ -487,8 +493,10 @@ namespace storm {
                 } else {
                     // If there are maybe states, we need to solve an equation system.
                     if (!maybeStates.isZero()) {
+                        // If we maximize, we know that the solution to the equation system is unique.
+                        bool uniqueSolution = dir == storm::solver::OptimizationDirection::Maximize;
                         // Check for requirements of the solver this early so we can adapt the maybe states accordingly.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir);
+                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(uniqueSolution, dir);
                         storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements;
                         bool extendMaybeStates = false;
                         if (!clearedRequirements.empty()) {
@@ -568,6 +576,9 @@ namespace storm {
                         // Now solve the resulting equation system.
                         std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create();
                         
+                        // Set whether the equation system will have a unique solution
+                        solver->setHasUniqueSolution(uniqueSolution);
+                        
                         // If the solver requires upper bounds, compute them now.
                         if (requirements.requiresUpperBounds()) {
                             setUpperRewardBounds(*solver, dir, explicitRepresentation.first, explicitRepresentation.second, solverRequirementsData.oneStepTargetProbabilities.get());

src/storm/modelchecker/prctl/helper/SolutionType.h

@@ -0,0 +1,12 @@
+#pragma once
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+            enum class SolutionType {
+                UntilProbabilities,
+                ExpectedRewards
+            };
+        }
+    }
+}

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -26,6 +26,7 @@
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/MinMaxEquationSolverSettings.h"
 #include "storm/settings/modules/GeneralSettings.h"
+#include "storm/settings/modules/CoreSettings.h"
 
 #include "storm/utility/Stopwatch.h"
 
@@ -81,7 +82,7 @@ namespace storm {
             }
 
             template<typename ValueType>
-            std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<ValueType> const& upperBound) {
+            std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(SolutionType const& type, OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
                 storm::utility::Stopwatch swAll(true), swBuild, swCheck;
                 auto initEpoch = rewardUnfolding.getStartEpoch();
                 auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
@@ -98,8 +99,6 @@ namespace storm {
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet()) {
                     precision = precision / storm::utility::convertNumber<ValueType>(epochCount);
                 }
-                STORM_PRINT_AND_LOG("Objective/Dimension/Epoch count is: " << 1 << "/" << rewardUnfolding.getEpochManager().getDimensionCount() << "/" <<  epochOrder.size() << "."  << std::endl);
-
                 for (auto const& epoch : epochOrder) {
                     swBuild.start();
                     auto& epochModel = rewardUnfolding.setCurrentEpoch(epoch);
@@ -155,23 +154,23 @@ namespace storm {
                         if (epochModel.epochMatrixChanged) {
                             x.assign(epochModel.epochMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
                             minMaxSolver = minMaxLinearEquationSolverFactory.create(epochModel.epochMatrix);
+                            minMaxSolver->setHasUniqueSolution();
                             minMaxSolver->setPrecision(precision);
                             minMaxSolver->setOptimizationDirection(dir);
                             minMaxSolver->setCachingEnabled(true);
                             minMaxSolver->setTrackScheduler(true);
-                            auto req = minMaxSolver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath, dir);
+                            auto req = minMaxSolver->getRequirements(dir);
                             minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
                             req.clearLowerBounds();
-                            if (upperBound) {
-                                minMaxSolver->setUpperBound(upperBound.get());
+                            if (type == SolutionType::UntilProbabilities) {
+                                minMaxSolver->setUpperBound(storm::utility::one<ValueType>());
                                 req.clearUpperBounds();
+                            } else if (type == SolutionType::ExpectedRewards) {
+                                // TODO
+                                STORM_LOG_WARN_COND(!req.requiresUpperBounds(), "Upper bounds for expected reward are not specified.");
                             }
-                            req.clearNoEndComponents();
-                            if (!req.empty()) {
-                                // Todo: currently we wrongly require lower bounds for plain value iteration even if the fixpoint is unique
-                                STORM_LOG_DEBUG("A solver requirement is not satisfied.");
-                                minMaxSolver->setRequirementsChecked();
-                            }
+                            STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
+                            minMaxSolver->setRequirementsChecked();
                         } else {
                             auto choicesTmp = minMaxSolver->getSchedulerChoices();
                             minMaxSolver->setInitialScheduler(std::move(choicesTmp));
@@ -205,14 +204,16 @@ namespace storm {
                 }
                 
                 swAll.stop();
-                std::cout << "---------------------------------" << std::endl;
-                std::cout << "Statistics:" << std::endl;
-                std::cout << "---------------------------------" << std::endl;
-                std::cout << "          #checked epochs: " << epochOrder.size() << "." << std::endl;
-                std::cout << "             overall Time: " << swAll << "." << std::endl;
-                std::cout << "Epoch Model building Time: " << swBuild << "." << std::endl;
-                std::cout << "Epoch Model checking Time: " << swCheck << "." << std::endl;
-                std::cout << "---------------------------------" << std::endl;
+                if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
+                    STORM_PRINT_AND_LOG("---------------------------------" << std::endl);
+                    STORM_PRINT_AND_LOG("Statistics:" << std::endl);
+                    STORM_PRINT_AND_LOG("---------------------------------" << std::endl);
+                    STORM_PRINT_AND_LOG("          #checked epochs: " << epochOrder.size() << "." << std::endl);
+                    STORM_PRINT_AND_LOG("             overall Time: " << swAll << "." << std::endl);
+                    STORM_PRINT_AND_LOG("Epoch Model building Time: " << swBuild << "." << std::endl);
+                    STORM_PRINT_AND_LOG("Epoch Model checking Time: " << swCheck << "." << std::endl);
+                    STORM_PRINT_AND_LOG("---------------------------------" << std::endl);
+                }
                 
                 return  result;
             }
@@ -231,12 +232,12 @@ namespace storm {
             }
             
             template<typename ValueType>
-            std::vector<uint_fast64_t> computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) {
+            std::vector<uint_fast64_t> computeValidSchedulerHint(SolutionType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) {
                 storm::storage::Scheduler<ValueType> validScheduler(maybeStates.size());
 
-                if (type == storm::solver::EquationSystemType::UntilProbabilities) {
+                if (type == SolutionType::UntilProbabilities) {
                     storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler, boost::none);
-                } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) {
+                } else if (type == SolutionType::ExpectedRewards) {
                     storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates, validScheduler);
                 } else {
                     STORM_LOG_ASSERT(false, "Unexpected equation system type.");
@@ -254,7 +255,7 @@ namespace storm {
             
             template<typename ValueType>
             struct SparseMdpHintType {
-                SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false) {
+                SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false) {
                     // Intentionally left empty.
                 }
                 
@@ -310,6 +311,10 @@ namespace storm {
                     return computeUpperBounds;
                 }
 
+                bool hasUniqueSolution() const {
+                    return uniqueSolution;
+                }
+                
                 boost::optional<std::vector<uint64_t>> schedulerHint;
                 boost::optional<std::vector<ValueType>> valueHint;
                 boost::optional<ValueType> lowerResultBound;
@@ -317,6 +322,7 @@ namespace storm {
                 boost::optional<std::vector<ValueType>> upperResultBounds;
                 bool eliminateEndComponents;
                 bool computeUpperBounds;
+                bool uniqueSolution;
             };
             
             template<typename ValueType>
@@ -370,19 +376,22 @@ namespace storm {
             }
             
             template<typename ValueType>
-            SparseMdpHintType<ValueType> computeHints(storm::solver::EquationSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
+            SparseMdpHintType<ValueType> computeHints(SolutionType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
                 SparseMdpHintType<ValueType> result;
 
+                // The solution to the min-max equation system is unique if we minimize until probabilities or
+                // maximize reachability rewards or if the hint tells us that there are no end-compontnes.
+                result.uniqueSolution = (dir == storm::solver::OptimizationDirection::Minimize && type == SolutionType::UntilProbabilities)
+                                      || (dir == storm::solver::OptimizationDirection::Maximize && type == SolutionType::ExpectedRewards)
+                                      || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
+                
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type, dir);
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(result.uniqueSolution, dir);
                 if (!requirements.empty()) {
-                    // If the hint tells us that there are no end-components, we can clear that requirement.
-                    if (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates()) {
-                        requirements.clearNoEndComponents();
-                    }
                     
                     // If the solver still requires no end-components, we have to eliminate them later.
                     if (requirements.requiresNoEndComponents()) {
+                        STORM_LOG_ASSERT(!result.hasUniqueSolution(), "The solver requires to eliminate the end components although the solution is already assumed to be unique.");
                         STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
                         result.eliminateEndComponents = true;
                         requirements.clearNoEndComponents();
@@ -396,9 +405,9 @@ namespace storm {
                     }
                     
                     // Finally, we have information on the bounds depending on the problem type.
-                    if (type == storm::solver::EquationSystemType::UntilProbabilities) {
+                    if (type == SolutionType::UntilProbabilities) {
                         requirements.clearBounds();
-                    } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) {
+                    } else if (type == SolutionType::ExpectedRewards) {
                         requirements.clearLowerBounds();
                     }
                     if (requirements.requiresUpperBounds()) {
@@ -413,8 +422,7 @@ namespace storm {
                 // Only if there is no end component decomposition that we will need to do later, we use value and scheduler
                 // hints from the provided hint.
                 if (!result.eliminateEndComponents) {
-                    bool skipEcWithinMaybeStatesCheck = dir == storm::OptimizationDirection::Minimize || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
-                    extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck);
+                    extractValueAndSchedulerHint(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, result.uniqueSolution);
                 } else {
                     STORM_LOG_WARN_COND(hint.isEmpty(), "A non-empty hint was provided, but its information will be disregarded.");
                 }
@@ -423,7 +431,7 @@ namespace storm {
                 if (!result.hasLowerResultBound()) {
                     result.lowerResultBound = storm::utility::zero<ValueType>();
                 }
-                if (!result.hasUpperResultBound() && type == storm::solver::EquationSystemType::UntilProbabilities) {
+                if (!result.hasUpperResultBound() && type == SolutionType::UntilProbabilities) {
                     result.upperResultBound = storm::utility::one<ValueType>();
                 }
                 
@@ -466,6 +474,7 @@ namespace storm {
                 // Set up the solver.
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix));
                 solver->setRequirementsChecked();
+                solver->setHasUniqueSolution(hint.hasUniqueSolution());
                 if (hint.hasLowerResultBound()) {
                     solver->setLowerBound(hint.getLowerResultBound());
                 }
@@ -666,7 +675,7 @@ namespace storm {
                         // In this case we have have to compute the remaining probabilities.
                         
                         // Obtain proper hint information either from the provided hint or from requirements of the solver.
-                        SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::EquationSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory);
+                        SparseMdpHintType<ValueType> hintInformation = computeHints(SolutionType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, phiStates, qualitativeStateSets.statesWithProbability1, minMaxLinearEquationSolverFactory);
                         
                         // Declare the components of the equation system we will solve.
                         storm::storage::SparseMatrix<ValueType> submatrix;
@@ -1022,7 +1031,7 @@ namespace storm {
                         }
                         
                         // Obtain proper hint information either from the provided hint or from requirements of the solver.
-                        SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::EquationSystemType::ReachabilityRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices);
+                        SparseMdpHintType<ValueType> hintInformation = computeHints(SolutionType::ExpectedRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, qualitativeStateSets.maybeStates, ~targetStates, targetStates, minMaxLinearEquationSolverFactory, selectedChoices);
                         
                         // Declare the components of the equation system we will solve.
                         storm::storage::SparseMatrix<ValueType> submatrix;
@@ -1229,14 +1238,16 @@ namespace storm {
                 storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates);
                 
                 // Check for requirements of the solver.
-                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
-                requirements.clearLowerBounds();
+                storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(true, goal.direction());
+                requirements.clearBounds();
                 STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
                 
                 std::vector<ValueType> sspResult(numberOfSspStates);
                 goal.restrictRelevantValues(statesNotContainedInAnyMec);
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(std::move(goal), minMaxLinearEquationSolverFactory, sspMatrix);
                 solver->setLowerBound(storm::utility::zero<ValueType>());
+                solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end()));
+                solver->setHasUniqueSolution();
                 solver->setRequirementsChecked();
                 solver->solveEquations(sspResult, b);
                 

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -4,6 +4,7 @@
 #include <vector>
 
 #include "storm/modelchecker/hints/ModelCheckerHint.h"
+#include "storm/modelchecker/prctl/helper/SolutionType.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/MaximalEndComponent.h"
 #include "storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h"
@@ -34,9 +35,10 @@ namespace storm {
             template <typename ValueType>
             class SparseMdpPrctlHelper {
             public:
+                
                 static std::vector<ValueType> computeStepBoundedUntilProbabilities(storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
 
-                static std::map<storm::storage::sparse::state_type, ValueType> computeRewardBoundedValues(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<ValueType> const& upperBound = boost::none);
+                static std::map<storm::storage::sparse::state_type, ValueType> computeRewardBoundedValues(SolutionType const& type, OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
                 
                 static std::vector<ValueType> computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 

src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp

@@ -22,14 +22,20 @@ namespace storm {
     namespace modelchecker {
         namespace helper {
        
+            enum class EquationSystemType {
+                UntilProbabilities,
+                ExpectedRewards
+            };
+
+            
             template<storm::dd::DdType DdType, typename ValueType>
-            storm::dd::Bdd<DdType> computeValidSchedulerHint(storm::solver::EquationSystemType const& type, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& maybeStates, storm::dd::Bdd<DdType> const& targetStates) {
+            storm::dd::Bdd<DdType> computeValidSchedulerHint(EquationSystemType const& type, storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, storm::dd::Bdd<DdType> const& maybeStates, storm::dd::Bdd<DdType> const& targetStates) {
             
                 storm::dd::Bdd<DdType> result;
                 
-                if (type == storm::solver::EquationSystemType::UntilProbabilities) {
+                if (type == EquationSystemType::UntilProbabilities) {
                     result = storm::utility::graph::computeSchedulerProbGreater0E(model, transitionMatrix.notZero(), maybeStates, targetStates);
-                } else if (type == storm::solver::EquationSystemType::ReachabilityRewards) {
+                } else if (type == EquationSystemType::ExpectedRewards) {
                     result = storm::utility::graph::computeSchedulerProb1E(model, transitionMatrix.notZero(), maybeStates, targetStates, maybeStates || targetStates);
                 }
                 
@@ -78,13 +84,18 @@ namespace storm {
                         // Now solve the resulting equation system.
                         std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
 
+                        // If we minimize, we know that the solution is unique
+                        if (dir == storm::solver::OptimizationDirection::Minimize) {
+                            solver->setHasUniqueSolution();
+                        }
+                        
                         // Check requirements of solver.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::UntilProbabilities, dir);
+                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir);
                         boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
                         if (!requirements.empty()) {
                             if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
                                 STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
-                                initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability01.second);
+                                initialScheduler = computeValidSchedulerHint(EquationSystemType::UntilProbabilities, model, transitionMatrix, maybeStates, statesWithProbability01.second);
                                 requirements.clearValidInitialScheduler();
                             }
                             requirements.clearBounds();
@@ -237,13 +248,18 @@ namespace storm {
                         // Now solve the resulting equation system.
                         std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getIllegalMask() && maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getNondeterminismVariables(), model.getRowColumnMetaVariablePairs());
                         
+                        // If we maximize, we know that the solution is unique
+                        if (dir == storm::solver::OptimizationDirection::Maximize) {
+                            solver->setHasUniqueSolution();
+                        }
+                        
                         // Check requirements of solver.
-                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(storm::solver::EquationSystemType::ReachabilityRewards, dir);
+                        storm::solver::MinMaxLinearEquationSolverRequirements requirements = solver->getRequirements(dir);
                         boost::optional<storm::dd::Bdd<DdType>> initialScheduler;
                         if (!requirements.empty()) {
                             if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
                                 STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
-                                initialScheduler = computeValidSchedulerHint(storm::solver::EquationSystemType::ReachabilityRewards, model, transitionMatrix, maybeStates, targetStates);
+                                initialScheduler = computeValidSchedulerHint(EquationSystemType::ExpectedRewards, model, transitionMatrix, maybeStates, targetStates);
                                 requirements.clearValidInitialScheduler();
                             }
                             requirements.clearLowerBounds();

src/storm/solver/AbstractEquationSolver.cpp

@@ -176,6 +176,16 @@ namespace storm {
             }
         }
         
+        template<typename ValueType>
+        void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const {
+            STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s).");
+            if (this->hasUpperBound(BoundType::Global)) {
+                upperBoundsVector.assign(upperBoundsVector.size(), this->getUpperBound());
+            } else {
+                upperBoundsVector.assign(this->getUpperBounds().begin(), this->getUpperBounds().end());
+            }
+        }
+        
         template<typename ValueType>
         void AbstractEquationSolver<ValueType>::createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const {
             STORM_LOG_ASSERT(this->hasUpperBound(), "Expecting upper bound(s).");
@@ -187,17 +197,7 @@ namespace storm {
                     upperBoundsVector = std::make_unique<std::vector<ValueType>>(length, this->getUpperBound());
                 }
             } else {
-                if (this->hasUpperBound(BoundType::Global)) {
-                    for (auto& e : *upperBoundsVector) {
-                        e = this->getUpperBound();
-                    }
-                } else {
-                    auto upperBoundsIt = this->getUpperBounds().begin();
-                    for (auto& e : *upperBoundsVector) {
-                        e = *upperBoundsIt;
-                        ++upperBoundsIt;
-                    }
-                }
+                createUpperBoundsVector(*upperBoundsVector);
             }
         }
         

src/storm/solver/AbstractEquationSolver.h

@@ -167,6 +167,7 @@ namespace storm {
             TerminationCondition<ValueType> const& getTerminationCondition() const;
             std::unique_ptr<TerminationCondition<ValueType>> const& getTerminationConditionPointer() const;
             
+            void createUpperBoundsVector(std::vector<ValueType>& upperBoundsVector) const;
             void createUpperBoundsVector(std::unique_ptr<std::vector<ValueType>>& upperBoundsVector, uint64_t length) const;
             void createLowerBoundsVector(std::vector<ValueType>& lowerBoundsVector) const;
 

src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp

@@ -45,7 +45,6 @@ namespace storm {
             switch (solutionMethod) {
                 case MinMaxMethod::ValueIteration: this->solutionMethod = SolutionMethod::ValueIteration; break;
                 case MinMaxMethod::PolicyIteration: this->solutionMethod = SolutionMethod::PolicyIteration; break;
-                case MinMaxMethod::Acyclic: this->solutionMethod = SolutionMethod::Acyclic; break;
                 case MinMaxMethod::RationalSearch: this->solutionMethod = SolutionMethod::RationalSearch; break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver.");
@@ -124,23 +123,26 @@ namespace storm {
         
         template<typename ValueType>
         bool IterativeMinMaxLinearEquationSolver<ValueType>::internalSolveEquations(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
+            bool result = false;
             switch (this->getSettings().getSolutionMethod()) {
                 case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration:
                     if (this->getSettings().getForceSoundness()) {
-                        return solveEquationsSoundValueIteration(dir, x, b);
+                        result = solveEquationsSoundValueIteration(dir, x, b);
                     } else {
-                        return solveEquationsValueIteration(dir, x, b);
+                        result = solveEquationsValueIteration(dir, x, b);
                     }
+                    break;
                 case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration:
-                    return solveEquationsPolicyIteration(dir, x, b);
-                case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::Acyclic:
-                    return solveEquationsAcyclic(dir, x, b);
+                    result = solveEquationsPolicyIteration(dir, x, b);
+                    break;
                 case IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch:
-                    return solveEquationsRationalSearch(dir, x, b);
+                    result = solveEquationsRationalSearch(dir, x, b);
+                    break;
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "This solver does not implement the selected solution method");
             }
-            return false;
+            
+            return result;
         }
         
         template<typename ValueType>
@@ -267,67 +269,44 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             // Start by copying the requirements of the linear equation solver.
             MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements());
 
-            // General requirements.
             if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
-                requirements.requireLowerBounds();
-            } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) {
-                // As rational search needs to approach the solution from below, we cannot start with a valid scheduler hint as we would otherwise do.
-                // Instead, we need to require no end components.
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                if (this->getSettings().getForceSoundness()) {
+                    // Interval iteration requires a unique solution and lower+upper bounds
+                    if (!this->hasUniqueSolution()) {
                         requirements.requireNoEndComponents();
                     }
-                }
-            }
-            
-            // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden
-            if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) {
-                requirements.requireNoEndComponents();
-            }
-            
-            // Guide requirements by whether or not we force soundness.
-            if (this->getSettings().getForceSoundness()) {
-                if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
-                    // Require both bounds now.
                     requirements.requireBounds();
-                    
-                    // If we need to also converge from above, we cannot deal with end components in the notorious cases.
-                    if (equationSystemType == EquationSystemType::UntilProbabilities) {
-                        if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                            requirements.requireNoEndComponents();
-                        }
-                    } else if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                        if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                            requirements.requireNoEndComponents();
-                        }
-                    }
-                } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
-                    if (equationSystemType == EquationSystemType::UntilProbabilities) {
+                } else if (!this->hasUniqueSolution()) { // Traditional value iteration has no requirements if the solution is unique.
+                    // Computing a scheduler is only possible if the solution is unique
+                    if (this->isTrackSchedulerSet()) {
+                        requirements.requireNoEndComponents();
+                    } else {
+                        // As we want the smallest (largest) solution for maximizing (minimizing) equation systems, we have to approach the solution from below (above).
                         if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                            requirements.requireValidInitialScheduler();
+                            requirements.requireLowerBounds();
                         }
-                    } else if (equationSystemType == EquationSystemType::ReachabilityRewards) {
                         if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                            requirements.requireValidInitialScheduler();
+                            requirements.requireUpperBounds();
                         }
                     }
                 }
-            } else {
-                if (equationSystemType == EquationSystemType::UntilProbabilities) {
-                    if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
-                        if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                            requirements.requireValidInitialScheduler();
-                        }
-                    }
-                } else if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                        requirements.requireValidInitialScheduler();
-                    }
+            } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) {
+                // Rational search needs to approach the solution from below.
+                requirements.requireLowerBounds();
+                // The solution needs to be unique in case of minimizing or in cases where we want a scheduler.
+                if (!this->hasUniqueSolution() && (!direction || direction.get() == OptimizationDirection::Minimize || this->isTrackSchedulerSet())) {
+                    requirements.requireNoEndComponents();
                 }
+            } else if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
+                if (!this->hasUniqueSolution()) {
+                    requirements.requireValidInitialScheduler();
+                }
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unsupported technique for iterative MinMax linear equation solver.");
             }
         
             return requirements;
@@ -393,9 +372,8 @@ namespace storm {
                 auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
             }
             
-            // By default, the guarantee that we can provide is that our solution is always less-or-equal than the
-            // actual solution.
-            SolverGuarantee guarantee = SolverGuarantee::LessOrEqual;
+            // By default, we can not provide any guarantee
+            SolverGuarantee guarantee = SolverGuarantee::None;
             
             if (this->hasInitialScheduler()) {
                 // Resolve the nondeterminism according to the initial scheduler.
@@ -417,14 +395,21 @@ namespace storm {
                 }
                 submatrixSolver->solveEquations(x, *auxiliaryRowGroupVector);
                 
-                // If we were given an initial scheduler and are in fact minimizing, our current solution becomes
-                // always greater-or-equal than the actual solution.
-                if (dir == storm::OptimizationDirection::Minimize) {
+                // If we were given an initial scheduler and are maximizing (minimizing), our current solution becomes
+                // always less-or-equal (greater-or-equal) than the actual solution.
+                if (dir == storm::OptimizationDirection::Maximize) {
+                    guarantee = SolverGuarantee::LessOrEqual;
+                } else {
+                    guarantee = SolverGuarantee::GreaterOrEqual;
+                }
+            } else if (!this->hasUniqueSolution()) {
+                if (dir == storm::OptimizationDirection::Maximize) {
+                    this->createLowerBoundsVector(x);
+                    guarantee = SolverGuarantee::LessOrEqual;
+                } else {
+                    this->createUpperBoundsVector(x);
                     guarantee = SolverGuarantee::GreaterOrEqual;
                 }
-            } else {
-                // If no initial scheduler is given, we start from the lower bound.
-                this->createLowerBoundsVector(x);
             }
 
             std::vector<ValueType>* newX = auxiliaryRowGroupVector.get();
@@ -933,83 +918,6 @@ namespace storm {
             return solveEquationsRationalSearchHelper<double>(dir, x, b);
         }
         
-        template<typename ValueType>
-        bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsAcyclic(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
-            uint64_t numGroups = this->A->getRowGroupCount();
-
-            // Allocate memory for the scheduler (if required)
-            if (this->isTrackSchedulerSet()) {
-                if (this->schedulerChoices) {
-                    this->schedulerChoices->resize(numGroups);
-                } else {
-                    this->schedulerChoices = std::vector<uint_fast64_t>(numGroups);
-                }
-            }
-            
-            // We now compute a topological sort of the row groups.
-            // If caching is enabled, it might be possible to obtain this sort from the cache.
-            if (this->isCachingEnabled()) {
-                if (rowGroupOrdering) {
-                    for (auto const& group : *rowGroupOrdering) {
-                        computeOptimalValueForRowGroup(group, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[group] : nullptr);
-                    }
-                    return true;
-                } else {
-                    rowGroupOrdering = std::make_unique<std::vector<uint64_t>>();
-                    rowGroupOrdering->reserve(numGroups);
-                }
-            }
-            
-            auto transposedMatrix = this->A->transpose(true);
-            
-            // We store the groups that have already been processed, i.e., the groups for which x[group] was already set to the correct value.
-            storm::storage::BitVector processedGroups(numGroups, false);
-            // Furthermore, we keep track of all candidate groups for which we still need to check whether this group can be processed now.
-            // A group can be processed if all successors have already been processed.
-            // Notice that the BitVector candidates is considered in a reversed way, i.e., group i is a candidate iff candidates.get(numGroups - i - 1) is true.
-            // This is due to the observation that groups with higher indices usually need to be processed earlier.
-            storm::storage::BitVector candidates(numGroups, true);
-            uint64_t candidate = numGroups - 1;
-            for (uint64_t numCandidates = candidates.size(); numCandidates > 0; --numCandidates) {
-                candidates.set(numGroups - candidate - 1, false);
-                
-                // Check if the candidate row group has an unprocessed successor
-                bool hasUnprocessedSuccessor = false;
-                for (auto const& entry : this->A->getRowGroup(candidate)) {
-                    if (!processedGroups.get(entry.getColumn())) {
-                        hasUnprocessedSuccessor = true;
-                        break;
-                    }
-                }
-                
-                uint64_t nextCandidate = numGroups - candidates.getNextSetIndex(numGroups - candidate - 1 + 1) - 1;
-                
-                if (!hasUnprocessedSuccessor) {
-                    // This candidate can be processed.
-                    processedGroups.set(candidate);
-                    computeOptimalValueForRowGroup(candidate, dir, x, b, this->isTrackSchedulerSet() ? &this->schedulerChoices.get()[candidate] : nullptr);
-                    if (this->isCachingEnabled()) {
-                        rowGroupOrdering->push_back(candidate);
-                    }
-                    
-                    // Add new candidates
-                    for (auto const& predecessorEntry : transposedMatrix.getRow(candidate)) {
-                        uint64_t predecessor = predecessorEntry.getColumn();
-                        if (!candidates.get(numGroups - predecessor - 1)) {
-                            candidates.set(numGroups - predecessor - 1, true);
-                            nextCandidate = std::max(nextCandidate, predecessor);
-                            ++numCandidates;
-                        }
-                    }
-                }
-                candidate = nextCandidate;
-            }
-            
-            assert(candidates.empty());
-            STORM_LOG_THROW(processedGroups.full(), storm::exceptions::InvalidOperationException, "The MinMax equation system is not acyclic.");
-            return true;
-        }
-        
         template<typename ValueType>
         void IterativeMinMaxLinearEquationSolver<ValueType>::computeOptimalValueForRowGroup(uint_fast64_t group, OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b, uint_fast64_t* choice) const {
             uint64_t row = this->A->getRowGroupIndices()[group];

src/storm/solver/IterativeMinMaxLinearEquationSolver.h

@@ -64,7 +64,7 @@ namespace storm {
 
             bool getRelative() const;
             
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
             
         private:
             bool solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;

src/storm/solver/LpMinMaxLinearEquationSolver.cpp

@@ -110,12 +110,12 @@ namespace storm {
         
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements LpMinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             
             MinMaxLinearEquationSolverRequirements requirements;
             
-            // In case we need to retrieve a scheduler, end components are forbidden
-            if (this->isTrackSchedulerSet()) {
+            // In case we need to retrieve a scheduler, the solution has to be unique
+            if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) {
                 requirements.requireNoEndComponents();
             }
             

src/storm/solver/LpMinMaxLinearEquationSolver.h

@@ -18,7 +18,7 @@ namespace storm {
 
             virtual void clearCache() const override;
 
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const override;
             
         private:
             std::unique_ptr<storm::utility::solver::LpSolverFactory<ValueType>> lpSolverFactory;

src/storm/solver/MinMaxLinearEquationSolver.cpp

@@ -19,7 +19,7 @@ namespace storm {
     namespace solver {
         
         template<typename ValueType>
-        MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), cachingEnabled(false), requirementsChecked(false) {
+        MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), uniqueSolution(false), cachingEnabled(false), requirementsChecked(false) {
             // Intentionally left empty.
         }
         
@@ -56,6 +56,16 @@ namespace storm {
             direction = OptimizationDirectionSetting::Unset;
         }
         
+        template<typename ValueType>
+        void MinMaxLinearEquationSolver<ValueType>::setHasUniqueSolution(bool value) {
+            uniqueSolution = value;
+        }
+        
+        template<typename ValueType>
+        bool MinMaxLinearEquationSolver<ValueType>::hasUniqueSolution() const {
+            return uniqueSolution;
+        }
+        
         template<typename ValueType>
         void MinMaxLinearEquationSolver<ValueType>::setTrackScheduler(bool trackScheduler) {
             this->trackScheduler = trackScheduler;
@@ -127,7 +137,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             return MinMaxLinearEquationSolverRequirements();
         }
         
@@ -199,10 +209,11 @@ namespace storm {
         }
         
         template<typename ValueType>
-        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             // Create dummy solver and ask it for requirements.
             std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->create();
-            return solver->getRequirements(equationSystemType, direction);
+            solver->setHasUniqueSolution(hasUniqueSolution);
+            return solver->getRequirements(direction);
         }
         
         template<typename ValueType>

src/storm/solver/MinMaxLinearEquationSolver.h

@@ -12,7 +12,6 @@
 #include "storm/storage/sparse/StateType.h"
 #include "storm/storage/Scheduler.h"
 #include "storm/solver/OptimizationDirection.h"
-#include "storm/solver/EquationSystemType.h"
 #include "storm/solver/MinMaxLinearEquationSolverRequirements.h"
 
 #include "storm/exceptions/InvalidSettingsException.h"
@@ -94,6 +93,16 @@ namespace storm {
              */
             void unsetOptimizationDirection();
             
+            /*!
+             * Sets whether the solution to the min max equation system is known to be unique.
+             */
+            void setHasUniqueSolution(bool value = true);
+            
+            /*!
+             * Retrieves whether the solution to the min max equation system is assumed to be unique
+             */
+            bool hasUniqueSolution() const;
+            
             /*!
              * Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently
              * stored scheduler (if any) is deleted.
@@ -155,7 +164,7 @@ namespace storm {
              * Retrieves the requirements of this solver for solving equations with the current settings. The requirements
              * are guaranteed to be ordered according to their appearance in the SolverRequirement type.
              */
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
             
             /*!
              * Notifies the solver that the requirements for solving equations have been checked. If this has not been
@@ -184,6 +193,9 @@ namespace storm {
             boost::optional<std::vector<uint_fast64_t>> initialScheduler;
             
         private:
+            // Whether the solver can assume that the min-max equation system has a unique solution
+            bool uniqueSolution;
+            
             /// Whether some of the generated data during solver calls should be cached.
             bool cachingEnabled;
             
@@ -212,7 +224,7 @@ namespace storm {
              * Retrieves the requirements of the solver that would be created when calling create() right now. The
              * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type.
              */
-            MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
             void setRequirementsChecked(bool value = true);
             bool isRequirementsCheckedSet() const;
 

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -86,7 +86,7 @@ namespace storm {
         void NativeLinearEquationSolverSettings<ValueType>::setForceSoundness(bool value) {
             forceSoundness = value;
             if (forceSoundness && method != SolutionMethod::Power && method != SolutionMethod::RationalSearch) {
-                STORM_LOG_WARN("To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'.");
+                STORM_LOG_INFO("To guarantee soundness, the equation solving technique has been switched to '" << storm::settings::modules::NativeEquationSolverSettings::LinearEquationMethod::Power << "'.");
                 method = SolutionMethod::Power;
             }
         }

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -86,12 +86,12 @@ namespace storm {
         }
 
         template<storm::dd::DdType DdType, typename ValueType>
-        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(), settings(settings), requirementsChecked(false) {
+        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(), settings(settings), uniqueSolution(false), requirementsChecked(false) {
             // Intentionally left empty.
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), requirementsChecked(false) {
+        SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::SymbolicMinMaxLinearEquationSolver(storm::dd::Add<DdType, ValueType> const& A, storm::dd::Bdd<DdType> const& allRows, storm::dd::Bdd<DdType> const& illegalMask, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables, std::set<storm::expressions::Variable> const& choiceVariables, std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs, std::unique_ptr<SymbolicLinearEquationSolverFactory<DdType, ValueType>>&& linearEquationSolverFactory, SymbolicMinMaxLinearEquationSolverSettings<ValueType> const& settings) : SymbolicEquationSolver<DdType, ValueType>(allRows), A(A), illegalMask(illegalMask), illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())), rowMetaVariables(rowMetaVariables), columnMetaVariables(columnMetaVariables), choiceVariables(choiceVariables), rowColumnMetaVariablePairs(rowColumnMetaVariablePairs), linearEquationSolverFactory(std::move(linearEquationSolverFactory)), settings(settings), uniqueSolution(false), requirementsChecked(false) {
             // Intentionally left empty.
         }
         
@@ -280,11 +280,15 @@ namespace storm {
             // Set up the environment.
             storm::dd::Add<DdType, ValueType> localX;
             
-            // If we were given an initial scheduler, we take its solution as the starting point.
-            if (this->hasInitialScheduler()) {
-                localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
+            if (this->hasUniqueSolution()) {
+                localX = x;
             } else {
-                localX = this->getLowerBoundsVector();
+                // If we were given an initial scheduler, we take its solution as the starting point.
+                if (this->hasInitialScheduler()) {
+                    localX = solveEquationsWithScheduler(this->getInitialScheduler(), x, b);
+                } else {
+                    localX = this->getLowerBoundsVector();
+                }
             }
             
             ValueIterationResult viResult = performValueIteration(dir, localX, b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->settings.getMaximalNumberOfIterations());
@@ -419,39 +423,42 @@ namespace storm {
         }
         
         template<storm::dd::DdType DdType, typename ValueType>
-        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             MinMaxLinearEquationSolverRequirements requirements;
 
             if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
-                if (equationSystemType == EquationSystemType::UntilProbabilities) {
-                    if (!direction || direction.get() == OptimizationDirection::Maximize) {
-                        requirements.requireValidInitialScheduler();
-                    }
-                }
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                        requirements.requireValidInitialScheduler();
-                    }
+                if (!this->hasUniqueSolution()) {
+                    requirements.requireValidInitialScheduler();
                 }
             } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::ValueIteration) {
-                requirements.requireLowerBounds();
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
+                if (!this->hasUniqueSolution()) {
+                    if (!direction || direction.get() == storm::solver::OptimizationDirection::Maximize) {
+                        requirements.requireLowerBounds();
+                    }
+                    if (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize) {
                         requirements.requireValidInitialScheduler();
                     }
                 }
             } else if (this->getSettings().getSolutionMethod() == SymbolicMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::RationalSearch) {
                 requirements.requireLowerBounds();
-                if (equationSystemType == EquationSystemType::ReachabilityRewards) {
-                    if (!direction || direction.get() == OptimizationDirection::Minimize) {
-                        requirements.requireNoEndComponents();
-                    }
+                if (!this->hasUniqueSolution() && (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize)) {
+                    requirements.requireNoEndComponents();
                 }
             }
 
             return requirements;
         }
         
+        template<storm::dd::DdType DdType, typename ValueType>
+        void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::setHasUniqueSolution(bool value) {
+            this->uniqueSolution = value;
+        }
+        
+        template<storm::dd::DdType DdType, typename ValueType>
+        bool SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::hasUniqueSolution() const {
+            return this->uniqueSolution;
+        }
+        
         template<storm::dd::DdType DdType, typename ValueType>
         void SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::setRequirementsChecked(bool value) {
             this->requirementsChecked = value;
@@ -484,9 +491,10 @@ namespace storm {
         }
 
         template<storm::dd::DdType DdType, typename ValueType>
-        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
+        MinMaxLinearEquationSolverRequirements SymbolicMinMaxLinearEquationSolverFactory<DdType, ValueType>::getRequirements(bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
             std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = this->create();
-            return solver->getRequirements(equationSystemType, direction);
+            solver->setHasUniqueSolution(hasUniqueSolution);
+            return solver->getRequirements(direction);
         }
         
         template<storm::dd::DdType DdType, typename ValueType>

src/storm/solver/SymbolicMinMaxLinearEquationSolver.h

@@ -127,7 +127,17 @@ namespace storm {
             /*!
              * Retrieves the requirements of the solver.
              */
-            virtual MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            virtual MinMaxLinearEquationSolverRequirements getRequirements(boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            
+                        /*!
+             * Sets whether the solution to the min max equation system is known to be unique.
+             */
+            void setHasUniqueSolution(bool value = true);
+            
+            /*!
+             * Retrieves whether the solution to the min max equation system is assumed to be unique
+             */
+            bool hasUniqueSolution() const;
             
             /*!
              * Notifies the solver that the requirements for solving equations have been checked. If this has not been
@@ -208,6 +218,9 @@ namespace storm {
             // The settings to use.
             SymbolicMinMaxLinearEquationSolverSettings<ValueType> settings;
             
+            // Whether the solver can assume that the min-max equation system has a unique solution
+            bool uniqueSolution;
+            
             // A flag indicating whether the requirements were checked.
             bool requirementsChecked;
             
@@ -230,7 +243,7 @@ namespace storm {
              * Retrieves the requirements of the solver that would be created when calling create() right now. The
              * requirements are guaranteed to be ordered according to their appearance in the SolverRequirement type.
              */
-            MinMaxLinearEquationSolverRequirements getRequirements(EquationSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
+            MinMaxLinearEquationSolverRequirements getRequirements(bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
             
         private:
             virtual std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> create() const = 0;

src/storm/solver/SymbolicNativeLinearEquationSolver.cpp

@@ -120,6 +120,8 @@ namespace storm {
         storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsJacobi(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
             storm::dd::DdManager<DdType>& manager = this->getDdManager();
 
+            STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (jacobi)");
+
             // Start by computing the Jacobi decomposition of the matrix A.
             storm::dd::Bdd<DdType> diagonal = storm::utility::dd::getRowColumnDiagonal(x.getDdManager(), this->rowColumnMetaVariablePairs);
             diagonal &= this->allRows;
@@ -185,6 +187,7 @@ namespace storm {
         
         template<storm::dd::DdType DdType, typename ValueType>
         storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsPower(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (power)");
             PowerIterationResult result = performPowerIteration(this->getLowerBoundsVector(), b, this->getSettings().getPrecision(), this->getSettings().getRelativeTerminationCriterion(), this->getSettings().getMaximalNumberOfIterations());
             
             if (result.status == SolverStatus::Converged) {
@@ -311,6 +314,7 @@ namespace storm {
         
         template<storm::dd::DdType DdType, typename ValueType>
         storm::dd::Add<DdType, ValueType> SymbolicNativeLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearch(storm::dd::Add<DdType, ValueType> const& x, storm::dd::Add<DdType, ValueType> const& b) const {
+            STORM_LOG_INFO("Solving symbolic linear equation system with NativeLinearEquationSolver (rational search)");
             return solveEquationsRationalSearchHelper<double>(x, b);
         }
         

src/storm/storage/dd/bisimulation/QuotientExtractor.cpp

@@ -271,16 +271,11 @@ namespace storm {
                         std::vector<ValueType> valueVector = extractVectorInternal(vector, this->allSourceVariablesCube, this->nondeterminismOdd);
 
                         // Reorder the values according to the known row permutation.
-                        for (uint64_t position = 0; position < valueVector.size(); ) {
-                            if (rowPermutation[position] != position) {
-                                std::swap(valueVector[position], valueVector[rowPermutation[position]]);
-                                std::swap(rowPermutation[position], rowPermutation[rowPermutation[position]]);
-                            } else {
-                                ++position;
-                            }
+                        std::vector<ValueType> reorderedValues(valueVector.size());
+                        for (uint64_t pos = 0; pos < valueVector.size(); ++pos) {
+                            reorderedValues[pos] = valueVector[rowPermutation[pos]];
                         }
-
-                        return valueVector;
+                        return reorderedValues;
                     }
                 }
                 
@@ -892,7 +887,6 @@ namespace storm {
                     
                     boost::optional<std::vector<ValueType>> quotientStateActionRewards;
                     if (rewardModel.hasStateActionRewards()) {
-                        rewardModel.getStateActionRewardVector().exportToDot("vector.dot");
                         quotientStateActionRewards = sparseExtractor.extractStateActionVector(rewardModel.getStateActionRewardVector());
                     }
                     

src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp

@@ -285,8 +285,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
     
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     
@@ -365,8 +365,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
     
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     

src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
     result = stateAndTransitionRewardModelChecker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(14.666666666666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
 
@@ -181,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(4.2857129064503061, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
 

src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp

@@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
     
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
     
@@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
     
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
     
@@ -280,8 +280,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
     
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     
@@ -360,8 +360,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
     result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
     storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
     
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
-    EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
     
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
     

src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

@@ -76,7 +76,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
 
@@ -98,7 +98,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
     result = stateRewardModelChecker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(7.3333294987678528, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
 
@@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
     result = stateAndTransitionRewardModelChecker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(14.666658997535706, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
 
@@ -178,7 +178,7 @@ TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) {
     result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
 
-    EXPECT_NEAR(4.2857092687973175, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
+    EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 
     formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
 

src/test/storm/solver/GmmxxMinMaxLinearEquationSolverTest.cpp

@@ -19,6 +19,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptions) {
     
     auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
     auto solver = factory.create(A);
+    solver->setHasUniqueSolution();
     ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
     ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());
     
@@ -42,6 +43,8 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithStandardOptionsAndEarlyTerminatio
     
     auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>();
     auto solver = factory.create(A);
+    solver->setLowerBound(0.0);
+    solver->setUpperBound(1.0);
     
     solver->setTerminationCondition(std::make_unique<storm::solver::TerminateIfFilteredExtremumExceedsThreshold<double>>(storm::storage::BitVector(A.getRowGroupCount(), true), false, bound, true));
     ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
@@ -111,6 +114,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) {
 
     auto factory = storm::solver::GmmxxMinMaxLinearEquationSolverFactory<double>(storm::solver::MinMaxMethodSelection::PolicyIteration);
     auto solver = factory.create(A);
+    solver->setHasUniqueSolution();
     
 	ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
 	ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::GmmxxEquationSolverSettings>().getPrecision());

src/test/storm/solver/NativeMinMaxLinearEquationSolverTest.cpp

@@ -20,6 +20,7 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithStandardOptions) {
     
     auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>();
     auto solver = factory.create(A);
+    solver->setHasUniqueSolution();
 
     ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
     
@@ -83,6 +84,8 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) {
 
     auto factory = storm::solver::NativeMinMaxLinearEquationSolverFactory<double>(storm::solver::MinMaxMethodSelection::PolicyIteration);
     auto solver = factory.create(A);
+    solver->setLowerBound(0.0);
+    solver->setUpperBound(1.0);
 
 	ASSERT_NO_THROW(solver->solveEquations(storm::OptimizationDirection::Minimize, x, b));
 	ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());