Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Attributes | List of all members
storm::modelchecker::MonotonicityBackend< ParametricType > Class Template Reference

#include <MonotonicityBackend.h>

Inheritance diagram for storm::modelchecker::MonotonicityBackend< ParametricType >:
Inheritance graph
[legend]

Public Types

using CoefficientType = storm::utility::parametric::CoefficientType_t< ParametricType >
 
using VariableType = storm::utility::parametric::VariableType_t< ParametricType >
 
using Valuation = storm::utility::parametric::Valuation< ParametricType >
 
using MonotonicityKind = storm::analysis::MonotonicityKind
 

Public Member Functions

 MonotonicityBackend ()=default
 
virtual ~MonotonicityBackend ()=default
 
void setMonotoneParameter (VariableType const &parameter, MonotonicityKind const &kind)
 Sets parameters that are assumed to be monotone throughout the analysis.
 
virtual bool requiresInteractionWithRegionModelChecker () const
 Returns true, if a region model checker needs to implement specific methods to properly use this backend.
 
virtual bool recommendModelSimplifications () const
 Returns whether additional model simplifications are recommended when using this backend.
 
virtual void initializeMonotonicity (storm::Environment const &env, AnnotatedRegion< ParametricType > &region)
 Initializes the monotonicity information for the given region.
 
virtual void updateMonotonicity (storm::Environment const &env, AnnotatedRegion< ParametricType > &region)
 Updates the monotonicity information for the given region.
 
virtual void updateMonotonicityBeforeSplitting (storm::Environment const &env, AnnotatedRegion< ParametricType > &region)
 Updates the monotonicity information for the given region right before splitting it.
 
virtual std::map< VariableType, MonotonicityKind > getOptimisticMonotonicityApproximation (AnnotatedRegion< ParametricType > const &region)
 Returns an optimistic approximation of the monotonicity of the parameters in this region.
 

Protected Attributes

std::map< VariableType, MonotonicityKind > globallyKnownMonotonicityInformation
 

Detailed Description

template<typename ParametricType>
class storm::modelchecker::MonotonicityBackend< ParametricType >

Definition at line 17 of file MonotonicityBackend.h.

Member Typedef Documentation

◆ CoefficientType

template<typename ParametricType >
using storm::modelchecker::MonotonicityBackend< ParametricType >::CoefficientType = storm::utility::parametric::CoefficientType_t<ParametricType>

Definition at line 19 of file MonotonicityBackend.h.

◆ MonotonicityKind

template<typename ParametricType >
using storm::modelchecker::MonotonicityBackend< ParametricType >::MonotonicityKind = storm::analysis::MonotonicityKind

Definition at line 22 of file MonotonicityBackend.h.

◆ Valuation

template<typename ParametricType >
using storm::modelchecker::MonotonicityBackend< ParametricType >::Valuation = storm::utility::parametric::Valuation<ParametricType>

Definition at line 21 of file MonotonicityBackend.h.

◆ VariableType

template<typename ParametricType >
using storm::modelchecker::MonotonicityBackend< ParametricType >::VariableType = storm::utility::parametric::VariableType_t<ParametricType>

Definition at line 20 of file MonotonicityBackend.h.

Constructor & Destructor Documentation

◆ MonotonicityBackend()

template<typename ParametricType >
storm::modelchecker::MonotonicityBackend< ParametricType >::MonotonicityBackend ( )
default

◆ ~MonotonicityBackend()

template<typename ParametricType >
virtual storm::modelchecker::MonotonicityBackend< ParametricType >::~MonotonicityBackend ( )
virtualdefault

Member Function Documentation

◆ getOptimisticMonotonicityApproximation()

template<typename ParametricType >
std::map< typename MonotonicityBackend< ParametricType >::VariableType, typename MonotonicityBackend< ParametricType >::MonotonicityKind > storm::modelchecker::MonotonicityBackend< ParametricType >::getOptimisticMonotonicityApproximation ( AnnotatedRegion< ParametricType > const &  region)
virtual

