21template<storm::dd::DdType DdType,
typename ValueType>
27template<storm::dd::DdType DdType,
typename ValueType>
30 std::set<storm::expressions::Variable>
const& rowMetaVariables, std::set<storm::expressions::Variable>
const& columnMetaVariables,
31 std::set<storm::expressions::Variable>
const& choiceVariables,
32 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>>
const& rowColumnMetaVariablePairs,
36 illegalMask(illegalMask),
37 illegalMaskAdd(illegalMask.ite(A.getDdManager().getConstant(
storm::utility::infinity<ValueType>()), A.getDdManager().template getAddZero<ValueType>())),
38 rowMetaVariables(rowMetaVariables),
39 columnMetaVariables(columnMetaVariables),
40 choiceVariables(choiceVariables),
41 rowColumnMetaVariablePairs(rowColumnMetaVariablePairs),
42 linearEquationSolverFactory(
std::move(linearEquationSolverFactory)),
43 uniqueSolution(false),
44 requirementsChecked(false) {
48template<storm::dd::DdType DdType,
typename ValueType>
53 if (isExactMode && method != MinMaxMethod::RationalSearch) {
56 "Selecting 'rational search' as the solution technique to guarantee exact results. If you want to override this, please explicitly specify a "
58 method = MinMaxMethod::RationalSearch;
60 STORM_LOG_WARN(
"The selected solution method does not guarantee exact results.");
63 if (method != MinMaxMethod::ValueIteration && method != MinMaxMethod::PolicyIteration && method != MinMaxMethod::RationalSearch) {
64 STORM_LOG_WARN(
"Selected method is not supported for this solver, switching to value iteration.");
65 method = MinMaxMethod::ValueIteration;
71template<storm::dd::DdType DdType,
typename ValueType>
77 "The requirements of the solver have not been marked as checked. Please provide the appropriate check or mark the requirements "
78 "as checked (if applicable).");
80 switch (getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value)) {
81 case MinMaxMethod::ValueIteration:
82 return solveEquationsValueIteration(env, dir, x, b);
84 case MinMaxMethod::PolicyIteration:
85 return solveEquationsPolicyIteration(env, dir, x, b);
87 case MinMaxMethod::RationalSearch:
88 return solveEquationsRationalSearch(env, dir, x, b);
91 STORM_LOG_THROW(
false, storm::exceptions::InvalidEnvironmentException,
"The selected min max technique is not supported by this solver.");
96template<storm::dd::DdType DdType,
typename ValueType>
101 bool relativeTerminationCriterion, uint64_t maximalIterations)
const {
104 uint64_t iterations = 0;
114 if (dir == storm::solver::OptimizationDirection::Minimize) {
115 tmp += illegalMaskAdd;
138 return SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::ValueIterationResult(status, iterations, localX);
141template<storm::dd::DdType DdType,
typename ValueType>
148 if (dir == storm::solver::OptimizationDirection::Minimize) {
149 tmp += illegalMaskAdd;
158template<storm::dd::DdType DdType,
typename ValueType>
159template<
typename RationalType,
typename ImpreciseType>
165 for (uint64_t p = 1; p < precision; ++p) {
167 isSolution = rationalSolver.
isSolution(dir, sharpenedX, rationalB);
177template<storm::dd::DdType DdType,
typename ValueType>
178template<
typename RationalType,
typename ImpreciseType>
180 Environment
const& env,
OptimizationDirection dir, SymbolicMinMaxLinearEquationSolver<DdType, RationalType>
const& rationalSolver,
188 uint64_t overallIterations = 0;
189 uint64_t valueIterationInvocations = 0;
190 ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
191 uint64_t maxIter = env.solver().minMax().getMaximalNumberOfIterations();
192 bool relative = env.solver().minMax().getRelativeTerminationCriterion();
195 typename SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType>::ValueIterationResult viResult =
196 impreciseSolver.performValueIteration(dir, currentX, b, storm::utility::convertNumber<ImpreciseType, ValueType>(precision), relative, maxIter);
198 ++valueIterationInvocations;
199 STORM_LOG_TRACE(
"Completed " << valueIterationInvocations <<
" value iteration invocations, the last one with precision " << precision
200 <<
" completed in " << viResult.iterations <<
" iterations.");
203 overallIterations += viResult.iterations;
207 storm::utility::convertNumber<uint64_t>(
storm::utility::ceil(storm::utility::log10<ValueType>(storm::utility::one<ValueType>() / precision)));
209 bool isSolution =
false;
210 sharpenedX = sharpen<RationalType, ImpreciseType>(dir, p, rationalSolver, viResult.values, rationalB, isSolution);
215 currentX = viResult.values;
216 precision /= storm::utility::convertNumber<ValueType, uint64_t>(10);
228 STORM_LOG_INFO(
"Iterative solver (rational search) converged in " << overallIterations <<
" iterations.");
230 STORM_LOG_WARN(
"Iterative solver (rational search) did not converge in " << overallIterations <<
" iterations.");
236template<storm::dd::DdType DdType,
typename ValueType>
237template<
typename ImpreciseType>
239SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(Environment
const& env,
243 return solveEquationsRationalSearchHelper<ValueType, ValueType>(env, dir, *
this, *
this, b, this->getLowerBoundsVector(), b);
246template<storm::dd::DdType DdType,
typename ValueType>
247template<
typename ImpreciseType>
249SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(Environment
const& env,
254 SymbolicMinMaxLinearEquationSolver<DdType, storm::RationalNumber> rationalSolver(
255 this->A.template toValueType<storm::RationalNumber>(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables,
256 this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique<GeneralSymbolicLinearEquationSolverFactory<DdType, storm::RationalNumber>>());
259 solveEquationsRationalSearchHelper<storm::RationalNumber, ImpreciseType>(env, dir, rationalSolver, *
this, rationalB, this->getLowerBoundsVector(), b);
260 return rationalResult.template toValueType<ValueType>();
263template<storm::dd::DdType DdType,
typename ValueType>
264template<
typename ImpreciseType>
266SymbolicMinMaxLinearEquationSolver<DdType, ValueType>::solveEquationsRationalSearchHelper(Environment
const& env,
274 impreciseX = this->getLowerBoundsVector().template toValueType<ImpreciseType>();
276 SymbolicMinMaxLinearEquationSolver<DdType, ImpreciseType> impreciseSolver(
277 this->A.template toValueType<ImpreciseType>(), this->allRows, this->illegalMask, this->rowMetaVariables, this->columnMetaVariables,
278 this->choiceVariables, this->rowColumnMetaVariablePairs, std::make_unique<GeneralSymbolicLinearEquationSolverFactory<DdType, ImpreciseType>>());
280 rationalResult = solveEquationsRationalSearchHelper<ValueType, ImpreciseType>(env, dir, *
this, impreciseSolver, b, impreciseX, impreciseB);
281 }
catch (storm::exceptions::PrecisionExceededException
const& e) {
282 STORM_LOG_WARN(
"Precision of value type was exceeded, trying to recover by switching to rational arithmetic.");
285 rationalResult = solveEquationsRationalSearchHelper<ValueType, ValueType>(env, dir, *
this, *
this, b, impreciseX.template toValueType<ValueType>(), b);
287 return rationalResult.template toValueType<ValueType>();
290template<storm::dd::DdType DdType,
typename ValueType>
294 return solveEquationsRationalSearchHelper<double>(env, dir, x, b);
297template<storm::dd::DdType DdType,
typename ValueType>
304 if (this->hasUniqueSolution()) {
308 if (this->hasInitialScheduler()) {
310 std::unique_ptr<storm::Environment> environmentOfSolverStorage;
311 auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType());
313 bool changePrecision = precOfSolver.first && precOfSolver.first.get() > env.solver().minMax().getPrecision();
314 bool changeRelative = precOfSolver.second && !precOfSolver.second.get() && env.solver().minMax().getRelativeTerminationCriterion();
315 if (changePrecision || changeRelative) {
316 environmentOfSolverStorage = std::make_unique<storm::Environment>(env);
317 boost::optional<storm::RationalNumber> newPrecision;
318 boost::optional<bool> newRelative;
319 if (changePrecision) {
320 newPrecision = env.solver().minMax().getPrecision();
322 if (changeRelative) {
325 environmentOfSolverStorage->solver().setLinearEquationSolverPrecision(newPrecision, newRelative);
328 storm::Environment const& environmentOfSolver = environmentOfSolverStorage ? *environmentOfSolverStorage : env;
329 localX = solveEquationsWithScheduler(environmentOfSolver, this->getInitialScheduler(), x, b);
331 localX = this->getLowerBoundsVector();
335 ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().minMax().getPrecision());
336 ValueIterationResult viResult = performValueIteration(dir, localX, b, precision, env.solver().minMax().getRelativeTerminationCriterion(),
337 env.solver().minMax().getMaximalNumberOfIterations());
340 STORM_LOG_INFO(
"Iterative solver (value iteration) converged in " << viResult.iterations <<
" iterations.");
342 STORM_LOG_WARN(
"Iterative solver (value iteration) did not converge in " << viResult.iterations <<
" iterations.");
345 return viResult.values;
348template<storm::dd::DdType DdType,
typename ValueType>
352 std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> solver =
353 linearEquationSolverFactory->create(env, this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
354 this->forwardBounds(*solver);
357 (storm::utility::dd::getRowColumnDiagonal<DdType>(x.
getDdManager(), this->rowColumnMetaVariablePairs) && this->allRows).
template toAdd<ValueType>();
358 return solveEquationsWithScheduler(env, *solver, scheduler, x, b, diagonal);
361template<storm::dd::DdType DdType,
typename ValueType>
363 Environment
const& env, SymbolicLinearEquationSolver<DdType, ValueType>& solver,
storm::dd::Bdd<DdType> const& scheduler,
367 scheduler.
ite(this->A, scheduler.
getDdManager().template getAddZero<ValueType>()).sumAbstract(this->choiceVariables);
369 schedulerA = diagonal - schedulerA;
373 scheduler.
ite(b, scheduler.
getDdManager().template getAddZero<ValueType>()).sumAbstract(this->choiceVariables);
376 solver.setMatrix(schedulerA);
384template<storm::dd::DdType DdType,
typename ValueType>
391 (storm::utility::dd::getRowColumnDiagonal<DdType>(x.
getDdManager(), this->rowColumnMetaVariablePairs) && this->allRows).
template toAdd<ValueType>();
392 uint_fast64_t iterations = 0;
393 bool converged =
false;
397 this->hasInitialScheduler()
398 ? this->getInitialScheduler()
399 : (this->A.sumAbstract(this->columnMetaVariables).notZero() || b.notZero()).existsAbstractRepresentative(this->choiceVariables);
403 std::unique_ptr<storm::Environment> environmentOfSolverStorage;
404 auto precOfSolver = env.solver().getPrecisionOfLinearEquationSolver(env.solver().getLinearEquationSolverType());
406 bool changePrecision = precOfSolver.first && precOfSolver.first.get() > env.solver().minMax().getPrecision();
407 bool changeRelative = precOfSolver.second && !precOfSolver.second.get() && env.solver().minMax().getRelativeTerminationCriterion();
408 if (changePrecision || changeRelative) {
409 environmentOfSolverStorage = std::make_unique<storm::Environment>(env);
410 boost::optional<storm::RationalNumber> newPrecision;
411 boost::optional<bool> newRelative;
412 if (changePrecision) {
413 newPrecision = env.solver().minMax().getPrecision();
415 if (changeRelative) {
418 environmentOfSolverStorage->solver().setLinearEquationSolverPrecision(newPrecision, newRelative);
421 storm::Environment const& environmentOfSolver = environmentOfSolverStorage ? *environmentOfSolverStorage : env;
423 std::unique_ptr<SymbolicLinearEquationSolver<DdType, ValueType>> linearEquationSolver = linearEquationSolverFactory->create(
424 environmentOfSolver, this->allRows, this->rowMetaVariables, this->columnMetaVariables, this->rowColumnMetaVariablePairs);
425 this->forwardBounds(*linearEquationSolver);
428 uint64_t maxIter = env.solver().minMax().getMaximalNumberOfIterations();
429 while (!converged && iterations < maxIter) {
431 solveEquationsWithScheduler(environmentOfSolver, *linearEquationSolver, scheduler, currentSolution, b, diagonal);
438 if (dir == storm::solver::OptimizationDirection::Minimize) {
439 choiceValues += illegalMaskAdd;
453 converged = nextScheduler == scheduler;
457 scheduler = nextScheduler;
460 currentSolution = schedulerX;
465 STORM_LOG_INFO(
"Iterative solver (policy iteration) converged in " << iterations <<
" iterations.");
467 STORM_LOG_WARN(
"Iterative solver (policy iteration) did not converge in " << iterations <<
" iterations.");
470 return currentSolution;
473template<storm::dd::DdType DdType,
typename ValueType>
477 uint_fast64_t n)
const {
481 for (uint_fast64_t i = 0; i < n; ++i) {
482 xCopy = xCopy.
swapVariables(this->rowColumnMetaVariablePairs);
488 if (dir == storm::solver::OptimizationDirection::Minimize) {
491 xCopy += illegalMaskAdd;
501template<storm::dd::DdType DdType,
typename ValueType>
503 this->initialScheduler = scheduler;
506template<storm::dd::DdType DdType,
typename ValueType>
508 return initialScheduler.get();
511template<storm::dd::DdType DdType,
typename ValueType>
513 return static_cast<bool>(initialScheduler);
516template<storm::dd::DdType DdType,
typename ValueType>
518 Environment const& env, boost::optional<storm::solver::OptimizationDirection>
const& direction)
const {
521 auto method = getMethod(env, std::is_same<ValueType, storm::RationalNumber>::value);
522 if (method == MinMaxMethod::PolicyIteration) {
523 if (!this->hasUniqueSolution()) {
526 }
else if (method == MinMaxMethod::ValueIteration) {
527 if (!this->hasUniqueSolution()) {
528 if (!direction || direction.get() == storm::solver::OptimizationDirection::Maximize) {
531 if (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize) {
535 }
else if (method == MinMaxMethod::RationalSearch) {
537 if (!this->hasUniqueSolution() && (!direction || direction.get() == storm::solver::OptimizationDirection::Minimize)) {
541 STORM_LOG_THROW(
false, storm::exceptions::InvalidEnvironmentException,
"The selected min max technique is not supported by this solver.");
547template<storm::dd::DdType DdType,
typename ValueType>
549 this->uniqueSolution = value;
552template<storm::dd::DdType DdType,
typename ValueType>
554 return this->uniqueSolution;
557template<storm::dd::DdType DdType,
typename ValueType>
559 this->requirementsChecked = value;
562template<storm::dd::DdType DdType,
typename ValueType>
564 return this->requirementsChecked;
567template<storm::dd::DdType DdType,
typename ValueType>
569 if (this->hasLowerBound()) {
572 if (this->hasLowerBounds()) {
575 if (this->hasUpperBound()) {
578 if (this->hasUpperBounds()) {
583template<storm::dd::DdType DdType,
typename ValueType>
585 Environment const& env,
bool hasUniqueSolution, boost::optional<storm::solver::OptimizationDirection>
const& direction)
const {
586 std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>> solver = this->create();
587 solver->setHasUniqueSolution(hasUniqueSolution);
588 return solver->getRequirements(env, direction);
591template<storm::dd::DdType DdType,
typename ValueType>
592std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>>
595 std::set<storm::expressions::Variable>
const& rowMetaVariables, std::set<storm::expressions::Variable>
const& columnMetaVariables,
596 std::set<storm::expressions::Variable>
const& choiceVariables,
597 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>>
const& rowColumnMetaVariablePairs)
const {
598 return std::make_unique<SymbolicMinMaxLinearEquationSolver<DdType, ValueType>>(
599 A, allRows, illegalMask, rowMetaVariables, columnMetaVariables, choiceVariables, rowColumnMetaVariablePairs,
600 std::make_unique<GeneralSymbolicLinearEquationSolverFactory<DdType, ValueType>>());
603template<storm::dd::DdType DdType,
typename ValueType>
604std::unique_ptr<storm::solver::SymbolicMinMaxLinearEquationSolver<DdType, ValueType>>
606 return std::make_unique<SymbolicMinMaxLinearEquationSolver<DdType, ValueType>>();
609template class SymbolicMinMaxLinearEquationSolver<storm::dd::DdType::CUDD, double>;
610template class SymbolicMinMaxLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
611template class SymbolicMinMaxLinearEquationSolver<storm::dd::DdType::Sylvan, storm::RationalNumber>;
613template class GeneralSymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
614template class GeneralSymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
615template class GeneralSymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalNumber>;
SolverEnvironment & solver()
bool const & isMethodSetFromDefault() const
storm::solver::MinMaxMethod const & getMethod() const
MinMaxSolverEnvironment & minMax()
Add< LibraryType, ValueType > swapVariables(std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &metaVariablePairs) const
Swaps the given pairs of meta variables in the ADD.
Add< LibraryType, storm::RationalNumber > sharpenKwekMehlhorn(uint64_t precision) const
Retrieves the function that sharpens all values in the current ADD with the Kwek-Mehlhorn algorithm.
Bdd< LibraryType > greater(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one whose function value in the first ADD are gre...
Add< LibraryType, ValueType > maxAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Max-abstracts from the given meta variables.
Bdd< LibraryType > minAbstractRepresentative(std::set< storm::expressions::Variable > const &metaVariables) const
Similar to minAbstract, but does not abstract from the variables but rather picks a valuation of each...
Add< LibraryType, ValueType > minAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Min-abstracts from the given meta variables.
Add< LibraryType, ValueType > multiplyMatrix(Add< LibraryType, ValueType > const &otherMatrix, std::set< storm::expressions::Variable > const &summationMetaVariables) const
Multiplies the current ADD (representing a matrix) with the given matrix by summing over the given me...
bool equalModuloPrecision(Add< LibraryType, ValueType > const &other, ValueType const &precision, bool relative=true) const
Checks whether the current and the given ADD represent the same function modulo some given precision.
Bdd< LibraryType > maxAbstractRepresentative(std::set< storm::expressions::Variable > const &metaVariables) const
Similar to maxAbstract, but does not abstract from the variables but rather picks a valuation of each...
Bdd< LibraryType > less(Add< LibraryType, ValueType > const &other) const
Retrieves the function that maps all evaluations to one whose function value in the first ADD are les...
Bdd< LibraryType > ite(Bdd< LibraryType > const &thenBdd, Bdd< LibraryType > const &elseBdd) const
Performs an if-then-else with the given operands, i.e.
DdManager< LibraryType > & getDdManager() const
Retrieves the manager that is responsible for this DD.
MinMaxLinearEquationSolverRequirements & requireUniqueSolution(bool critical=true)
MinMaxLinearEquationSolverRequirements & requireLowerBounds(bool critical=true)
MinMaxLinearEquationSolverRequirements & requireValidInitialScheduler(bool critical=true)
virtual void setUpperBound(ValueType const &lowerBound)
virtual void setLowerBounds(storm::dd::Add< DdType, ValueType > const &lowerBounds)
virtual void setUpperBounds(storm::dd::Add< DdType, ValueType > const &upperBounds)
virtual void setLowerBound(ValueType const &lowerBound)
An interface that represents an abstract symbolic linear equation solver.
MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, bool hasUniqueSolution=false, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none) const
Retrieves the requirements of the solver that would be created when calling create() right now.
An interface that represents an abstract symbolic linear equation solver.
bool hasUniqueSolution() const
Retrieves whether the solution to the min max equation system is assumed to be unique.
friend class SymbolicMinMaxLinearEquationSolver
bool hasInitialScheduler() const
Retrieves whether an initial scheduler was set.
void setHasUniqueSolution(bool value=true)
Sets whether the solution to the min max equation system is known to be unique.
virtual storm::dd::Add< DdType, ValueType > multiply(storm::solver::OptimizationDirection const &dir, storm::dd::Add< DdType, ValueType > const &x, storm::dd::Add< DdType, ValueType > const *b=nullptr, uint_fast64_t n=1) const
Performs repeated matrix-vector multiplication, using x[0] = x and x[i + 1] = A*x[i] + b.
virtual storm::dd::Add< DdType, ValueType > solveEquations(Environment const &env, storm::solver::OptimizationDirection const &dir, storm::dd::Add< DdType, ValueType > const &x, storm::dd::Add< DdType, ValueType > const &b) const
Solves the equation system A*x = b.
bool isSolution(OptimizationDirection dir, storm::dd::Add< DdType, ValueType > const &x, storm::dd::Add< DdType, ValueType > const &b) const
Determines whether the given vector x satisfies x = min/max Ax + b.
void setInitialScheduler(storm::dd::Bdd< DdType > const &scheduler)
Sets an initial scheduler that is required by some solvers (see requirements).
bool isRequirementsCheckedSet() const
Retrieves whether the solver is aware that the requirements were checked.
storm::dd::Bdd< DdType > const & getInitialScheduler() const
Retrieves the initial scheduler (if there is any).
void setRequirementsChecked(bool value=true)
Notifies the solver that the requirements for solving equations have been checked.
virtual MinMaxLinearEquationSolverRequirements getRequirements(Environment const &env, boost::optional< storm::solver::OptimizationDirection > const &direction=boost::none) const
Retrieves the requirements of the solver.
#define STORM_LOG_INFO(message)
#define STORM_LOG_WARN(message)
#define STORM_LOG_TRACE(message)
#define STORM_LOG_THROW(cond, exception, message)
#define STORM_LOG_WARN_COND_DEBUG(cond, message)
SFTBDDChecker::ValueType ValueType
@ MaximalIterationsExceeded
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
ValueType ceil(ValueType const &number)