storm::modelchecker::AnnotatedRegion< ParametricType > Struct Template Reference

#include <AnnotatedRegion.h>

Collaboration diagram for storm::modelchecker::AnnotatedRegion< ParametricType >:

Public Types
using	Region = storm::storage::ParameterRegion< ParametricType >
using	VariableType = typename Region::VariableType
using	CoefficientType = typename Region::CoefficientType

Public Member Functions
	AnnotatedRegion (Region const &region)
void	propagateAnnotationsToSubregions (bool allowDeleteAnnotationsOfThis)
void	splitAndPropagate (typename Region::Valuation const &splittingPoint, std::set< VariableType > const &consideredVariables, std::set< VariableType > const &discreteVariables, bool allowDeleteAnnotationsOfThis)
void	splitLeafNodeAtCenter (std::set< VariableType > const &splittingVariables, std::set< VariableType > const &discreteVariables, bool allowDeleteAnnotationsOfThis)
void	postOrderTraverseSubRegions (std::function< void(AnnotatedRegion< ParametricType > &)> const &visitor)
void	preOrderTraverseSubRegions (std::function< void(AnnotatedRegion< ParametricType > &)> const &visitor)
uint64_t	getMaxDepthOfSubRegions () const
bool	updateValueBound (CoefficientType const &newValue, storm::OptimizationDirection dir)
	what is known about this region in terms of monotonicity

Public Attributes
std::vector< AnnotatedRegion< ParametricType > >	subRegions
Region const	region
	The subregions of this region.
uint64_t	refinementDepth {0}
	The region this is an annotation for.
storm::modelchecker::RegionResult	result {storm::modelchecker::RegionResult::Unknown}
	The depth of the refinement tree this region is in.
bool	resultKnownThroughMonotonicity {false}
	The result of the analysis of this region.
storm::modelchecker::MonotonicityAnnotation< ParametricType >	monotonicityAnnotation
	Whether the result is known through monotonicity.
storm::utility::Maximum< CoefficientType >	knownLowerValueBound
storm::utility::Minimum< CoefficientType >	knownUpperValueBound

Detailed Description

template<typename ParametricType>
struct storm::modelchecker::AnnotatedRegion< ParametricType >

Definition at line 10 of file AnnotatedRegion.h.

Member Typedef Documentation

CoefficientType

template<typename ParametricType >

using storm::modelchecker::AnnotatedRegion< ParametricType >::CoefficientType = typename Region::CoefficientType

Definition at line 13 of file AnnotatedRegion.h.

Region

template<typename ParametricType >

using storm::modelchecker::AnnotatedRegion< ParametricType >::Region = storm::storage::ParameterRegion<ParametricType>

Definition at line 11 of file AnnotatedRegion.h.

VariableType

template<typename ParametricType >

using storm::modelchecker::AnnotatedRegion< ParametricType >::VariableType = typename Region::VariableType

Definition at line 12 of file AnnotatedRegion.h.

Constructor & Destructor Documentation

AnnotatedRegion()

template<typename ParametricType >

storm::modelchecker::AnnotatedRegion< ParametricType >::AnnotatedRegion ( Region const &  region )

explicit

Definition at line 6 of file AnnotatedRegion.cpp.

Member Function Documentation

getMaxDepthOfSubRegions()

template<typename ParametricType >

uint64_t storm::modelchecker::AnnotatedRegion< ParametricType >::getMaxDepthOfSubRegions

(

)

const

Definition at line 70 of file AnnotatedRegion.cpp.

postOrderTraverseSubRegions()

template<typename ParametricType >

void storm::modelchecker::AnnotatedRegion< ParametricType >::postOrderTraverseSubRegions

(

std::function< void(AnnotatedRegion< ParametricType > &)> const &

visitor

)

Definition at line 54 of file AnnotatedRegion.cpp.

preOrderTraverseSubRegions()

template<typename ParametricType >

