diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index a199b3781..1b938f717 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -149,8 +149,8 @@ namespace storm {
lowerResultBound = storm::utility::zero<ConstantType>();
upperResultBound = storm::utility::one<ConstantType>();
- // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
- auto req = solverFactory->getRequirements(env, true, boost::none, true);
+ // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations, every induced DTMC has the same graph structure).
+ auto req = solverFactory->getRequirements(env, true, true, boost::none, true);
req.clearBounds();
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
solverFactory->setRequirementsChecked(true);
@@ -188,8 +188,8 @@ namespace storm {
// We only know a lower bound for the result
lowerResultBound = storm::utility::zero<ConstantType>();
- // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
- auto req = solverFactory->getRequirements(env, true, boost::none, true);
+ // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations, every induced DTMC has the same graph structure).
+ auto req = solverFactory->getRequirements(env, true, true, boost::none, true);
req.clearLowerBounds();
if (req.upperBounds()) {
solvingRequiresUpperRewardBounds = true;
@@ -258,6 +258,7 @@ namespace storm {
} else {
auto solver = solverFactory->create(env, parameterLifter->getMatrix());
solver->setHasUniqueSolution();
+ solver->setHasNoEndComponents();
if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
if (upperResultBound) {
solver->setUpperBound(upperResultBound.get());
diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index f813564c2..b1d8ffea9 100644
--- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -310,13 +310,14 @@ namespace storm {
// Create solver.
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir);
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir);
requirements.clearBounds();
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
if (numberOfProbabilisticChoices > 0) {
solver = minMaxLinearEquationSolverFactory.create(env, probMatrix);
solver->setHasUniqueSolution();
+ solver->setHasNoEndComponents();
solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->setRequirementsChecked();
solver->setCachingEnabled(true);
@@ -486,14 +487,15 @@ namespace storm {
}
// Check for requirements of the solver.
- // The solution is unique as we assume non-zeno MAs.
+ // The min-max system has no end components as we assume non-zeno MAs.
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir);
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir);
requirements.clearBounds();
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(env, aProbabilistic);
solver->setHasUniqueSolution();
+ solver->setHasNoEndComponents();
solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->setRequirementsChecked();
solver->setCachingEnabled(true);
@@ -819,12 +821,13 @@ namespace storm {
// Check for requirements of the solver.
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, dir);
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, true, dir);
requirements.clearBounds();
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(underlyingSolverEnvironment, sspMatrix);
solver->setHasUniqueSolution();
+ solver->setHasNoEndComponents();
solver->setLowerBound(storm::utility::zero<ValueType>());
solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end()));
solver->setRequirementsChecked();
@@ -1053,13 +1056,14 @@ namespace storm {
// Check for requirements of the solver.
// The solution is unique as we assume non-zeno MAs.
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, dir);
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, true, true, dir);
requirements.clearLowerBounds();
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
solver = minMaxLinearEquationSolverFactory.create(env, std::move(aProbabilistic));
solver->setLowerBound(storm::utility::zero<ValueType>());
solver->setHasUniqueSolution(true);
+ solver->setHasNoEndComponents(true);
solver->setRequirementsChecked(true);
solver->setCachingEnabled(true);
}
diff --git a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
index 79eae73bb..4f1d97bf8 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
@@ -318,6 +318,7 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
cachedData.minMaxSolver = minMaxSolverFactory.create(env, epochModel.epochMatrix);
cachedData.minMaxSolver->setHasUniqueSolution();
+ cachedData.minMaxSolver->setHasNoEndComponents();
cachedData.minMaxSolver->setTrackScheduler(true);
cachedData.minMaxSolver->setCachingEnabled(true);
auto req = cachedData.minMaxSolver->getRequirements(env);
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
index d43db0d5c..c6a2fa140 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
@@ -301,6 +301,7 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxSolverFactory;
result->solver = minMaxSolverFactory.create(env, PS.toPS);
result->solver->setHasUniqueSolution(true);
+ result->solver->setHasNoEndComponents(true); // Non-zeno MA
result->solver->setTrackScheduler(true);
result->solver->setCachingEnabled(true);
auto req = result->solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, false);
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 3dd8e8988..b2d9e0dbf 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -161,6 +161,50 @@ namespace storm {
return result;
}
+ template <typename ValueType>
+ std::vector<uint64_t> computeValidInitialScheduler(storm::storage::SparseMatrix<ValueType> const& matrix, storm::storage::BitVector const& rowsWithSumLessOne) {
+ std::vector<uint64_t> result(matrix.getRowGroupCount());
+ auto const& groups = matrix.getRowGroupIndices();
+ auto backwardsTransitions = matrix.transpose(true);
+ storm::storage::BitVector processedStates(result.size(), false);
+ for (uint64_t state = 0; state < result.size(); ++state) {
+ if (rowsWithSumLessOne.getNextSetIndex(groups[state]) < groups[state + 1]) {
+ result[state] = rowsWithSumLessOne.getNextSetIndex(groups[state]) - groups[state];
+ processedStates.set(state, true);
+ }
+ }
+ std::vector<uint64_t> stack(processedStates.begin(), processedStates.end());
+ while (!stack.empty()) {
+ uint64_t current = stack.back();
+ stack.pop_back();
+ STORM_LOG_ASSERT(processedStates.get(current), "states on the stack shall be processed.");
+ for (auto const& entry : backwardsTransitions.getRow(current)) {
+ uint64_t pred = entry.getColumn();
+ if (!processedStates.get(pred)) {
+ // Find a choice that leads to a processed state
+ uint64_t predChoice = groups[pred];
+ bool foundSuccessor = false;
+ for (; predChoice < groups[pred + 1]; ++predChoice) {
+ for (auto const& predEntry : matrix.getRow(predChoice)) {
+ if (processedStates.get(predEntry.getColumn())) {
+ foundSuccessor = true;
+ break;
+ }
+ }
+ if (foundSuccessor) {
+ break;
+ }
+ }
+ STORM_LOG_ASSERT(foundSuccessor && predChoice < groups[pred + 1], "Predecessor of a processed state should have a processed successor");
+ result[pred] = predChoice - groups[pred];
+ processedStates.set(pred, true);
+ stack.push_back(pred);
+ }
+ }
+ }
+ return result;
+ }
+
template <class SparseModelType>
void StandardPcaaWeightVectorChecker<SparseModelType>::unboundedWeightedPhase(Environment const& env, std::vector<ValueType> const& weightedRewardVector, std::vector<ValueType> const& weightVector) {
@@ -187,6 +231,10 @@ namespace storm {
if (solver->hasUpperBound()) {
req.clearUpperBounds();
}
+ if (req.validInitialScheduler()) {
+ solver->setInitialScheduler(computeValidInitialScheduler(ecQuotient->matrix, ecQuotient->rowsWithSumLessOne));
+ req.clearValidInitialScheduler();
+ }
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
solver->setRequirementsChecked(true);
diff --git a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
index 7cb054574..d1755ef38 100644
--- a/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
@@ -146,22 +146,23 @@ 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;
+ // If we minimize, we know that the solution to the equation system has no end components
+ bool hasNoEndComponents = dir == storm::solver::OptimizationDirection::Minimize;
// Check for requirements of the solver early so we can adjust the maybe state computation accordingly.
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir);
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, hasNoEndComponents, hasNoEndComponents, dir);
storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements;
SolverRequirementsData<ValueType> solverRequirementsData;
bool extendMaybeStates = false;
if (clearedRequirements.hasEnabledRequirement()) {
- if (clearedRequirements.noEndComponents()) {
- STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
+ if (clearedRequirements.uniqueSolution()) {
+ STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires a unique solution.");
extendMaybeStates = true;
- clearedRequirements.clearNoEndComponents();
+ clearedRequirements.clearUniqueSolution();
+ hasNoEndComponents = true;
}
- if (clearedRequirements.validInitialScheduler()) {
+ if (clearedRequirements.validInitialScheduler() && !hasNoEndComponents) {
STORM_LOG_DEBUG("Scheduling valid scheduler computation, because the solver requires it.");
clearedRequirements.clearValidInitialScheduler();
}
@@ -210,8 +211,6 @@ namespace storm {
// Eliminate the end components and remove the states that are not interesting (target or non-filter).
eliminateEndComponentsAndExtendedStatesUntilProbabilities(explicitRepresentation, solverRequirementsData, targetStates);
- // The solution becomes unique after end components have been eliminated.
- uniqueSolution = true;
} else {
// Then compute the vector that contains the one-step probabilities to a state with probability 1 for all
// maybe states.
@@ -240,8 +239,9 @@ namespace storm {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(explicitRepresentation.first));
- // Set whether the equation system will have a unique solution
- solver->setHasUniqueSolution(uniqueSolution);
+ // Set whether the equation system will have a unique solution / no end components
+ solver->setHasUniqueSolution(hasNoEndComponents);
+ solver->setHasNoEndComponents(hasNoEndComponents);
if (solverRequirementsData.initialScheduler) {
solver->setInitialScheduler(std::move(solverRequirementsData.initialScheduler.get()));
@@ -251,7 +251,7 @@ namespace storm {
solver->solveEquations(env, dir, x, explicitRepresentation.second);
// If we included some target and non-filter states in the ODD, we need to expand the result from the solver.
- if (requirements.noEndComponents() && solverRequirementsData.ecInformation) {
+ if (requirements.uniqueSolution() && solverRequirementsData.ecInformation) {
std::vector<ValueType> extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits());
solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x);
x = std::move(extendedVector);
@@ -543,17 +543,20 @@ namespace storm {
// 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;
+ bool hasNoEndComponents = dir == storm::solver::OptimizationDirection::Maximize;
+ bool hasUniqueSolution = hasNoEndComponents;
// Check for requirements of the solver this early so we can adapt the maybe states accordingly.
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> linearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, uniqueSolution, dir);
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(env, hasUniqueSolution, hasNoEndComponents, dir);
storm::solver::MinMaxLinearEquationSolverRequirements clearedRequirements = requirements;
bool extendMaybeStates = false;
if (clearedRequirements.hasEnabledRequirement()) {
- if (clearedRequirements.noEndComponents()) {
+ if (clearedRequirements.uniqueSolution()) {
STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires it.");
extendMaybeStates = true;
- clearedRequirements.clearNoEndComponents();
+ clearedRequirements.clearUniqueSolution();
+ hasUniqueSolution = true;
+ // There might still be end components in which reward is collected.
}
if (clearedRequirements.validInitialScheduler()) {
STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
@@ -611,11 +614,15 @@ namespace storm {
storm::storage::BitVector targetStates = computeTargetStatesForReachabilityRewardsFromExplicitRepresentation(explicitRepresentation.first);
solverRequirementsData.properMaybeStates = ~targetStates;
- if (requirements.noEndComponents()) {
+ if (requirements.uniqueSolution()) {
+ STORM_LOG_THROW(!requirements.validInitialScheduler(), storm::exceptions::UncheckedRequirementException, "The underlying solver requires a unique solution and an initial valid scheduler. This is currently not supported for expected reward properties.");
+ // eliminate the end components with reward 0.
+ // Note that this may also compute the oneStepTargetProbabilities if upper bounds are required.
eliminateEndComponentsAndTargetStatesReachabilityRewards(explicitRepresentation, solverRequirementsData, targetStates, requirements.upperBounds());
// The solution becomes unique after end components have been eliminated.
- uniqueSolution = true;
- } else {
+ hasUniqueSolution = true;
+ }
+ else {
if (requirements.validInitialScheduler()) {
// Compute a valid initial scheduler.
solverRequirementsData.initialScheduler = computeValidInitialSchedulerForReachabilityRewards<ValueType>(explicitRepresentation.first, solverRequirementsData.properMaybeStates, targetStates);
@@ -637,8 +644,9 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env);
- // Set whether the equation system will have a unique solution
- solver->setHasUniqueSolution(uniqueSolution);
+ // Set whether the equation system will have a unique solution / no end components
+ solver->setHasUniqueSolution(hasUniqueSolution);
+ solver->setHasNoEndComponents(hasNoEndComponents);
// If the solver requires upper bounds, compute them now.
if (requirements.upperBounds()) {
@@ -657,7 +665,7 @@ namespace storm {
solver->solveEquations(env, dir, x, explicitRepresentation.second);
// If we eliminated end components, we need to extend the solution vector.
- if (requirements.noEndComponents() && solverRequirementsData.ecInformation) {
+ if (requirements.uniqueSolution() && solverRequirementsData.ecInformation) {
std::vector<ValueType> extendedVector(solverRequirementsData.properMaybeStates.getNumberOfSetBits());
solverRequirementsData.ecInformation.get().setValues(extendedVector, solverRequirementsData.properMaybeStates, x);
x = std::move(extendedVector);
diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index d8bb7dc32..dcadd10f8 100644
--- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -205,7 +205,7 @@ namespace storm {
template<typename ValueType>
struct SparseMdpHintType {
- SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false) {
+ SparseMdpHintType() : eliminateEndComponents(false), computeUpperBounds(false), uniqueSolution(false), noEndComponents(false) {
// Intentionally left empty.
}
@@ -265,6 +265,10 @@ namespace storm {
return uniqueSolution;
}
+ bool hasNoEndComponents() const {
+ return noEndComponents;
+ }
+
boost::optional<std::vector<uint64_t>> schedulerHint;
boost::optional<std::vector<ValueType>> valueHint;
boost::optional<ValueType> lowerResultBound;
@@ -273,6 +277,7 @@ namespace storm {
bool eliminateEndComponents;
bool computeUpperBounds;
bool uniqueSolution;
+ bool noEndComponents;
};
template<typename ValueType>
@@ -329,29 +334,36 @@ namespace storm {
SparseMdpHintType<ValueType> computeHints(Environment const& env, 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, bool produceScheduler, 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)
+ // There are no end components if we minimize until probabilities or
+ // maximize reachability rewards or if the hint tells us so.
+ result.noEndComponents = (dir == storm::solver::OptimizationDirection::Minimize && type == SolutionType::UntilProbabilities)
|| (dir == storm::solver::OptimizationDirection::Maximize && type == SolutionType::ExpectedRewards)
|| (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
+ // If there are no end components, the solution is unique. (Note that the other direction does not hold,
+ // e.g., end components in which infinite reward is collected.
+ result.uniqueSolution = result.hasNoEndComponents();
+
// Check for requirements of the solver.
bool hasSchedulerHint = hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint();
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, dir, hasSchedulerHint, produceScheduler);
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(env, result.uniqueSolution, result.noEndComponents, dir, hasSchedulerHint, produceScheduler);
if (requirements.hasEnabledRequirement()) {
// If the solver still requires no end-components, we have to eliminate them later.
- if (requirements.noEndComponents()) {
+ if (requirements.uniqueSolution()) {
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.");
+ STORM_LOG_DEBUG("Scheduling EC elimination, because the solver requires a unique solution.");
result.eliminateEndComponents = true;
// If end components have been eliminated we can assume a unique solution.
result.uniqueSolution = true;
- requirements.clearNoEndComponents();
+ requirements.clearUniqueSolution();
+ // If we compute until probabilities, we can even assume the absence of end components.
+ // Note that in the case of minimizing expected rewards there might still be end components in which reward is collected.
+ result.noEndComponents = (type == SolutionType::UntilProbabilities);
}
- // If the solver requires an initial scheduler, compute one now.
- if (requirements.validInitialScheduler()) {
+ // If the solver requires an initial scheduler, compute one now. Note that any scheduler is valid if there are no end components.
+ if (requirements.validInitialScheduler() && !result.noEndComponents) {
STORM_LOG_DEBUG("Computing valid scheduler, because the solver requires it.");
result.schedulerHint = computeValidSchedulerHint(env, type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates);
requirements.clearValidInitialScheduler();
@@ -429,6 +441,7 @@ namespace storm {
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(env, std::move(goal), minMaxLinearEquationSolverFactory, std::move(submatrix));
solver->setRequirementsChecked();
solver->setHasUniqueSolution(hint.hasUniqueSolution());
+ solver->setHasNoEndComponents(hint.hasNoEndComponents());
if (hint.hasLowerResultBound()) {
solver->setLowerBound(hint.getLowerResultBound());
}
@@ -1348,7 +1361,7 @@ namespace storm {
// Check for requirements of the solver.
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
- storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, goal.direction());
+ storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(underlyingSolverEnvironment, true, true, goal.direction());
requirements.clearBounds();
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
@@ -1359,6 +1372,7 @@ namespace storm {
solver->setLowerBound(storm::utility::zero<ValueType>());
solver->setUpperBound(*std::max_element(lraValuesForEndComponents.begin(), lraValuesForEndComponents.end()));
solver->setHasUniqueSolution();
+ solver->setHasNoEndComponents();
solver->setRequirementsChecked();
solver->solveEquations(underlyingSolverEnvironment, sspResult, b);
diff --git a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
index f52d7eb17..212151e5e 100644
--- a/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
@@ -82,10 +82,10 @@ namespace storm {
requirements.clearValidInitialScheduler();
}
requirements.clearBounds();
- if (requirements.noEndComponents()) {
+ if (requirements.uniqueSolution()) {
// Check whether there are end components
if (storm::utility::graph::performProb0E(model, transitionMatrix.notZero(), maybeStates, !maybeStates && model.getReachableStates()).isZero()) {
- requirements.clearNoEndComponents();
+ requirements.clearUniqueSolution();
}
}
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
@@ -253,10 +253,10 @@ namespace storm {
requirements.clearValidInitialScheduler();
}
requirements.clearLowerBounds();
- if (requirements.noEndComponents()) {
+ if (requirements.uniqueSolution()) {
// Check whether there are end components
if (storm::utility::graph::performProb0E(model, transitionMatrixBdd, maybeStates, !maybeStates && model.getReachableStates()).isZero()) {
- requirements.clearNoEndComponents();
+ requirements.clearUniqueSolution();
}
}
STORM_LOG_THROW(!requirements.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + requirements.getEnabledRequirementsAsString() + " not checked.");
diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp
index e8b059f32..f48253fca 100644
--- a/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp
+++ b/src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp
@@ -140,6 +140,7 @@ namespace storm {
storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType> minMaxLinearEquationSolverFactory;
minMaxSolver = minMaxLinearEquationSolverFactory.create(env, epochModel.epochMatrix);
minMaxSolver->setHasUniqueSolution();
+ minMaxSolver->setHasNoEndComponents();
minMaxSolver->setOptimizationDirection(dir);
minMaxSolver->setCachingEnabled(true);
minMaxSolver->setTrackScheduler(true);
diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
index becaa1d17..37f9c1ab5 100644
--- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
@@ -241,7 +241,7 @@ namespace storm {
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();
+ requirements.requireUniqueSolution();
} 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) {
@@ -255,7 +255,7 @@ namespace storm {
} else if (method == MinMaxMethod::IntervalIteration) {
// Interval iteration requires a unique solution and lower+upper bounds
if (!this->hasUniqueSolution()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
requirements.requireBounds();
} else if (method == MinMaxMethod::RationalSearch) {
@@ -263,22 +263,22 @@ namespace storm {
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();
+ requirements.requireUniqueSolution();
}
} else if (method == MinMaxMethod::PolicyIteration) {
- if (!this->hasUniqueSolution()) {
+ // The initial scheduler shall not select an end component
+ if (!this->hasNoEndComponents()) {
requirements.requireValidInitialScheduler();
}
} else if (method == MinMaxMethod::SoundValueIteration) {
if (!this->hasUniqueSolution()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
requirements.requireBounds(false);
} else if (method == MinMaxMethod::ViToPi) {
- // Since we want to use value iteration to extract an initial scheduler, it helps to eliminate all end components first.
- // TODO: We might get around this, as the initial value iteration scheduler is only a heuristic.
+ // Since we want to use value iteration to extract an initial scheduler, the solution has to be unique.
if (!this->hasUniqueSolution()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "Unsupported technique for iterative MinMax linear equation solver.");
diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
index 78bc75752..2b371aae3 100644
--- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp
@@ -117,7 +117,7 @@ namespace storm {
// In case we need to retrieve a scheduler, the solution has to be unique
if (!this->hasUniqueSolution() && this->isTrackSchedulerSet()) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
requirements.requireBounds(false);
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp
index be724ea0d..df0fef614 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.cpp
+++ b/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), uniqueSolution(false), cachingEnabled(false), requirementsChecked(false) {
+ MinMaxLinearEquationSolver<ValueType>::MinMaxLinearEquationSolver(OptimizationDirectionSetting direction) : direction(direction), trackScheduler(false), uniqueSolution(false), noEndComponents(false), cachingEnabled(false), requirementsChecked(false) {
// Intentionally left empty.
}
@@ -57,7 +57,17 @@ namespace storm {
template<typename ValueType>
bool MinMaxLinearEquationSolver<ValueType>::hasUniqueSolution() const {
- return uniqueSolution;
+ return uniqueSolution || noEndComponents;
+ }
+
+ template<typename ValueType>
+ void MinMaxLinearEquationSolver<ValueType>::setHasNoEndComponents(bool value) {
+ noEndComponents = value;
+ }
+
+ template<typename ValueType>
+ bool MinMaxLinearEquationSolver<ValueType>::hasNoEndComponents() const {
+ return noEndComponents;
}
template<typename ValueType>
@@ -161,11 +171,12 @@ namespace storm {
}
template<typename ValueType>
- MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env, bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection> const& direction, bool hasInitialScheduler, bool trackScheduler) const {
+ MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(Environment const& env, bool hasUniqueSolution, bool hasNoEndComponents, boost::optional<storm::solver::OptimizationDirection> const& direction, bool hasInitialScheduler, bool trackScheduler) const {
// Create dummy solver and ask it for requirements.
std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> solver = this->create(env);
solver->setTrackScheduler(trackScheduler);
solver->setHasUniqueSolution(hasUniqueSolution);
+ solver->setHasNoEndComponents(hasNoEndComponents);
return solver->getRequirements(env, direction, hasInitialScheduler);
}
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h
index 7ca89dfb9..5ab51dc95 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.h
+++ b/src/storm/solver/MinMaxLinearEquationSolver.h
@@ -76,10 +76,24 @@ namespace storm {
void setHasUniqueSolution(bool value = true);
/*!
- * Retrieves whether the solution to the min max equation system is assumed to be unique
+ * Retrieves whether the solution to the min max equation system is assumed to be unique.
+ * Note that having no end components implies that the solution is unique. Thus, this also returns true if
+ * `hasNoEndComponents()` returns true.
+ * Also note that a unique solution does not imply the absence of ECs, because, e.g. in Rmin properties there
+ * can still be ECs in which infinite reward is collected.
*/
bool hasUniqueSolution() const;
+ /*!
+ * Sets whether the min max equation system is known to not have any end components
+ */
+ void setHasNoEndComponents(bool value = true);
+
+ /*!
+ * Retrieves whether the min max equation system is known to not have any end components
+ */
+ bool hasNoEndComponents() const;
+
/*!
* Sets whether schedulers are generated when solving equation systems. If the argument is false, the currently
* stored scheduler (if any) is deleted.
@@ -173,6 +187,9 @@ namespace storm {
/// Whether the solver can assume that the min-max equation system has a unique solution
bool uniqueSolution;
+ /// Whether the solver can assume that the min-max equation system has no end components
+ bool noEndComponents;
+
/// Whether some of the generated data during solver calls should be cached.
bool cachingEnabled;
@@ -194,7 +211,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(Environment const& env, bool hasUniqueSolution = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool hasInitialScheduler = false, bool trackScheduler = false) const;
+ MinMaxLinearEquationSolverRequirements getRequirements(Environment const& env, bool hasUniqueSolution = false, bool hasNoEndComponents = false, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none, bool hasInitialScheduler = false, bool trackScheduler = false) const;
void setRequirementsChecked(bool value = true);
bool isRequirementsCheckedSet() const;
diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
index e16bbdf54..3e5e867ab 100644
--- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
+++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
@@ -7,8 +7,8 @@ namespace storm {
// Intentionally left empty.
}
- MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireNoEndComponents(bool critical) {
- noEndComponentsRequirement.enable(critical);
+ MinMaxLinearEquationSolverRequirements& MinMaxLinearEquationSolverRequirements::requireUniqueSolution(bool critical) {
+ uniqueSolutionRequirement.enable(critical);
return *this;
}
@@ -33,8 +33,8 @@ namespace storm {
return *this;
}
- SolverRequirement const& MinMaxLinearEquationSolverRequirements::noEndComponents() const {
- return noEndComponentsRequirement;
+ SolverRequirement const& MinMaxLinearEquationSolverRequirements::uniqueSolution() const {
+ return uniqueSolutionRequirement;
}
SolverRequirement const& MinMaxLinearEquationSolverRequirements::validInitialScheduler() const {
@@ -51,16 +51,15 @@ namespace storm {
SolverRequirement const& MinMaxLinearEquationSolverRequirements::get(Element const& element) const {
switch (element) {
- case Element::NoEndComponents: return noEndComponents(); break;
+ case Element::UniqueSolution: return uniqueSolution(); break;
case Element::ValidInitialScheduler: return validInitialScheduler(); break;
case Element::LowerBounds: return lowerBounds(); break;
case Element::UpperBounds: return upperBounds(); break;
}
}
- void MinMaxLinearEquationSolverRequirements::clearNoEndComponents() {
- noEndComponentsRequirement.clear();
- validInitialSchedulerRequirement.clear();
+ void MinMaxLinearEquationSolverRequirements::clearUniqueSolution() {
+ uniqueSolutionRequirement.clear();
}
void MinMaxLinearEquationSolverRequirements::clearValidInitialScheduler() {
@@ -81,20 +80,20 @@ namespace storm {
}
bool MinMaxLinearEquationSolverRequirements::hasEnabledRequirement() const {
- return noEndComponentsRequirement || validInitialSchedulerRequirement || lowerBoundsRequirement || upperBoundsRequirement;
+ return uniqueSolutionRequirement || validInitialSchedulerRequirement || lowerBoundsRequirement || upperBoundsRequirement;
}
bool MinMaxLinearEquationSolverRequirements::hasEnabledCriticalRequirement() const {
- return noEndComponentsRequirement.isCritical() || validInitialSchedulerRequirement.isCritical() || lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical();
+ return uniqueSolutionRequirement.isCritical() || validInitialSchedulerRequirement.isCritical() || lowerBoundsRequirement.isCritical() || upperBoundsRequirement.isCritical();
}
std::string MinMaxLinearEquationSolverRequirements::getEnabledRequirementsAsString() const {
std::string res = "[";
bool first = true;
- if (noEndComponents()) {
+ if (uniqueSolution()) {
if (!first) { res += ", "; } else {first = false;}
- res += "NoEndComponents";
- if (noEndComponents().isCritical()) {
+ res += "UniqueSolution";
+ if (uniqueSolution().isCritical()) {
res += "(mandatory)";
}
}
diff --git a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h
index 06ba623c1..38f2f1849 100644
--- a/src/storm/solver/MinMaxLinearEquationSolverRequirements.h
+++ b/src/storm/solver/MinMaxLinearEquationSolverRequirements.h
@@ -15,7 +15,7 @@ namespace storm {
// Requirements that are related to the graph structure of the system. Note that the requirements in this
// category are to be interpreted incrementally in the following sense: whenever the system has no end
// components then automatically both requirements are fulfilled.
- NoEndComponents,
+ UniqueSolution,
ValidInitialScheduler,
// Requirements that are related to bounds for the actual solution.
@@ -27,19 +27,19 @@ namespace storm {
MinMaxLinearEquationSolverRequirements(LinearEquationSolverRequirements const& linearEquationSolverRequirements = LinearEquationSolverRequirements());
- MinMaxLinearEquationSolverRequirements& requireNoEndComponents(bool critical = true);
+ MinMaxLinearEquationSolverRequirements& requireUniqueSolution(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireValidInitialScheduler(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireLowerBounds(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireUpperBounds(bool critical = true);
MinMaxLinearEquationSolverRequirements& requireBounds(bool critical = true);
- SolverRequirement const& noEndComponents() const;
+ SolverRequirement const& uniqueSolution() const;
SolverRequirement const& validInitialScheduler() const;
SolverRequirement const& lowerBounds() const;
SolverRequirement const& upperBounds() const;
SolverRequirement const& get(Element const& element) const;
- void clearNoEndComponents();
+ void clearUniqueSolution();
void clearValidInitialScheduler();
void clearLowerBounds();
void clearUpperBounds();
@@ -54,7 +54,7 @@ namespace storm {
std::string getEnabledRequirementsAsString() const;
private:
- SolverRequirement noEndComponentsRequirement;
+ SolverRequirement uniqueSolutionRequirement;
SolverRequirement validInitialSchedulerRequirement;
SolverRequirement lowerBoundsRequirement;
SolverRequirement upperBoundsRequirement;
diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
index c54df3acf..2ba997ed8 100644
--- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
@@ -455,7 +455,7 @@ namespace storm {
} else if (method == MinMaxMethod::RationalSearch) {
requirements.requireLowerBounds();
if (!this->hasUniqueSolution() && (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize)) {
- requirements.requireNoEndComponents();
+ requirements.requireUniqueSolution();
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidEnvironmentException, "The selected min max technique is not supported by this solver.");
diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
index 998c9d782..d98902694 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
@@ -181,6 +181,7 @@ namespace storm {
}
this->sccSolver->setMatrix(*this->A);
this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution());
+ this->sccSolver->setHasNoEndComponents(this->hasNoEndComponents());
this->sccSolver->setBoundsFromOtherSolver(*this);
this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet());
if (this->hasInitialScheduler()) {
@@ -194,10 +195,12 @@ namespace storm {
if (req.lowerBounds() && this->hasLowerBound()) {
req.clearLowerBounds();
}
-
- // If all requirements of the underlying solver have been passed as requirements to the calling site, we can
- // assume that the system has no end components if the underlying solver requires this.
- req.clearNoEndComponents();
+ if (req.validInitialScheduler() && this->hasInitialScheduler()) {
+ req.clearValidInitialScheduler();
+ }
+ if (req.uniqueSolution() && this->hasUniqueSolution()) {
+ req.clearUniqueSolution();
+ }
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
this->sccSolver->setRequirementsChecked(true);
@@ -217,6 +220,7 @@ namespace storm {
this->sccSolver->setCachingEnabled(true);
}
this->sccSolver->setHasUniqueSolution(this->hasUniqueSolution());
+ this->sccSolver->setHasNoEndComponents(this->hasNoEndComponents());
this->sccSolver->setTrackScheduler(this->isTrackSchedulerSet());
// SCC Matrix
@@ -269,6 +273,9 @@ namespace storm {
if (req.validInitialScheduler() && this->hasInitialScheduler()) {
req.clearValidInitialScheduler();
}
+ if (req.uniqueSolution() && this->hasUniqueSolution()) {
+ req.clearUniqueSolution();
+ }
STORM_LOG_THROW(!req.hasEnabledCriticalRequirement(), storm::exceptions::UncheckedRequirementException, "Solver requirements " + req.getEnabledRequirementsAsString() + " not checked.");
this->sccSolver->setRequirementsChecked(true);
@@ -291,7 +298,7 @@ namespace storm {
template<typename ValueType>
MinMaxLinearEquationSolverRequirements TopologicalMinMaxLinearEquationSolver<ValueType>::getRequirements(Environment const& env, boost::optional<storm::solver::OptimizationDirection> const& direction, bool const& hasInitialScheduler) const {
// Return the requirements of the underlying solver
- return GeneralMinMaxLinearEquationSolverFactory<ValueType>().getRequirements(getEnvironmentForUnderlyingSolver(env), this->hasUniqueSolution(), direction, hasInitialScheduler);
+ return GeneralMinMaxLinearEquationSolverFactory<ValueType>().getRequirements(getEnvironmentForUnderlyingSolver(env), this->hasUniqueSolution(), this->hasNoEndComponents(), direction, hasInitialScheduler, this->isTrackSchedulerSet());
}
template<typename ValueType>
diff --git a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp
index 725590bc8..ef565f946 100644
--- a/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp
+++ b/src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp
@@ -149,6 +149,7 @@ namespace {
auto factory = storm::solver::GeneralMinMaxLinearEquationSolverFactory<ValueType>();
auto solver = factory.create(this->env(), A);
solver->setHasUniqueSolution(true);
+ solver->setHasNoEndComponents(true);
solver->setBounds(this->parseNumber("0"), this->parseNumber("2"));
storm::solver::MinMaxLinearEquationSolverRequirements req = solver->getRequirements(this->env());
req.clearBounds();