Storm
A Modern Probabilistic Model Checker
|
#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 ®ion) |
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 ®) |
Checks if a derivative >=0 or/and <=0. | |
Definition at line 23 of file MonotonicityChecker.h.
typedef utility::parametric::CoefficientType<ValueType>::type storm::analysis::MonotonicityChecker< ValueType >::CoefficientType |
Definition at line 26 of file MonotonicityChecker.h.
typedef MonotonicityResult<VariableType>::Monotonicity storm::analysis::MonotonicityChecker< ValueType >::Monotonicity |
Definition at line 27 of file MonotonicityChecker.h.
typedef storage::ParameterRegion<ValueType> storm::analysis::MonotonicityChecker< ValueType >::Region |
Definition at line 28 of file MonotonicityChecker.h.
typedef utility::parametric::VariableType<ValueType>::type storm::analysis::MonotonicityChecker< ValueType >::VariableType |
Definition at line 25 of file MonotonicityChecker.h.
storm::analysis::MonotonicityChecker< ValueType >::MonotonicityChecker | ( | storage::SparseMatrix< ValueType > const & | matrix | ) |
Constructs a new MonotonicityChecker object.
matrix | The Matrix of the model. |
Definition at line 8 of file MonotonicityChecker.cpp.
|
static |
Checks if a derivative >=0 or/and <=0.
derivative | The derivative you want to check. |
reg | The region of the parameters. |
Definition at line 119 of file MonotonicityChecker.cpp.
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.
order | The order on which the monotonicity should be checked. |
state | The considerd state. |
var | The variable in which we check for monotonicity. |
region | The region on which we check the monotonicity. |
Definition at line 13 of file MonotonicityChecker.cpp.