sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

computing unbounded until on MDPs with the sparse helper now respects solver requirements

tempestpy_adaptions
dehnert 7 years ago
parent
569b0122b8
commit
74eeaa7f81
7 changed files with 66 additions and 21 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/storm/modelchecker/hints/ModelCheckerHint.h
  2. 42
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  3. 2
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
  4. 13
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  5. 2
      src/storm/solver/IterativeMinMaxLinearEquationSolver.h
  6. 6
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  7. 20
      src/storm/solver/MinMaxLinearEquationSolver.h

2
src/storm/modelchecker/hints/ModelCheckerHint.h
View File

@ -7,14 +7,12 @@ namespace storm {
template<typename ValueType>
class ExplicitModelCheckerHint;
/*!
* This class contains information that might accelerate the model checking process.
* @note The model checker has to make sure whether a given hint is actually applicable and thus a hint might be ignored.
*/
class ModelCheckerHint {
public:
ModelCheckerHint() = default;
// Returns true iff this hint does not contain any information

42
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -157,9 +157,33 @@ namespace storm {
// obtain hint information if possible
bool skipEcWithinMaybeStatesCheck = goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
std::pair<boost::optional<std::vector<ValueType>>, boost::optional<std::vector<uint_fast64_t>>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, boost::none, hint, skipEcWithinMaybeStatesCheck);
// Now compute the results for the maybeStates
std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero<ValueType>(), storm::utility::one<ValueType>(), storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
if (!requirements.empty()) {
std::unique_ptr<storm::storage::Scheduler<ValueType>> validScheduler;
for (auto const& requirement : requirements) {
if (requirement == storm::solver::MinMaxLinearEquationSolverRequirement::ValidSchedulerHint) {
// If the solver requires a valid scheduler (a scheduler that produces non-zero
// probabilities for all maybe states), we need to compute such a scheduler now.
validScheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(maybeStates.size());
storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, phiStates, statesWithProbability1, *validScheduler, boost::none);
STORM_LOG_WARN_COND(hintInformation.second, "A scheduler hint was provided, but the solver requires a valid scheduler hint. The hint will be ignored.");
hintInformation.second = std::vector<uint_fast64_t>(maybeStates.getNumberOfSetBits());
auto maybeIt = maybeStates.begin();
for (auto& choice : hintInformation.second.get()) {
choice = validScheduler->getChoice(*maybeIt).getDeterministicChoice();
}
} else {
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
}
}
}
// Now compute the results for the maybe states.
std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.first);
@ -252,13 +276,9 @@ namespace storm {
}
template<typename ValueType>
std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> SparseMdpPrctlHelper<ValueType>::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>>&& hintValues, boost::optional<std::vector<uint_fast64_t>>&& hintChoices, boost::optional<ValueType> const& lowerResultBound, boost::optional<ValueType> const& upperResultBound, storm::solver::MinMaxLinearEquationSolverSystemType const& equationSystemType) {
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements(equationSystemType);
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> SparseMdpPrctlHelper<ValueType>::computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>>&& hintValues, boost::optional<std::vector<uint_fast64_t>>&& hintChoices, boost::optional<ValueType> const& lowerResultBound, boost::optional<ValueType> const& upperResultBound) {
// Set up the solver
// Set up the solver.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix);
solver->setRequirementsChecked();
if (lowerResultBound) {
@ -278,7 +298,7 @@ namespace storm {
// Solve the corresponding system of equations.
solver->solveEquations(x, b);
// If requested, a scheduler was produced
// If requested, return the requested scheduler.
if (produceScheduler) {
return std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>>(std::move(x), std::move(solver->getSchedulerChoices()));
} else {
@ -460,7 +480,7 @@ namespace storm {
std::pair<boost::optional<std::vector<ValueType>>, boost::optional<std::vector<uint_fast64_t>>> hintInformation = extractHintInformationForMaybeStates(transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck);
// Now compute the results for the maybeStates
std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero<ValueType>(), boost::none, storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards);
std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> resultForMaybeStates = computeValuesOnlyMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, std::move(hintInformation.first), std::move(hintInformation.second), storm::utility::zero<ValueType>(), boost::none);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.first);

2
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
View File

@ -41,7 +41,7 @@ namespace storm {
static std::pair<boost::optional<std::vector<ValueType>>, boost::optional<std::vector<uint_fast64_t>>> extractHintInformationForMaybeStates(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, boost::optional<storm::storage::BitVector> const& selectedChoices, ModelCheckerHint const& hint, bool skipECWithinMaybeStatesCheck);
static std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>>&& hintValues = boost::none, boost::optional<std::vector<uint_fast64_t>>&& hintChoices = boost::none, boost::optional<ValueType> const& lowerResultBound = boost::none, boost::optional<ValueType> const& upperResultBound = boost::none, storm::solver::MinMaxLinearEquationSolverSystemType const& equationSystemType = storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
static std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>> computeValuesOnlyMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<std::vector<ValueType>>&& hintValues = boost::none, boost::optional<std::vector<uint_fast64_t>>&& hintChoices = boost::none, boost::optional<ValueType> const& lowerResultBound = boost::none, boost::optional<ValueType> const& upperResultBound = boost::none);
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());

13
src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
View File

@ -216,6 +216,19 @@ namespace storm {
bool IterativeMinMaxLinearEquationSolver<ValueType>::getRelative() const {
return this->getSettings().getRelativeTerminationCriterion();
}
template<typename ValueType>
std::vector<MinMaxLinearEquationSolverRequirement> IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
std::vector<MinMaxLinearEquationSolverRequirement> requirements;
if (equationSystemType == MinMaxLinearEquationSolverSystemType::UntilProbabilities) {
if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
if (!direction || direction.get() == OptimizationDirection::Maximize) {
requirements.push_back(MinMaxLinearEquationSolverRequirement::ValidSchedulerHint);
}
}
}
return requirements;
}
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {

2
src/storm/solver/IterativeMinMaxLinearEquationSolver.h
View File

@ -50,6 +50,8 @@ namespace storm {
ValueType getPrecision() const;
bool getRelative() const;
virtual std::vector<MinMaxLinearEquationSolverRequirement> getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, 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;
bool solveEquationsValueIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const;

6
src/storm/solver/MinMaxLinearEquationSolver.cpp
View File

@ -138,7 +138,7 @@ namespace storm {
}
template<typename ValueType>
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolver<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const {
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolver<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
return std::vector<MinMaxLinearEquationSolverRequirement>();
}
@ -210,10 +210,10 @@ namespace storm {
}
template<typename ValueType>
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const {
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, 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);
return solver->getRequirements(equationSystemType, direction);
}
template<typename ValueType>

20
src/storm/solver/MinMaxLinearEquationSolver.h
View File

@ -29,10 +29,17 @@ namespace storm {
StochasticShortestPath
};
// Possible requirements of solvers. Note that the order must not be changed as it shall be guaranteed that the
// solver announces requirements in the order in which they appear in this list.
enum class MinMaxLinearEquationSolverRequirement {
// Graph requirements.
NoEndComponents,
// Hint requirements.
ValidSchedulerHint,
ValidValueHint,
NoEndComponents,
// Global bounds requirements.
GlobalUpperBound,
GlobalLowerBound
};
@ -174,9 +181,10 @@ namespace storm {
bool hasSchedulerHint() const;
/*!
* Retrieves the requirements of this solver for solving equations with the current settings.
* 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 std::vector<MinMaxLinearEquationSolverRequirement> getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const;
virtual std::vector<MinMaxLinearEquationSolverRequirement> getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, 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
@ -235,7 +243,11 @@ namespace storm {
MinMaxMethod const& getMinMaxMethod() const;
std::vector<MinMaxLinearEquationSolverRequirement> getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType) const;
/*!
* 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.
*/
std::vector<MinMaxLinearEquationSolverRequirement> getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
void setRequirementsChecked(bool value = true);
bool isRequirementsCheckedSet() const;

Write Preview
Loading…
Cancel
Save