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

Sparse MDP helper now also respects solver requirements for reachability rewards

tempestpy_adaptions
dehnert 7 years ago
parent
74eeaa7f81
commit
4c5cdfeafc
9 changed files with 328 additions and 175 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. 6
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  2. 10
      src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
  3. 333
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  4. 4
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h
  5. 2
      src/storm/settings/modules/EigenEquationSolverSettings.cpp
  6. 27
      src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp
  7. 2
      src/storm/solver/IterativeMinMaxLinearEquationSolver.h
  8. 19
      src/storm/solver/MinMaxLinearEquationSolver.cpp
  9. 100
      src/storm/solver/MinMaxLinearEquationSolver.h

6
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -89,7 +89,7 @@ namespace storm {
}
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic);
@ -376,7 +376,7 @@ namespace storm {
std::vector<ValueType> x(numberOfSspStates);
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath);
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath);
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix);
@ -584,7 +584,7 @@ namespace storm {
std::vector<ValueType> b = probabilisticChoiceRewards;
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards);
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards);
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
auto solver = minMaxLinearEquationSolverFactory.create(std::move(aProbabilistic));

10
src/storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp
View File

@ -72,15 +72,15 @@ namespace storm {
// Finally cut away all columns targeting non-maybe states.
submatrix *= maybeStatesAdd.swapVariables(model.getRowColumnMetaVariablePairs());
// Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
// Translate the symbolic matrix/vector to their explicit representations and solve the equation system.
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities);
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
// Create the solution vector.
std::vector<ValueType> x(maybeStates.getNonZeroCount(), storm::utility::zero<ValueType>());
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitRepresentation.first));
solver->setRequirementsChecked();
@ -274,7 +274,7 @@ namespace storm {
std::pair<storm::storage::SparseMatrix<ValueType>, std::vector<ValueType>> explicitRepresentation = submatrix.toMatrixVector(subvector, std::move(rowGroupSizes), model.getNondeterminismVariables(), odd, odd);
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards);
storm::solver::MinMaxLinearEquationSolverRequirements requirements = linearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards);
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
// Now solve the resulting equation system.

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

