Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::analysis::MonotonicityChecker< ValueType > Class Template Reference

#include <MonotonicityChecker.h>

Public Types

typedef utility::parametric::VariableType< ValueType >::type VariableType
 
typedef utility::parametric::CoefficientType< ValueType >::type CoefficientType
 
typedef MonotonicityResult< VariableType >::Monotonicity Monotonicity
 
typedef storage::ParameterRegion< ValueType > Region
 

Public Member Functions

 MonotonicityChecker (storage::SparseMatrix< ValueType > const &matrix)
 Constructs a new MonotonicityChecker object.
 
Monotonicity checkLocalMonotonicity (std::shared_ptr< Order > const &order, uint_fast64_t state, VariableType const &var, storage::ParameterRegion< ValueType > const &region)
 Checks for local monotonicity at the given state.
 

Static Public Member Functions

static std::pair< bool, bool > checkDerivative (ValueType const &derivative, storage::ParameterRegion< ValueType > const &reg)
 Checks if a derivative >=0 or/and <=0.
 

Detailed Description

template<typename ValueType>
class storm::analysis::MonotonicityChecker< ValueType >

Definition at line 23 of file MonotonicityChecker.h.

Member Typedef Documentation

◆ CoefficientType

template<typename ValueType >
typedef utility::parametric::CoefficientType<ValueType>::type storm::analysis::MonotonicityChecker< ValueType >::CoefficientType

Definition at line 26 of file MonotonicityChecker.h.

◆ Monotonicity

template<typename ValueType >
typedef MonotonicityResult<VariableType>::Monotonicity storm::analysis::MonotonicityChecker< ValueType >::Monotonicity

Definition at line 27 of file MonotonicityChecker.h.

◆ Region

template<typename ValueType >
typedef storage::ParameterRegion<ValueType> storm::analysis::MonotonicityChecker< ValueType >::Region

Definition at line 28 of file MonotonicityChecker.h.

◆ VariableType

template<typename ValueType >
typedef utility::parametric::VariableType<ValueType>::type storm::analysis::MonotonicityChecker< ValueType >::VariableType

Definition at line 25 of file MonotonicityChecker.h.

Constructor & Destructor Documentation

◆ MonotonicityChecker()

template<typename ValueType >
storm::analysis::MonotonicityChecker< ValueType >::MonotonicityChecker ( storage::SparseMatrix< ValueType > const &  matrix)

Constructs a new MonotonicityChecker object.

Parameters
matrixThe Matrix of the model.

Definition at line 8 of file MonotonicityChecker.cpp.

Member Function Documentation

◆ checkDerivative()

template<typename ValueType >
std::pair< bool, bool > storm::analysis::MonotonicityChecker< ValueType >::checkDerivative ( ValueType const &  derivative,
storage::ParameterRegion< ValueType > const &  reg 
)
static

Checks if a derivative >=0 or/and <=0.

Parameters
derivativeThe derivative you want to check.
regThe region of the parameters.
Returns
Pair of bools, >= 0 and <= 0.

Definition at line 119 of file MonotonicityChecker.cpp.

◆ checkLocalMonotonicity()

template<typename ValueType >
MonotonicityChecker< ValueType >::Monotonicity storm::analysis::MonotonicityChecker< ValueType >::checkLocalMonotonicity ( std::shared_ptr< Order > const &  order,
uint_fast64_t  state,
VariableType const &  var,
storage::ParameterRegion< ValueType > const &  region 
)

Checks for local monotonicity at the given state.

Parameters
orderThe order on which the monotonicity should be checked.
stateThe considerd state.
varThe variable in which we check for monotonicity.
regionThe region on which we check the monotonicity.
Returns
Incr, Decr, Constant, Unknown or Not

Definition at line 13 of file MonotonicityChecker.cpp.


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