|
Storm 1.11.1.1
A Modern Probabilistic Model Checker
|
#include <AbstractEquationSolver.h>

Public Types | |
| enum class | BoundType { Global , Local , Any } |
Public Member Functions | |
| AbstractEquationSolver () | |
| void | setTerminationCondition (std::unique_ptr< TerminationCondition< ValueType > > terminationCondition) |
| Sets a custom termination condition that is used together with the regular termination condition of the solver. | |
| void | resetTerminationCondition () |
| Removes a previously set custom termination condition. | |
| bool | hasCustomTerminationCondition () const |
| Retrieves whether a custom termination condition has been set. | |
| bool | terminateNow (std::vector< ValueType > const &values, SolverGuarantee const &guarantee) const |
| Checks whether the solver can terminate wrt. | |
| bool | hasRelevantValues () const |
| Retrieves whether this solver has particularly relevant values. | |
| storm::storage::BitVector const & | getRelevantValues () const |
| Retrieves the relevant values (if there are any). | |
| boost::optional< storm::storage::BitVector > const & | getOptionalRelevantValues () const |
| void | setRelevantValues (storm::storage::BitVector &&valuesOfInterest) |
| Sets the relevant values. | |
| void | setRelevantValues (storm::storage::BitVector const &valuesOfInterest) |
| Sets the relevant values. | |
| void | clearRelevantValues () |
| Removes the values of interest (if there were any). | |
| bool | hasLowerBound (BoundType const &type=BoundType::Any) const |
| Retrieves whether this solver has a lower bound. | |
| bool | hasUpperBound (BoundType const &type=BoundType::Any) const |
| Retrieves whether this solver has an upper bound. | |
| void | setLowerBound (ValueType const &value) |
| Sets a lower bound for the solution that can potentially be used by the solver. | |
| void | setUpperBound (ValueType const &value) |
| Sets an upper bound for the solution that can potentially be used by the solver. | |
| void | setBounds (ValueType const &lower, ValueType const &upper) |
| Sets bounds for the solution that can potentially be used by the solver. | |
| ValueType const & | getLowerBound () const |
| Retrieves the lower bound (if there is any). | |
| ValueType const & | getLowerBound (uint64_t const &index) const |
| Retrieves the lower bound for the variable with the given index (if there is any lower bound). | |
| ValueType | getLowerBound (bool convertLocalBounds) const |
| Retrieves the lower bound (if there is any). | |
| ValueType const & | getUpperBound () const |
| Retrieves the upper bound (if there is any). | |
| ValueType const & | getUpperBound (uint64_t const &index) const |
| Retrieves the upper bound for the variable with the given index (if there is any upper bound). | |
| ValueType | getUpperBound (bool convertLocalBounds) const |
| Retrieves the upper bound (if there is any). | |
| std::vector< ValueType > const & | getLowerBounds () const |
| Retrieves a vector containing the lower bounds (if there are any). | |
| std::vector< ValueType > const & | getUpperBounds () const |
| Retrieves a vector containing the upper bounds (if there are any). | |
| void | setLowerBounds (std::vector< ValueType > const &values) |
| Sets lower bounds for the solution that can potentially be used by the solver. | |
| void | setLowerBounds (std::vector< ValueType > &&values) |
| Sets lower bounds for the solution that can potentially be used by the solver. | |
| void | setUpperBounds (std::vector< ValueType > const &values) |
| Sets upper bounds for the solution that can potentially be used by the solver. | |
| void | setUpperBounds (std::vector< ValueType > &&values) |
| Sets upper bounds for the solution that can potentially be used by the solver. | |
| void | setBounds (std::vector< ValueType > const &lower, std::vector< ValueType > const &upper) |
| Sets bounds for the solution that can potentially be used by the solver. | |
| void | setBoundsFromOtherSolver (AbstractEquationSolver< ValueType > const &other) |
| void | clearBounds () |
| Removes all specified solution bounds. | |
| bool | isShowProgressSet () const |
| Retrieves whether progress is to be shown. | |
| uint64_t | getShowProgressDelay () const |
| Retrieves the delay between progress emissions. | |
| void | startMeasureProgress (uint64_t startingIteration=0) const |
| Starts to measure progress. | |
| void | showProgressIterative (uint64_t iterations, boost::optional< uint64_t > const &bound=boost::none) const |
| Shows progress if this solver is asked to do so. | |
Protected Member Functions | |
| TerminationCondition< ValueType > const & | getTerminationCondition () const |
| Retrieves the custom termination condition (if any was set). | |
| std::unique_ptr< TerminationCondition< ValueType > > const & | getTerminationConditionPointer () const |
| void | createUpperBoundsVector (std::vector< ValueType > &upperBoundsVector) const |
| void | createUpperBoundsVector (std::unique_ptr< std::vector< ValueType > > &upperBoundsVector, uint64_t length) const |
| void | createLowerBoundsVector (std::vector< ValueType > &lowerBoundsVector) const |
| void | reportStatus (SolverStatus status, boost::optional< uint64_t > const &iterations=boost::none) const |
| Report the current status of the solver. | |
| SolverStatus | updateStatus (SolverStatus status, std::vector< ValueType > const &x, SolverGuarantee const &guarantee, uint64_t iterations, uint64_t maximalNumberOfIterations) const |
| Update the status of the solver with respect to convergence, early termination, abortion, etc. | |
| SolverStatus | updateStatus (SolverStatus status, bool earlyTermination, uint64_t iterations, uint64_t maximalNumberOfIterations) const |
| Update the status of the solver with respect to convergence, early termination, abortion, etc. | |
Protected Attributes | |
| std::unique_ptr< TerminationCondition< ValueType > > | terminationCondition |
| boost::optional< storm::storage::BitVector > | relevantValues |
| boost::optional< ValueType > | lowerBound |
| boost::optional< ValueType > | upperBound |
| boost::optional< std::vector< ValueType > > | lowerBounds |
| boost::optional< std::vector< ValueType > > | upperBounds |
Definition at line 17 of file AbstractEquationSolver.h.
|
strong |
| Enumerator | |
|---|---|
| Global | |
| Local | |
| Any | |
Definition at line 71 of file AbstractEquationSolver.h.
| storm::solver::AbstractEquationSolver< ValueType >::AbstractEquationSolver | ( | ) |
Definition at line 16 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::clearBounds | ( | ) |
Removes all specified solution bounds.
Definition at line 241 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::clearRelevantValues | ( | ) |
Removes the values of interest (if there were any).
Definition at line 82 of file AbstractEquationSolver.cpp.
|
protected |
Definition at line 249 of file AbstractEquationSolver.cpp.
|
protected |
Definition at line 271 of file AbstractEquationSolver.cpp.
|
protected |
Definition at line 261 of file AbstractEquationSolver.cpp.
| ValueType const & storm::solver::AbstractEquationSolver< ValueType >::getLowerBound | ( | ) | const |
Retrieves the lower bound (if there is any).
Definition at line 127 of file AbstractEquationSolver.cpp.
| ValueType storm::solver::AbstractEquationSolver< ValueType >::getLowerBound | ( | bool | convertLocalBounds | ) | const |
Retrieves the lower bound (if there is any).
If the given flag is true and if there are only local bounds, the minimum of the local bounds is returned.
Definition at line 147 of file AbstractEquationSolver.cpp.
| ValueType const & storm::solver::AbstractEquationSolver< ValueType >::getLowerBound | ( | uint64_t const & | index | ) | const |
Retrieves the lower bound for the variable with the given index (if there is any lower bound).
Definition at line 132 of file AbstractEquationSolver.cpp.
| std::vector< ValueType > const & storm::solver::AbstractEquationSolver< ValueType >::getLowerBounds | ( | ) | const |
Retrieves a vector containing the lower bounds (if there are any).
Definition at line 189 of file AbstractEquationSolver.cpp.
| boost::optional< storm::storage::BitVector > const & storm::solver::AbstractEquationSolver< ValueType >::getOptionalRelevantValues | ( | ) | const |
Definition at line 67 of file AbstractEquationSolver.cpp.
| storm::storage::BitVector const & storm::solver::AbstractEquationSolver< ValueType >::getRelevantValues | ( | ) | const |
Retrieves the relevant values (if there are any).
Definition at line 62 of file AbstractEquationSolver.cpp.
| uint64_t storm::solver::AbstractEquationSolver< ValueType >::getShowProgressDelay | ( | ) | const |
Retrieves the delay between progress emissions.
Definition at line 291 of file AbstractEquationSolver.cpp.
|
protected |
Retrieves the custom termination condition (if any was set).
Definition at line 38 of file AbstractEquationSolver.cpp.
|
protected |
Definition at line 43 of file AbstractEquationSolver.cpp.
| ValueType const & storm::solver::AbstractEquationSolver< ValueType >::getUpperBound | ( | ) | const |
Retrieves the upper bound (if there is any).
Definition at line 158 of file AbstractEquationSolver.cpp.
| ValueType storm::solver::AbstractEquationSolver< ValueType >::getUpperBound | ( | bool | convertLocalBounds | ) | const |
Retrieves the upper bound (if there is any).
If the given flag is true and if there are only local bounds, the maximum of the local bounds is returned.
Definition at line 178 of file AbstractEquationSolver.cpp.
| ValueType const & storm::solver::AbstractEquationSolver< ValueType >::getUpperBound | ( | uint64_t const & | index | ) | const |
Retrieves the upper bound for the variable with the given index (if there is any upper bound).
Definition at line 163 of file AbstractEquationSolver.cpp.
| std::vector< ValueType > const & storm::solver::AbstractEquationSolver< ValueType >::getUpperBounds | ( | ) | const |
Retrieves a vector containing the upper bounds (if there are any).
Definition at line 194 of file AbstractEquationSolver.cpp.
| bool storm::solver::AbstractEquationSolver< ValueType >::hasCustomTerminationCondition | ( | ) | const |
Retrieves whether a custom termination condition has been set.
Definition at line 33 of file AbstractEquationSolver.cpp.
| bool storm::solver::AbstractEquationSolver< ValueType >::hasLowerBound | ( | BoundType const & | type = BoundType::Any | ) | const |
Retrieves whether this solver has a lower bound.
Definition at line 87 of file AbstractEquationSolver.cpp.
| bool storm::solver::AbstractEquationSolver< ValueType >::hasRelevantValues | ( | ) | const |
Retrieves whether this solver has particularly relevant values.
Definition at line 57 of file AbstractEquationSolver.cpp.
| bool storm::solver::AbstractEquationSolver< ValueType >::hasUpperBound | ( | BoundType const & | type = BoundType::Any | ) | const |
Retrieves whether this solver has an upper bound.
Definition at line 99 of file AbstractEquationSolver.cpp.
| bool storm::solver::AbstractEquationSolver< ValueType >::isShowProgressSet | ( | ) | const |
Retrieves whether progress is to be shown.
Definition at line 286 of file AbstractEquationSolver.cpp.
|
protected |
Report the current status of the solver.
| status | Solver status. |
| iterations | Number of iterations (if solver is iterative). |
Definition at line 314 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::resetTerminationCondition | ( | ) |
Removes a previously set custom termination condition.
Definition at line 28 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setBounds | ( | std::vector< ValueType > const & | lower, |
| std::vector< ValueType > const & | upper | ||
| ) |
Sets bounds for the solution that can potentially be used by the solver.
Definition at line 219 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setBounds | ( | ValueType const & | lower, |
| ValueType const & | upper | ||
| ) |
Sets bounds for the solution that can potentially be used by the solver.
Definition at line 121 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setBoundsFromOtherSolver | ( | AbstractEquationSolver< ValueType > const & | other | ) |
Definition at line 225 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setLowerBound | ( | ValueType const & | value | ) |
Sets a lower bound for the solution that can potentially be used by the solver.
Definition at line 111 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setLowerBounds | ( | std::vector< ValueType > && | values | ) |
Sets lower bounds for the solution that can potentially be used by the solver.
Definition at line 204 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setLowerBounds | ( | std::vector< ValueType > const & | values | ) |
Sets lower bounds for the solution that can potentially be used by the solver.
Definition at line 199 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setRelevantValues | ( | storm::storage::BitVector && | valuesOfInterest | ) |
Sets the relevant values.
Definition at line 72 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setRelevantValues | ( | storm::storage::BitVector const & | valuesOfInterest | ) |
Sets the relevant values.
Definition at line 77 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setTerminationCondition | ( | std::unique_ptr< TerminationCondition< ValueType > > | terminationCondition | ) |
Sets a custom termination condition that is used together with the regular termination condition of the solver.
| terminationCondition | An object that can be queried whether to terminate early or not. |
Definition at line 23 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setUpperBound | ( | ValueType const & | value | ) |
Sets an upper bound for the solution that can potentially be used by the solver.
Definition at line 116 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setUpperBounds | ( | std::vector< ValueType > && | values | ) |
Sets upper bounds for the solution that can potentially be used by the solver.
Definition at line 214 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::setUpperBounds | ( | std::vector< ValueType > const & | values | ) |
Sets upper bounds for the solution that can potentially be used by the solver.
Definition at line 209 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::showProgressIterative | ( | uint64_t | iterations, |
| boost::optional< uint64_t > const & | bound = boost::none |
||
| ) | const |
Shows progress if this solver is asked to do so.
Definition at line 304 of file AbstractEquationSolver.cpp.
| void storm::solver::AbstractEquationSolver< ValueType >::startMeasureProgress | ( | uint64_t | startingIteration = 0 | ) | const |
Starts to measure progress.
Definition at line 297 of file AbstractEquationSolver.cpp.
| bool storm::solver::AbstractEquationSolver< ValueType >::terminateNow | ( | std::vector< ValueType > const & | values, |
| SolverGuarantee const & | guarantee | ||
| ) | const |
Checks whether the solver can terminate wrt.
to its termination condition. If no termination condition, this will yield false.
Definition at line 48 of file AbstractEquationSolver.cpp.
|
protected |
Update the status of the solver with respect to convergence, early termination, abortion, etc.
| status | Current status. |
| earlyTermination | Flag indicating if the solver can be terminated early. |
| iterations | Current number of iterations. |
| maximalNumberOfIterations | Maximal number of iterations. |
Definition at line 354 of file AbstractEquationSolver.cpp.
|
protected |
Update the status of the solver with respect to convergence, early termination, abortion, etc.
| status | Current status. |
| x | Vector for terminatation condition. |
| guarantee | Guarentee for termination condition. |
| iterations | Current number of iterations. |
| maximalNumberOfIterations | Maximal number of iterations. |
Definition at line 369 of file AbstractEquationSolver.cpp.
|
protected |
Definition at line 247 of file AbstractEquationSolver.h.
|
protected |
Definition at line 253 of file AbstractEquationSolver.h.
|
protected |
Definition at line 244 of file AbstractEquationSolver.h.
|
protected |
Definition at line 241 of file AbstractEquationSolver.h.
|
protected |
Definition at line 250 of file AbstractEquationSolver.h.
|
protected |
Definition at line 256 of file AbstractEquationSolver.h.