@ -85,6 +85,203 @@ namespace storm {
return result;
}
template<typename ValueType>
std::vector<uint_fast64_t> computeValidSchedulerHint(storm::solver::MinMaxLinearEquationSolverSystemType const& type, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& filterStates, storm::storage::BitVector const& targetStates) {
std::unique_ptr<storm::storage::Scheduler<ValueType>> validScheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(maybeStates.size());
if (type == storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities) {
storm::utility::graph::computeSchedulerProbGreater0E(transitionMatrix, backwardTransitions, filterStates, targetStates, *validScheduler, boost::none);
} else if (type == storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards) {
storm::utility::graph::computeSchedulerProb1E(maybeStates | targetStates, transitionMatrix, backwardTransitions, filterStates, targetStates, *validScheduler);
} else {
STORM_LOG_ASSERT(false, "Unexpected equation system type.");
}
// Extract the relevant parts of the scheduler for the solver.
std::vector<uint_fast64_t> schedulerHint(maybeStates.getNumberOfSetBits());
auto maybeIt = maybeStates.begin();
for (auto& choice : schedulerHint) {
choice = validScheduler->getChoice(*maybeIt).getDeterministicChoice();
++maybeIt;
}
return schedulerHint;
}
template<typename ValueType>
struct SparseMdpHintType {
bool hasSchedulerHint() const {
return static_cast<bool>(schedulerHint);
}
bool hasValueHint() const {
return static_cast<bool>(valueHint);
}
bool hasLowerResultBound() const {
return static_cast<bool>(lowerResultBound);
}
ValueType const& getLowerResultBound() const {
return lowerResultBound.get();
}
bool hasUpperResultBound() const {
return static_cast<bool>(upperResultBound);
}
ValueType const& getUpperResultBound() const {
return upperResultBound.get();
}
std::vector<uint64_t>& getSchedulerHint() {
return schedulerHint.get();
}
std::vector<ValueType>& getValueHint() {
return valueHint.get();
}
boost::optional<std::vector<uint64_t>> schedulerHint;
boost::optional<std::vector<ValueType>> valueHint;
boost::optional<ValueType> lowerResultBound;
boost::optional<ValueType> upperResultBound;
};
template<typename ValueType>
void extractHintInformationForMaybeStates(SparseMdpHintType<ValueType>& hintStorage, 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) {
// Deal with scheduler hint.
if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint()) {
if (hintStorage.hasSchedulerHint()) {
STORM_LOG_WARN("A scheduler hint was provided, but the solver requires a specific one. The provided scheduler hint will be ignored.");
} else {
auto const& schedulerHint = hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint();
std::vector<uint64_t> hintChoices;
// The scheduler hint is only applicable if it induces no BSCC consisting of maybe states.
bool hintApplicable;
if (!skipECWithinMaybeStatesCheck) {
hintChoices.reserve(maybeStates.size());
for (uint_fast64_t state = 0; state < maybeStates.size(); ++state) {
hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice());
}
hintApplicable = storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hintChoices), maybeStates, ~maybeStates).full();
} else {
hintApplicable = true;
}
if (hintApplicable) {
// Compute the hint w.r.t. the given subsystem.
hintChoices.clear();
hintChoices.reserve(maybeStates.getNumberOfSetBits());
for (auto const& state : maybeStates) {
uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice();
if (selectedChoices) {
uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state];
uint_fast64_t lastChoice = firstChoice + hintChoice;
hintChoice = 0;
for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice; choice = selectedChoices->getNextSetIndex(choice + 1)) {
++hintChoice;
}
}
hintChoices.push_back(hintChoice);
}
hintStorage.schedulerHint = std::move(hintChoices);
}
}
}
// Deal with solution value hint. Only applicable if there are no End Components consisting of maybe states.
if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint() && (skipECWithinMaybeStatesCheck || hintStorage.hasSchedulerHint() || storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) {
hintStorage.valueHint = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint<ValueType>().getResultHint(), maybeStates);
}
}
template<typename ValueType>
SparseMdpHintType<ValueType> computeHints(storm::solver::MinMaxLinearEquationSolverSystemType const& type, ModelCheckerHint const& hint, storm::OptimizationDirection const& dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& targetStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<storm::storage::BitVector> const& selectedChoices = boost::none) {
SparseMdpHintType<ValueType> result;
// Check for requirements of the solver.
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(type);
if (!(hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates()) && !requirements.empty()) {
if (requirements.requires(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler)) {
STORM_LOG_DEBUG("Computing valid scheduler hint, because the solver requires it.");
result.schedulerHint = computeValidSchedulerHint(type, transitionMatrix, backwardTransitions, maybeStates, phiStates, targetStates);
requirements.set(storm::solver::MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler, false);
}
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "There are unchecked requirements of the solver.");
}
bool skipEcWithinMaybeStatesCheck = dir == storm::OptimizationDirection::Minimize || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint<ValueType>().getNoEndComponentsInMaybeStates());
extractHintInformationForMaybeStates(result, transitionMatrix, backwardTransitions, maybeStates, selectedChoices, hint, skipEcWithinMaybeStatesCheck);
result.lowerResultBound = storm::utility::zero<ValueType>();
if (type == storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities) {
result.upperResultBound = storm::utility::one<ValueType>();
} else if (type == storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards) {
// Intentionally left empty.
} else {
STORM_LOG_ASSERT(false, "Unexpected equation system type.");
}
return result;
}
template<typename ValueType>
struct MaybeStateResult {
MaybeStateResult(std::vector<ValueType>&& values) : values(std::move(values)) {
// Intentionally left empty.
}
bool hasScheduler() const {
return static_cast<bool>(scheduler);
}
std::vector<uint64_t> const& getScheduler() const {
return scheduler.get();
}
std::vector<ValueType> const& getValues() const {
return values;
}
std::vector<ValueType> values;
boost::optional<std::vector<uint64_t>> scheduler;
};
template<typename ValueType>
MaybeStateResult<ValueType> computeValuesForMaybeStates(storm::solver::SolveGoal const& goal, storm::storage::SparseMatrix<ValueType> const& submatrix, std::vector<ValueType> const& b, bool produceScheduler, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, SparseMdpHintType<ValueType>& hint) {
// Set up the solver.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix);
solver->setRequirementsChecked();
if (hint.hasLowerResultBound()) {
solver->setLowerBound(hint.getLowerResultBound());
}
if (hint.hasUpperResultBound()) {
solver->setUpperBound(hint.getUpperResultBound());
}
if (hint.hasSchedulerHint()) {
solver->setInitialScheduler(std::move(hint.getSchedulerHint()));
}
solver->setTrackScheduler(produceScheduler);
// Initialize the solution vector.
std::vector<ValueType> x = hint.hasValueHint() ? std::move(hint.getValueHint()) : std::vector<ValueType>(submatrix.getRowGroupCount(), hint.hasLowerResultBound() ? hint.getLowerResultBound() : storm::utility::zero<ValueType>());
// Solve the corresponding system of equations.
solver->solveEquations(x, b);
// Create result.
MaybeStateResult<ValueType> result(std::move(x));
// If requested, return the requested scheduler.
if (produceScheduler) {
result.scheduler = std::move(solver->getSchedulerChoices());
}
return result;
}
template<typename ValueType>
MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<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) {
STORM_LOG_THROW(!(qualitative && produceScheduler), storm::exceptions::InvalidSettingsException, "Cannot produce scheduler when performing qualitative model checking only.");
@ -154,42 +351,17 @@ namespace storm {
// the accumulated probability of going from state i to some 'yes' state.
std::vector<ValueType> b = transitionMatrix.getConstrainedRowGroupSumVector(maybeStates, statesWithProbability1);
// 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);
// 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.");
}
}
}
// Obtain proper hint information either from the provided hint or from requirements of the solver.
SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::MinMaxLinearEquationSolverSystemType::UntilProbabilities, hint, goal.direction(), transitionMatrix, backwardTransitions, maybeStates, phiStates, statesWithProbability1, minMaxLinearEquationSolverFactory);
// 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>());
MaybeStateResult<ValueType> resultForMaybeStates = computeValuesForMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.first);
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.getValues());
if (produceScheduler) {
std::vector<uint_fast64_t> const& subChoices = resultForMaybeStates.second.get();
std::vector<uint_fast64_t> const& subChoices = resultForMaybeStates.getScheduler();
auto subChoiceIt = subChoices.begin();
for (auto maybeState : maybeStates) {
scheduler->setChoice(*subChoiceIt, maybeState);
@ -222,89 +394,6 @@ namespace storm {
return MDPSparseModelCheckingHelperReturnType<ValueType>(std::move(result), std::move(scheduler));
}
template<typename ValueType>
std::pair<boost::optional<std::vector<ValueType>>, boost::optional<std::vector<uint_fast64_t>>> SparseMdpPrctlHelper<ValueType>::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) {
// Scheduler hint
boost::optional<std::vector<uint_fast64_t>> subSchedulerChoices;
if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasSchedulerHint()) {
auto const& schedulerHint = hint.template asExplicitModelCheckerHint<ValueType>().getSchedulerHint();
std::vector<uint_fast64_t> hintChoices;
// the scheduler hint is only applicable if it induces no BSCC consisting of maybestates
bool hintApplicable;
if (!skipECWithinMaybeStatesCheck) {
hintChoices.reserve(maybeStates.size());
for (uint_fast64_t state = 0; state < maybeStates.size(); ++state) {
hintChoices.push_back(schedulerHint.getChoice(state).getDeterministicChoice());
}
hintApplicable = storm::utility::graph::performProb1(transitionMatrix.transposeSelectedRowsFromRowGroups(hintChoices), maybeStates, ~maybeStates).full();
} else {
hintApplicable = true;
}
if (hintApplicable) {
// Compute the hint w.r.t. the given subsystem
hintChoices.clear();
hintChoices.reserve(maybeStates.getNumberOfSetBits());
for (auto const& state : maybeStates) {
uint_fast64_t hintChoice = schedulerHint.getChoice(state).getDeterministicChoice();
if (selectedChoices) {
uint_fast64_t firstChoice = transitionMatrix.getRowGroupIndices()[state];
uint_fast64_t lastChoice = firstChoice + hintChoice;
hintChoice = 0;
for (uint_fast64_t choice = selectedChoices->getNextSetIndex(firstChoice); choice < lastChoice; choice = selectedChoices->getNextSetIndex(choice + 1)) {
++hintChoice;
}
}
hintChoices.push_back(hintChoice);
}
subSchedulerChoices = std::move(hintChoices);
}
}
// Solution value hint
boost::optional<std::vector<ValueType>> subValues;
// The result hint is only applicable if there are no End Components consisting of maybestates
if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().hasResultHint() &&
(skipECWithinMaybeStatesCheck || subSchedulerChoices ||
storm::utility::graph::performProb1A(transitionMatrix, transitionMatrix.getRowGroupIndices(), backwardTransitions, maybeStates, ~maybeStates).full())) {
subValues = storm::utility::vector::filterVector(hint.template asExplicitModelCheckerHint<ValueType>().getResultHint(), maybeStates);
}
return std::make_pair(std::move(subValues), std::move(subSchedulerChoices));
}
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) {
// Set up the solver.
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, minMaxLinearEquationSolverFactory, submatrix);
solver->setRequirementsChecked();
if (lowerResultBound) {
solver->setLowerBound(lowerResultBound.get());
}
if (upperResultBound) {
solver->setUpperBound(upperResultBound.get());
}
if (hintChoices) {
solver->setSchedulerHint(std::move(hintChoices.get()));
}
solver->setTrackScheduler(produceScheduler);
// Initialize the solution vector.
std::vector<ValueType> x = hintValues ? std::move(hintValues.get()) : std::vector<ValueType>(submatrix.getRowGroupCount(), lowerResultBound ? lowerResultBound.get() : storm::utility::zero<ValueType>());
// Solve the corresponding system of equations.
solver->solveEquations(x, b);
// 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 {
return std::pair<std::vector<ValueType>, boost::optional<std::vector<uint_fast64_t>>>(std::move(x), boost::none);
}
}
template<typename ValueType>
MDPSparseModelCheckingHelperReturnType<ValueType> SparseMdpPrctlHelper<ValueType>::computeUntilProbabilities(OptimizationDirection dir, 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) {
@ -462,6 +551,7 @@ namespace storm {
// Prepare matrix and vector for the equation system.
storm::storage::SparseMatrix<ValueType> submatrix;
std::vector<ValueType> b;
// Remove rows and columns from the original transition probability matrix for states whose reward values are already known.
// If there are infinity states, we additionaly have to remove choices of maybeState that lead to infinity
boost::optional<storm::storage::BitVector> selectedChoices; // if not given, all maybeState choices are selected
@ -475,18 +565,17 @@ namespace storm {
storm::utility::vector::filterVectorInPlace(b, *selectedChoices);
}
// 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, selectedChoices, hint, skipEcWithinMaybeStatesCheck);
// Obtain proper hint information either from the provided hint or from requirements of the solver.
SparseMdpHintType<ValueType> hintInformation = computeHints(storm::solver::MinMaxLinearEquationSolverSystemType::ReachabilityRewards, hint, goal.direction(), transitionMatrix, backwardTransitions, maybeStates, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true), targetStates, minMaxLinearEquationSolverFactory, selectedChoices);
// 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);
// Now compute the results for the maybe states.
MaybeStateResult<ValueType> resultForMaybeStates = computeValuesForMaybeStates(goal, submatrix, b, produceScheduler, minMaxLinearEquationSolverFactory, hintInformation);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.first);
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, resultForMaybeStates.getValues());
if (produceScheduler) {
std::vector<uint_fast64_t> const& subChoices = resultForMaybeStates.second.get();
std::vector<uint_fast64_t> const& subChoices = resultForMaybeStates.getScheduler();
auto subChoiceIt = subChoices.begin();
if (selectedChoices) {
for (auto maybeState : maybeStates) {
@ -678,7 +767,7 @@ namespace storm {
storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice, numberOfSspStates, numberOfSspStates);
// Check for requirements of the solver.
std::vector<storm::solver::MinMaxLinearEquationSolverRequirement> requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath);
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::MinMaxLinearEquationSolverSystemType::StochasticShortestPath);
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
std::vector<ValueType> sspResult(numberOfSspStates);

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

@ -39,10 +39,6 @@ namespace storm {
static MDPSparseModelCheckingHelperReturnType<ValueType> computeUntilProbabilities(OptimizationDirection dir, 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());
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);
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());
static std::vector<ValueType> computeGloballyProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, bool useMecBasedTechnique = false);