Returns an optimistic approximation of the monotonicity of the parameters in this region.

This means that the returned monotonicity does not necessarily hold, but there is "sufficient hope" that it does.

Reimplemented in storm::modelchecker::OrderBasedMonotonicityBackend< ParametricType, ConstantType >.

Definition at line 55 of file MonotonicityBackend.cpp.

◆ initializeMonotonicity()

template<typename ParametricType >
void storm::modelchecker::MonotonicityBackend< ParametricType >::initializeMonotonicity ( storm::Environment const &  env,
AnnotatedRegion< ParametricType > &  region 
)
virtual

Initializes the monotonicity information for the given region.

Overwrites all present monotonicity annotations in the given region.

Reimplemented in storm::modelchecker::OrderBasedMonotonicityBackend< ParametricType, ConstantType >.

Definition at line 15 of file MonotonicityBackend.cpp.

◆ recommendModelSimplifications()

template<typename ParametricType >
bool storm::modelchecker::MonotonicityBackend< ParametricType >::recommendModelSimplifications ( ) const
virtual

Returns whether additional model simplifications are recommended when using this backend.

Note
this returns true in the base class, but might return false in derived classes.

Reimplemented in storm::modelchecker::OrderBasedMonotonicityBackend< ParametricType, ConstantType >.

Definition at line 49 of file MonotonicityBackend.cpp.

◆ requiresInteractionWithRegionModelChecker()

template<typename ParametricType >
bool storm::modelchecker::MonotonicityBackend< ParametricType >::requiresInteractionWithRegionModelChecker ( ) const
virtual

Returns true, if a region model checker needs to implement specific methods to properly use this backend.

Returns false, if it is safe and reasonable to use this backend with any given region model checker.

Note
this returns false in the base class, but might return true in derived classes.

Reimplemented in storm::modelchecker::OrderBasedMonotonicityBackend< ParametricType, ConstantType >.

Definition at line 44 of file MonotonicityBackend.cpp.

◆ setMonotoneParameter()

template<typename ParametricType >
void storm::modelchecker::MonotonicityBackend< ParametricType >::setMonotoneParameter ( VariableType const &  parameter,
MonotonicityKind const &  kind 
)

Sets parameters that are assumed to be monotone throughout the analysis.

Previously specified parameters are overwritten.

Parameters
parameterthe parameter that is assumed to be monotone
kindthe kind of monotonicity. Must be either increasing, decreasing or constant.

Definition at line 9 of file MonotonicityBackend.cpp.

◆ updateMonotonicity()

template<typename ParametricType >
void storm::modelchecker::MonotonicityBackend< ParametricType >::updateMonotonicity ( storm::Environment const &  env,
AnnotatedRegion< ParametricType > &  region 
)
virtual

Updates the monotonicity information for the given region.

Assumes that some monotonicity information is already present (potentially inherited from a parent region) and potentially sharpens the results for the given region.

Reimplemented in storm::modelchecker::OrderBasedMonotonicityBackend< ParametricType, ConstantType >.

Definition at line 33 of file MonotonicityBackend.cpp.

◆ updateMonotonicityBeforeSplitting()

template<typename ParametricType >
void storm::modelchecker::MonotonicityBackend< ParametricType >::updateMonotonicityBeforeSplitting ( storm::Environment const &  env,
AnnotatedRegion< ParametricType > &  region 
)
virtual

Updates the monotonicity information for the given region right before splitting it.

Reimplemented in storm::modelchecker::OrderBasedMonotonicityBackend< ParametricType, ConstantType >.

Definition at line 39 of file MonotonicityBackend.cpp.

Member Data Documentation

◆ globallyKnownMonotonicityInformation

template<typename ParametricType >
std::map<VariableType, MonotonicityKind> storm::modelchecker::MonotonicityBackend< ParametricType >::globallyKnownMonotonicityInformation
protected

Definition at line 74 of file MonotonicityBackend.h.

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