void storm::modelchecker::AnnotatedRegion< ParametricType >::preOrderTraverseSubRegions

(

std::function< void(AnnotatedRegion< ParametricType > &)> const &

visitor

)

Definition at line 62 of file AnnotatedRegion.cpp.

propagateAnnotationsToSubregions()

template<typename ParametricType >

void storm::modelchecker::AnnotatedRegion< ParametricType >::propagateAnnotationsToSubregions

(

bool

allowDeleteAnnotationsOfThis

)

Definition at line 11 of file AnnotatedRegion.cpp.

splitAndPropagate()

template<typename ParametricType >

void storm::modelchecker::AnnotatedRegion< ParametricType >::splitAndPropagate	(	typename Region::Valuation const &	splittingPoint,
		std::set< VariableType > const &	consideredVariables,
		std::set< VariableType > const &	discreteVariables,
		bool	allowDeleteAnnotationsOfThis
	)

Definition at line 35 of file AnnotatedRegion.cpp.

splitLeafNodeAtCenter()

template<typename ParametricType >

void storm::modelchecker::AnnotatedRegion< ParametricType >::splitLeafNodeAtCenter	(	std::set< VariableType > const &	splittingVariables,
		std::set< VariableType > const &	discreteVariables,
		bool	allowDeleteAnnotationsOfThis
	)

Definition at line 47 of file AnnotatedRegion.cpp.

updateValueBound()

template<typename ParametricType >

bool storm::modelchecker::AnnotatedRegion< ParametricType >::updateValueBound	(	CoefficientType const &	newValue,
		storm::OptimizationDirection	dir
	)

what is known about this region in terms of monotonicity

Definition at line 79 of file AnnotatedRegion.cpp.

Member Data Documentation

knownLowerValueBound

template<typename ParametricType >

storm::utility::Maximum<CoefficientType> storm::modelchecker::AnnotatedRegion< ParametricType >::knownLowerValueBound

Definition at line 44 of file AnnotatedRegion.h.

knownUpperValueBound

template<typename ParametricType >

storm::utility::Minimum<CoefficientType> storm::modelchecker::AnnotatedRegion< ParametricType >::knownUpperValueBound

Definition at line 45 of file AnnotatedRegion.h.

monotonicityAnnotation

template<typename ParametricType >

storm::modelchecker::MonotonicityAnnotation<ParametricType> storm::modelchecker::AnnotatedRegion< ParametricType >::monotonicityAnnotation

Whether the result is known through monotonicity.

Definition at line 40 of file AnnotatedRegion.h.

refinementDepth

template<typename ParametricType >

uint64_t storm::modelchecker::AnnotatedRegion< ParametricType >::refinementDepth {0}

The region this is an annotation for.

Definition at line 35 of file AnnotatedRegion.h.

region

template<typename ParametricType >

Region const storm::modelchecker::AnnotatedRegion< ParametricType >::region

The subregions of this region.

Definition at line 33 of file AnnotatedRegion.h.

result

template<typename ParametricType >

storm::modelchecker::RegionResult storm::modelchecker::AnnotatedRegion< ParametricType >::result {storm::modelchecker::RegionResult::Unknown}

The depth of the refinement tree this region is in.

Definition at line 37 of file AnnotatedRegion.h.

resultKnownThroughMonotonicity

template<typename ParametricType >

bool storm::modelchecker::AnnotatedRegion< ParametricType >::resultKnownThroughMonotonicity {false}

The result of the analysis of this region.

Definition at line 38 of file AnnotatedRegion.h.

subRegions

template<typename ParametricType >

std::vector<AnnotatedRegion<ParametricType> > storm::modelchecker::AnnotatedRegion< ParametricType >::subRegions

Definition at line 31 of file AnnotatedRegion.h.

---

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

• src/storm-pars/modelchecker/region/AnnotatedRegion.h
• src/storm-pars/modelchecker/region/AnnotatedRegion.cpp