2
src/storm/settings/modules/EigenEquationSolverSettings.cpp
View File

@ -101,7 +101,7 @@ namespace storm {
// This list does not include the precision, because this option is shared with other modules.
bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isMaximalIterationCountSet();
STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "eigen is not selected as the preferred equation solver, so setting options for eigen might have no effect.");
STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver() == storm::solver::EquationSolverType::Eigen || !optionsSet, "Eigen is not selected as the preferred equation solver, so setting options for eigen might have no effect.");
return true;
}

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

@ -108,7 +108,7 @@ namespace storm {
template<typename ValueType>
bool IterativeMinMaxLinearEquationSolver<ValueType>::solveEquationsPolicyIteration(OptimizationDirection dir, std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
// Create the initial scheduler.
std::vector<storm::storage::sparse::state_type> scheduler = this->hasSchedulerHint() ? this->choicesHint.get() : std::vector<storm::storage::sparse::state_type>(this->A->getRowGroupCount());
std::vector<storm::storage::sparse::state_type> scheduler = this->hasInitialScheduler() ? this->getInitialScheduler() : std::vector<storm::storage::sparse::state_type>(this->A->getRowGroupCount());
// Get a vector for storing the right-hand side of the inner equation system.
if(!auxiliaryRowGroupVector) {
@ -135,9 +135,6 @@ namespace storm {
uint64_t iterations = 0;
do {
// Solve the equation system for the 'DTMC'.
// FIXME: we need to remove the 0- and 1- states to make the solution unique.
// HOWEVER: if we start with a valid scheduler, then we will never get an illegal one, because staying
// within illegal MECs will never strictly improve the value. Is this true?
solver->solveEquations(x, subB);
// Go through the multiplication result and see whether we can improve any of the choices.
@ -218,15 +215,23 @@ namespace storm {
}
template<typename ValueType>
std::vector<MinMaxLinearEquationSolverRequirement> IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
std::vector<MinMaxLinearEquationSolverRequirement> requirements;
MinMaxLinearEquationSolverRequirements IterativeMinMaxLinearEquationSolver<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
MinMaxLinearEquationSolverRequirements requirements;
if (equationSystemType == MinMaxLinearEquationSolverSystemType::UntilProbabilities) {
if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
if (!direction || direction.get() == OptimizationDirection::Maximize) {
requirements.push_back(MinMaxLinearEquationSolverRequirement::ValidSchedulerHint);
requirements.set(MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler);
}
}
} else if (equationSystemType == MinMaxLinearEquationSolverSystemType::ReachabilityRewards) {
if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::SolutionMethod::PolicyIteration) {
if (!direction || direction.get() == OptimizationDirection::Minimize) {
requirements.set(MinMaxLinearEquationSolverRequirements::Element::ValidInitialScheduler);
}
}
}
return requirements;
}
@ -246,11 +251,11 @@ namespace storm {
auxiliaryRowGroupVector = std::make_unique<std::vector<ValueType>>(this->A->getRowGroupCount());
}
if (this->hasSchedulerHint()) {
// Resolve the nondeterminism according to the scheduler hint
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(this->choicesHint.get(), true);
if (this->hasInitialScheduler()) {
// Resolve the nondeterminism according to the initial scheduler.
storm::storage::SparseMatrix<ValueType> submatrix = this->A->selectRowsFromRowGroups(this->getInitialScheduler(), true);
submatrix.convertToEquationSystem();
storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->choicesHint.get(), this->A->getRowGroupIndices(), b);
storm::utility::vector::selectVectorValues<ValueType>(*auxiliaryRowGroupVector, this->getInitialScheduler(), this->A->getRowGroupIndices(), b);
// Solve the resulting equation system.
// Note that the linEqSolver might consider a slightly different interpretation of "equalModuloPrecision". Hence, we iteratively increase its precision.

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

@ -50,7 +50,7 @@ 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;
virtual MinMaxLinearEquationSolverRequirements 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;

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

@ -128,18 +128,23 @@ namespace storm {
}
template<typename ValueType>
void MinMaxLinearEquationSolver<ValueType>::setSchedulerHint(std::vector<uint_fast64_t>&& choices) {
choicesHint = std::move(choices);
void MinMaxLinearEquationSolver<ValueType>::setInitialScheduler(std::vector<uint_fast64_t>&& choices) {
initialScheduler = std::move(choices);
}
template<typename ValueType>
bool MinMaxLinearEquationSolver<ValueType>::hasSchedulerHint() const {
return choicesHint.is_initialized();
bool MinMaxLinearEquationSolver<ValueType>::hasInitialScheduler() const {
return static_cast<bool>(initialScheduler);
}
template<typename ValueType>
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolver<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
return std::vector<MinMaxLinearEquationSolverRequirement>();
std::vector<uint_fast64_t> const& MinMaxLinearEquationSolver<ValueType>::getInitialScheduler() const {
return initialScheduler.get();
}
template<typename ValueType>
MinMaxLinearEquationSolverRequirements MinMaxLinearEquationSolver<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
return MinMaxLinearEquationSolverRequirements();
}
template<typename ValueType>
@ -210,7 +215,7 @@ namespace storm {
}
template<typename ValueType>
std::vector<MinMaxLinearEquationSolverRequirement> MinMaxLinearEquationSolverFactory<ValueType>::getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction) const {
MinMaxLinearEquationSolverRequirements 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, direction);

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

@ -29,19 +29,72 @@ 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,
// Global bounds requirements.
GlobalUpperBound,
GlobalLowerBound
class MinMaxLinearEquationSolverRequirements {
public:
enum class Element {
NoEndComponents, NoZeroRewardEndComponents, ValidInitialScheduler, GlobalLowerBound, GlobalUpperBound
};
MinMaxLinearEquationSolverRequirements() : noEndComponents(false), noZeroRewardEndComponents(false), validInitialScheduler(false), globalLowerBound(false), globalUpperBound(false) {
// Intentionally left empty.
}
MinMaxLinearEquationSolverRequirements& setNoEndComponents(bool value = true) {
noEndComponents = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setNoZeroRewardEndComponents(bool value = true) {
noZeroRewardEndComponents = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setValidInitialScheduler(bool value = true) {
validInitialScheduler = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setGlobalLowerBound(bool value = true) {
globalLowerBound = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& setGlobalUpperBound(bool value = true) {
globalUpperBound = value;
return *this;
}
MinMaxLinearEquationSolverRequirements& set(Element const& element, bool value = true) {
switch (element) {
case Element::NoEndComponents: noEndComponents = value; break;
case Element::NoZeroRewardEndComponents: noZeroRewardEndComponents = value; break;
case Element::ValidInitialScheduler: validInitialScheduler = value; break;
case Element::GlobalLowerBound: globalLowerBound = value; break;
case Element::GlobalUpperBound: globalUpperBound = value; break;
}
return *this;
}
bool requires(Element const& element) {
switch (element) {
case Element::NoEndComponents: return noEndComponents; break;
case Element::NoZeroRewardEndComponents: return noZeroRewardEndComponents; break;
case Element::ValidInitialScheduler: return validInitialScheduler; break;
case Element::GlobalLowerBound: return globalLowerBound; break;
case Element::GlobalUpperBound: return globalUpperBound; break;
}
}
bool empty() const {
return !noEndComponents && !noZeroRewardEndComponents && !validInitialScheduler && !globalLowerBound && !globalUpperBound;
}
private:
bool noEndComponents;
bool noZeroRewardEndComponents;
bool validInitialScheduler;
bool globalLowerBound;
bool globalUpperBound;
};
/*!
@ -171,20 +224,25 @@ namespace storm {
void setBounds(ValueType const& lower, ValueType const& upper);
/*!
* Sets a scheduler that might be considered by the solver as an initial guess
* Sets a valid initial scheduler that is required by some solvers (see requirements of solvers).
*/
void setInitialScheduler(std::vector<uint_fast64_t>&& choices);
/*!
* Returns true iff an initial scheduler is set.
*/
void setSchedulerHint(std::vector<uint_fast64_t>&& choices);
bool hasInitialScheduler() const;
/*!
* Returns true iff a scheduler hint was defined
* Retrieves the initial scheduler if one was set.
*/
bool hasSchedulerHint() const;
std::vector<uint_fast64_t> const& getInitialScheduler() const;
/*!
* 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, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
virtual MinMaxLinearEquationSolverRequirements 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
@ -215,8 +273,8 @@ namespace storm {
// An upper bound if one was set.
boost::optional<ValueType> upperBound;
// Scheduler choices that might be considered by the solver as an initial guess
boost::optional<std::vector<uint_fast64_t>> choicesHint;
// A scheduler that can be used by solvers that require a valid initial scheduler.
boost::optional<std::vector<uint_fast64_t>> initialScheduler;
private:
/// Whether some of the generated data during solver calls should be cached.
@ -247,7 +305,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.
*/
std::vector<MinMaxLinearEquationSolverRequirement> getRequirements(MinMaxLinearEquationSolverSystemType const& equationSystemType, boost::optional<storm::solver::OptimizationDirection> const& direction = boost::none) const;
MinMaxLinearEquationSolverRequirements 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