Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::solver::AbstractEquationSolver< ValueType > Class Template Reference

#include <AbstractEquationSolver.h>

Inheritance diagram for storm::solver::AbstractEquationSolver< ValueType >:

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::BitVectorrelevantValues
 
boost::optional< ValueType > lowerBound
 
boost::optional< ValueType > upperBound
 
boost::optional< std::vector< ValueType > > lowerBounds
 
boost::optional< std::vector< ValueType > > upperBounds
 

Detailed Description

template<typename ValueType>
class storm::solver::AbstractEquationSolver< ValueType >

Definition at line 17 of file AbstractEquationSolver.h.

Member Enumeration Documentation

◆ BoundType

template<typename ValueType >
enum class storm::solver::AbstractEquationSolver::BoundType
strong
Enumerator
Global 
Local 
Any 

Definition at line 71 of file AbstractEquationSolver.h.

Constructor & Destructor Documentation

◆ AbstractEquationSolver()

template<typename ValueType >
storm::solver::AbstractEquationSolver< ValueType >::AbstractEquationSolver ( )

Definition at line 16 of file AbstractEquationSolver.cpp.

Member Function Documentation

◆ clearBounds()

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::clearBounds ( )

Removes all specified solution bounds.

Definition at line 241 of file AbstractEquationSolver.cpp.

◆ clearRelevantValues()

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::clearRelevantValues ( )

Removes the values of interest (if there were any).

Definition at line 82 of file AbstractEquationSolver.cpp.

◆ createLowerBoundsVector()

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::createLowerBoundsVector ( std::vector< ValueType > &  lowerBoundsVector) const
protected

Definition at line 249 of file AbstractEquationSolver.cpp.

◆ createUpperBoundsVector() [1/2]

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::createUpperBoundsVector ( std::unique_ptr< std::vector< ValueType > > &  upperBoundsVector,
uint64_t  length 
) const
protected

Definition at line 271 of file AbstractEquationSolver.cpp.

◆ createUpperBoundsVector() [2/2]

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::createUpperBoundsVector ( std::vector< ValueType > &  upperBoundsVector) const
protected

Definition at line 261 of file AbstractEquationSolver.cpp.

◆ getLowerBound() [1/3]

template<typename ValueType >
ValueType const & storm::solver::AbstractEquationSolver< ValueType >::getLowerBound ( ) const

Retrieves the lower bound (if there is any).

Definition at line 127 of file AbstractEquationSolver.cpp.

◆ getLowerBound() [2/3]

template<typename ValueType >
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.

◆ getLowerBound() [3/3]

template<typename ValueType >
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).

Precondition
some lower bound (local or global) has been specified
Returns
the largest lower bound known for the given row

Definition at line 132 of file AbstractEquationSolver.cpp.

◆ getLowerBounds()

template<typename ValueType >
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.

◆ getOptionalRelevantValues()

template<typename ValueType >
boost::optional< storm::storage::BitVector > const & storm::solver::AbstractEquationSolver< ValueType >::getOptionalRelevantValues ( ) const

Definition at line 67 of file AbstractEquationSolver.cpp.

◆ getRelevantValues()

template<typename ValueType >
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.

◆ getShowProgressDelay()

template<typename ValueType >
uint64_t storm::solver::AbstractEquationSolver< ValueType >::getShowProgressDelay ( ) const

Retrieves the delay between progress emissions.

Definition at line 291 of file AbstractEquationSolver.cpp.

◆ getTerminationCondition()

template<typename ValueType >
TerminationCondition< ValueType > const & storm::solver::AbstractEquationSolver< ValueType >::getTerminationCondition ( ) const
protected

Retrieves the custom termination condition (if any was set).

Returns
The custom termination condition.

Definition at line 38 of file AbstractEquationSolver.cpp.

◆ getTerminationConditionPointer()

template<typename ValueType >
std::unique_ptr< TerminationCondition< ValueType > > const & storm::solver::AbstractEquationSolver< ValueType >::getTerminationConditionPointer ( ) const
protected

Definition at line 43 of file AbstractEquationSolver.cpp.

◆ getUpperBound() [1/3]

template<typename ValueType >
ValueType const & storm::solver::AbstractEquationSolver< ValueType >::getUpperBound ( ) const

Retrieves the upper bound (if there is any).

Definition at line 158 of file AbstractEquationSolver.cpp.

◆ getUpperBound() [2/3]

template<typename ValueType >
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.

◆ getUpperBound() [3/3]

template<typename ValueType >
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).

Precondition
some upper bound (local or global) has been specified
Returns
the smallest upper bound known for the given row

Definition at line 163 of file AbstractEquationSolver.cpp.

◆ getUpperBounds()

template<typename ValueType >
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.

◆ hasCustomTerminationCondition()

template<typename ValueType >
bool storm::solver::AbstractEquationSolver< ValueType >::hasCustomTerminationCondition ( ) const

Retrieves whether a custom termination condition has been set.

Definition at line 33 of file AbstractEquationSolver.cpp.

◆ hasLowerBound()

template<typename ValueType >
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.

◆ hasRelevantValues()

template<typename ValueType >
bool storm::solver::AbstractEquationSolver< ValueType >::hasRelevantValues ( ) const

Retrieves whether this solver has particularly relevant values.

Definition at line 57 of file AbstractEquationSolver.cpp.

◆ hasUpperBound()

