Browse Source

MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler.

Renamed the 'hasNoEndComponents' solver requirement to 'hasUniqueSolution' as this is the actual thing we require for, e.g. sound value iteration.
tempestpy_adaptions
Tim Quatmann 6 years ago
parent
commit
bc623d1203
  1. 9
      src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
  2. 14
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  3. 1
      src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
  4. 1
      src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
  5. 48
      src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
  6. 52
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  7. 36
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  8. 8
      src/storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  9. 1
      src/storm/modelchecker/prctl/helper/rewardbounded/EpochModel.cpp
  10. 16
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  11. 2
      src/storm/solver/LpMinMaxLinearEquationSolver.cpp
  12. 17
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  13. 21
      src/storm/solver/MinMaxLinearEquationSolver.h
  14. 25
      src/storm/solver/MinMaxLinearEquationSolverRequirements.cpp
  15. 10
      src/storm/solver/MinMaxLinearEquationSolverRequirements.h
  16. 2
      src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp
  17. 17
      src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
  18. 1
      src/test/storm/solver/MinMaxLinearEquationSolverTest.cpp

9
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());

14
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);
}

1
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);

1
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);

48
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);

52
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);

36
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);

8
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.");

1
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);

16
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.");

2
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);

17
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);
}

21
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;

25
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)";
}
}

10
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;

2
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.");

17
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>

1
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();

|||||||
100:0
Loading…
Cancel
Save