template<typename ValueType >
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.

◆ isShowProgressSet()

template<typename ValueType >
bool storm::solver::AbstractEquationSolver< ValueType >::isShowProgressSet ( ) const

Retrieves whether progress is to be shown.

Definition at line 286 of file AbstractEquationSolver.cpp.

◆ reportStatus()

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::reportStatus ( SolverStatus  status,
boost::optional< uint64_t > const &  iterations = boost::none 
) const
protected

Report the current status of the solver.

Parameters
statusSolver status.
iterationsNumber of iterations (if solver is iterative).

Definition at line 314 of file AbstractEquationSolver.cpp.

◆ resetTerminationCondition()

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::resetTerminationCondition ( )

Removes a previously set custom termination condition.

Definition at line 28 of file AbstractEquationSolver.cpp.

◆ setBounds() [1/2]

template<typename ValueType >
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.

◆ setBounds() [2/2]

template<typename ValueType >
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.

◆ setBoundsFromOtherSolver()

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::setBoundsFromOtherSolver ( AbstractEquationSolver< ValueType > const &  other)

Definition at line 225 of file AbstractEquationSolver.cpp.

◆ setLowerBound()

template<typename ValueType >
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.

◆ setLowerBounds() [1/2]

template<typename ValueType >
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.

◆ setLowerBounds() [2/2]

template<typename ValueType >
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.

◆ setRelevantValues() [1/2]

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::setRelevantValues ( storm::storage::BitVector &&  valuesOfInterest)

Sets the relevant values.

Definition at line 72 of file AbstractEquationSolver.cpp.

◆ setRelevantValues() [2/2]

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::setRelevantValues ( storm::storage::BitVector const &  valuesOfInterest)

Sets the relevant values.

Definition at line 77 of file AbstractEquationSolver.cpp.

◆ setTerminationCondition()

template<typename ValueType >
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.

Parameters
terminationConditionAn object that can be queried whether to terminate early or not.

Definition at line 23 of file AbstractEquationSolver.cpp.

◆ setUpperBound()

template<typename ValueType >
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.

◆ setUpperBounds() [1/2]

template<typename ValueType >
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.

◆ setUpperBounds() [2/2]

template<typename ValueType >
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.

◆ showProgressIterative()

template<typename ValueType >
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.

◆ startMeasureProgress()

template<typename ValueType >
void storm::solver::AbstractEquationSolver< ValueType >::startMeasureProgress ( uint64_t  startingIteration = 0) const

Starts to measure progress.

Definition at line 297 of file AbstractEquationSolver.cpp.

◆ terminateNow()

template<typename ValueType >
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.

◆ updateStatus() [1/2]

template<typename ValueType >
SolverStatus storm::solver::AbstractEquationSolver< ValueType >::updateStatus ( SolverStatus  status,
bool  earlyTermination,
uint64_t  iterations,
uint64_t  maximalNumberOfIterations 
) const
protected

Update the status of the solver with respect to convergence, early termination, abortion, etc.

Parameters
statusCurrent status.
earlyTerminationFlag indicating if the solver can be terminated early.
iterationsCurrent number of iterations.
maximalNumberOfIterationsMaximal number of iterations.
Returns
New status.

Definition at line 354 of file AbstractEquationSolver.cpp.

◆ updateStatus() [2/2]

template<typename ValueType >
SolverStatus storm::solver::AbstractEquationSolver< ValueType >::updateStatus ( SolverStatus  status,
std::vector< ValueType > const &  x,
SolverGuarantee const &  guarantee,
uint64_t  iterations,
uint64_t  maximalNumberOfIterations 
) const
protected

Update the status of the solver with respect to convergence, early termination, abortion, etc.

Parameters
statusCurrent status.
xVector for terminatation condition.
guaranteeGuarentee for termination condition.
iterationsCurrent number of iterations.
maximalNumberOfIterationsMaximal number of iterations.
Returns
New status.

Definition at line 369 of file AbstractEquationSolver.cpp.

Member Data Documentation

◆ lowerBound

template<typename ValueType >
boost::optional<ValueType> storm::solver::AbstractEquationSolver< ValueType >::lowerBound
protected

Definition at line 247 of file AbstractEquationSolver.h.

◆ lowerBounds

template<typename ValueType >
boost::optional<std::vector<ValueType> > storm::solver::AbstractEquationSolver< ValueType >::lowerBounds
protected

Definition at line 253 of file AbstractEquationSolver.h.

◆ relevantValues

template<typename ValueType >
boost::optional<storm::storage::BitVector> storm::solver::AbstractEquationSolver< ValueType >::relevantValues
protected

Definition at line 244 of file AbstractEquationSolver.h.

◆ terminationCondition

template<typename ValueType >
std::unique_ptr<TerminationCondition<ValueType> > storm::solver::AbstractEquationSolver< ValueType >::terminationCondition
protected

Definition at line 241 of file AbstractEquationSolver.h.

◆ upperBound

template<typename ValueType >
boost::optional<ValueType> storm::solver::AbstractEquationSolver< ValueType >::upperBound
protected

Definition at line 250 of file AbstractEquationSolver.h.

◆ upperBounds

template<typename ValueType >
boost::optional<std::vector<ValueType> > storm::solver::AbstractEquationSolver< ValueType >::upperBounds
protected

Definition at line 256 of file AbstractEquationSolver.h.


The documentation for this class was generated from the following files: