#include <RegionModelChecker.h>

Public Types
typedef storm::storage::ParameterRegion< ParametricType >::CoefficientType	CoefficientType

typedef storm::storage::ParameterRegion< ParametricType >::VariableType	VariableType

typedef storm::storage::ParameterRegion< ParametricType >::Valuation	Valuation

Public Member Functions
	RegionModelChecker ()=default

virtual	~RegionModelChecker ()=default

virtual bool	canHandle (std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, ParametricType > const &checkTask) const =0

virtual void	specify (Environment const &env, std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, ParametricType > const &checkTask, std::optional< RegionSplitEstimateKind > generateRegionSplitEstimates=std::nullopt, std::shared_ptr< MonotonicityBackend< ParametricType > > monotonicityBackend={}, bool allowModelSimplifications=true, bool graphPreserving=true)=0

virtual RegionResult	analyzeRegion (Environment const &env, AnnotatedRegion< ParametricType > &region, RegionResultHypothesis const &hypothesis=RegionResultHypothesis::Unknown, bool sampleVerticesOfRegion=false)=0
	Analyzes the given region.

RegionResult	analyzeRegion (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, RegionResultHypothesis const &hypothesis=RegionResultHypothesis::Unknown, bool sampleVerticesOfRegion=false)
	Analyzes the given region.

std::unique_ptr< storm::modelchecker::RegionCheckResult< ParametricType > >	analyzeRegions (Environment const &env, std::vector< storm::storage::ParameterRegion< ParametricType > > const &regions, std::vector< RegionResultHypothesis > const &hypotheses, bool sampleVerticesOfRegion=false)
	Analyzes the given regions.

virtual CoefficientType	getBoundAtInitState (Environment const &env, AnnotatedRegion< ParametricType > &region, storm::solver::OptimizationDirection const &dirForParameters)=0
	Over-approximates the value within the given region.

CoefficientType	getBoundAtInitState (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, storm::solver::OptimizationDirection const &dirForParameters)
	Over-approximates the value within the given region.

virtual std::pair< CoefficientType, Valuation >	getAndEvaluateGoodPoint (Environment const &env, AnnotatedRegion< ParametricType > &region, storm::solver::OptimizationDirection const &dirForParameters)=0
	Heuristically finds a point within the region and computes the value at the initial state for that point.

virtual RegionSplitEstimateKind	getDefaultRegionSplitEstimateKind (CheckTask< storm::logic::Formula, ParametricType > const &checkTask) const

virtual bool	isRegionSplitEstimateKindSupported (RegionSplitEstimateKind kind, CheckTask< storm::logic::Formula, ParametricType > const &checkTask) const

std::optional< RegionSplitEstimateKind >	getSpecifiedRegionSplitEstimateKind () const

virtual std::vector< CoefficientType >	obtainRegionSplitEstimates (std::set< VariableType > const &relevantParameters) const
	Returns an estimate of the benefit of splitting the last checked region with respect to each of the given parameters.

virtual bool	isMonotonicitySupported (MonotonicityBackend< ParametricType > const &backend, CheckTask< storm::logic::Formula, ParametricType > const &checkTask) const =0
	Returns whether this region model checker can work together with the given monotonicity backend.

Protected Member Functions
virtual void	specifySplitEstimates (std::optional< RegionSplitEstimateKind > splitEstimates, CheckTask< storm::logic::Formula, ParametricType > const &checkTask)

virtual void	specifyMonotonicity (std::shared_ptr< MonotonicityBackend< ParametricType > > backend, CheckTask< storm::logic::Formula, ParametricType > const &checkTask)

Protected Attributes
std::optional< storm::storage::ParameterRegion< ParametricType > >	lastCheckedRegion

std::optional< RegionSplitEstimateKind >	specifiedRegionSplitEstimateKind

std::shared_ptr< MonotonicityBackend< ParametricType > >	monotonicityBackend

Detailed Description

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

Definition at line 29 of file RegionModelChecker.h.

Member Typedef Documentation

◆ CoefficientType

template<typename ParametricType >

typedef storm::storage::ParameterRegion<ParametricType>::CoefficientType storm::modelchecker::RegionModelChecker< ParametricType >::CoefficientType

Definition at line 31 of file RegionModelChecker.h.

◆ Valuation

template<typename ParametricType >

typedef storm::storage::ParameterRegion<ParametricType>::Valuation storm::modelchecker::RegionModelChecker< ParametricType >::Valuation

Definition at line 33 of file RegionModelChecker.h.

◆ VariableType

template<typename ParametricType >

typedef storm::storage::ParameterRegion<ParametricType>::VariableType storm::modelchecker::RegionModelChecker< ParametricType >::VariableType

Definition at line 32 of file RegionModelChecker.h.

Constructor & Destructor Documentation

◆ RegionModelChecker()

template<typename ParametricType >

storm::modelchecker::RegionModelChecker< ParametricType >::RegionModelChecker ( )

default

◆ ~RegionModelChecker()

template<typename ParametricType >

virtual storm::modelchecker::RegionModelChecker< ParametricType >::~RegionModelChecker ( )

virtualdefault

Member Function Documentation

◆ analyzeRegion() [1/2]

template<typename ParametricType >

virtual RegionResult storm::modelchecker::RegionModelChecker< ParametricType >::analyzeRegion	(	Environment const &	env,
		AnnotatedRegion< ParametricType > &	region,
		RegionResultHypothesis const &	hypothesis = `RegionResultHypothesis::Unknown`,
		bool	sampleVerticesOfRegion = `false`
	)

pure virtual

Analyzes the given region.

Assumes that a property with a threshold was specified.

Precondition: specify must be called before.

Parameters

region	the region to analyze plus what is already known about this region. The annotations might be updated.
hypothesis	if not 'unknown', the region checker only tries to show the hypothesis
sampleVerticesOfRegion	enables sampling of the vertices of the region in cases where AllSat/AllViolated could not be shown.

Implemented in storm::modelchecker::SparseParameterLiftingModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType >.

◆ analyzeRegion() [2/2]

template<typename ParametricType >

RegionResult storm::modelchecker::RegionModelChecker< ParametricType >::analyzeRegion	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		RegionResultHypothesis const &	hypothesis = `RegionResultHypothesis::Unknown`,
		bool	sampleVerticesOfRegion = `false`
	)

Analyzes the given region.

Assumes that a property with a threshold was specified.

Precondition: specify must be called before.

Parameters

region	the region to analyze plus what is already known about this region. The annotations might be updated.
hypothesis	if not 'unknown', the region checker only tries to show the hypothesis
sampleVerticesOfRegion	enables sampling of the vertices of the region in cases where AllSat/AllViolated could not be shown.

Definition at line 13 of file RegionModelChecker.cpp.

◆ analyzeRegions()

template<typename ParametricType >

std::unique_ptr< storm::modelchecker::RegionCheckResult< ParametricType > > storm::modelchecker::RegionModelChecker< ParametricType >::analyzeRegions	(	Environment const &	env,
		std::vector< storm::storage::ParameterRegion< ParametricType > > const &	regions,
		std::vector< RegionResultHypothesis > const &	hypotheses,
		bool	sampleVerticesOfRegion = `false`
	)

Analyzes the given regions.

Precondition: specify must be called before.

Parameters

hypothesis if not 'unknown', we only try to show the hypothesis for each region If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown.

Definition at line 29 of file RegionModelChecker.cpp.

◆ canHandle()

template<typename ParametricType >

virtual bool storm::modelchecker::RegionModelChecker< ParametricType >::canHandle	(	std::shared_ptr< storm::models::ModelBase >	parametricModel,
		CheckTask< storm::logic::Formula, ParametricType > const &	checkTask
	)		const

pure virtual

Implemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType, Robust >, storm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType >.

◆ getAndEvaluateGoodPoint()

template<typename ParametricType >

virtual std::pair< CoefficientType, Valuation > storm::modelchecker::RegionModelChecker< ParametricType >::getAndEvaluateGoodPoint	(	Environment const &	env,
		AnnotatedRegion< ParametricType > &	region,
		storm::solver::OptimizationDirection const &	dirForParameters
	)

pure virtual

Heuristically finds a point within the region and computes the value at the initial state for that point.

The heuristic potentially takes annotations from the region such as monotonicity into account. Also data from previous analysis results might be used.

Precondition: specify must be called before and the model has a single initial state.

Parameters

region	the region to analyze plus what is already known about this region. The annotations might be updated.
dirForParameters	whether the heuristic tries to find a point with a high or low value

Returns: a pair of the value at the initial state and the point at which the value was computed

Implemented in storm::modelchecker::SparseParameterLiftingModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType >.

◆ getBoundAtInitState() [1/2]

template<typename ParametricType >

virtual CoefficientType storm::modelchecker::RegionModelChecker< ParametricType >::getBoundAtInitState	(	Environment const &	env,
		AnnotatedRegion< ParametricType > &	region,
		storm::solver::OptimizationDirection const &	dirForParameters
	)

pure virtual

Over-approximates the value within the given region.

If dirForParameters maximizes, the returned value is an upper bound on the maximum value within the region. If dirForParameters minimizes, the returned value is a lower bound on the minimum value within the region.

Precondition: specify must be called before and the model has a single initial state.

Parameters

region	the region to analyze plus what is already known about this region. The annotations might be updated.
dirForParameters	whether to maximize or minimize the value in the region

Returns: the over-approximated value within the region

Implemented in storm::modelchecker::SparseParameterLiftingModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType >.

◆ getBoundAtInitState() [2/2]

template<typename ParametricType >

RegionModelChecker< ParametricType >::CoefficientType storm::modelchecker::RegionModelChecker< ParametricType >::getBoundAtInitState	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		storm::solver::OptimizationDirection const &	dirForParameters
	)

Over-approximates the value within the given region.

If dirForParameters maximizes, the returned value is an upper bound on the maximum value within the region. If dirForParameters minimizes, the returned value is a lower bound on the minimum value within the region.

Precondition: specify must be called before and the model has a single initial state.

Parameters

region	the region to analyze plus what is already known about this region. The annotations might be updated.
dirForParameters	whether to maximize or minimize the value in the region

Returns: the over-approximated value within the region

Definition at line 21 of file RegionModelChecker.cpp.

◆ getDefaultRegionSplitEstimateKind()

template<typename ParametricType >

RegionSplitEstimateKind storm::modelchecker::RegionModelChecker< ParametricType >::getDefaultRegionSplitEstimateKind ( CheckTask< storm::logic::Formula, ParametricType > const & checkTask ) const

virtual

Returns: the default kind of region split estimate that this region model checker generates.

Definition at line 45 of file RegionModelChecker.cpp.

◆ getSpecifiedRegionSplitEstimateKind()

template<typename ParametricType >

std::optional< RegionSplitEstimateKind > storm::modelchecker::RegionModelChecker< ParametricType >::getSpecifiedRegionSplitEstimateKind ( ) const

Returns: the kind of region split estimation that was selected in the last call to specify (if any)

Definition at line 56 of file RegionModelChecker.cpp.

◆ isMonotonicitySupported()

template<typename ParametricType >

virtual bool storm::modelchecker::RegionModelChecker< ParametricType >::isMonotonicitySupported	(	MonotonicityBackend< ParametricType > const &	backend,
		CheckTask< storm::logic::Formula, ParametricType > const &	checkTask
	)		const

pure virtual

Returns whether this region model checker can work together with the given monotonicity backend.

Implemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType, Robust >, storm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType >.

◆ isRegionSplitEstimateKindSupported()

template<typename ParametricType >

bool storm::modelchecker::RegionModelChecker< ParametricType >::isRegionSplitEstimateKindSupported	(	RegionSplitEstimateKind	kind,
		CheckTask< storm::logic::Formula, ParametricType > const &	checkTask
	)		const

virtual

Returns: true if this can generate region split estimates of the given kind.

Definition at line 50 of file RegionModelChecker.cpp.

◆ obtainRegionSplitEstimates()

template<typename ParametricType >

std::vector< typename RegionModelChecker< ParametricType >::CoefficientType > storm::modelchecker::RegionModelChecker< ParametricType >::obtainRegionSplitEstimates ( std::set< VariableType > const & relevantParameters ) const

virtual

Returns an estimate of the benefit of splitting the last checked region with respect to each of the given parameters.

If a parameter is assigned a high value, we should prefer splitting with respect to this parameter.

Precondition: the last call to specify must have set generateRegionSplitEstimates to a non-empty value and either analyzeRegion or getBoundAtInitState must have been called before.

Reimplemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType, Robust >.

Definition at line 61 of file RegionModelChecker.cpp.

◆ specify()

template<typename ParametricType >

virtual void storm::modelchecker::RegionModelChecker< ParametricType >::specify	(	Environment const &	env,
		std::shared_ptr< storm::models::ModelBase >	parametricModel,
		CheckTask< storm::logic::Formula, ParametricType > const &	checkTask,
		std::optional< RegionSplitEstimateKind >	generateRegionSplitEstimates = `std::nullopt`,
		std::shared_ptr< MonotonicityBackend< ParametricType > >	monotonicityBackend = `{}`,
		bool	allowModelSimplifications = `true`,
		bool	graphPreserving = `true`
	)

pure virtual

Implemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType, Robust >, storm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, ConstantType >, and storm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType >.

◆ specifyMonotonicity()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::specifyMonotonicity	(	std::shared_ptr< MonotonicityBackend< ParametricType > >	backend,
		CheckTask< storm::logic::Formula, ParametricType > const &	checkTask
	)

protectedvirtual

Definition at line 83 of file RegionModelChecker.cpp.

◆ specifySplitEstimates()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::specifySplitEstimates	(	std::optional< RegionSplitEstimateKind >	splitEstimates,
		CheckTask< storm::logic::Formula, ParametricType > const &	checkTask
	)

protectedvirtual

Definition at line 75 of file RegionModelChecker.cpp.

Member Data Documentation

◆ lastCheckedRegion

template<typename ParametricType >

std::optional<storm::storage::ParameterRegion<ParametricType> > storm::modelchecker::RegionModelChecker< ParametricType >::lastCheckedRegion

protected

Definition at line 145 of file RegionModelChecker.h.

◆ monotonicityBackend

template<typename ParametricType >

std::shared_ptr<MonotonicityBackend<ParametricType> > storm::modelchecker::RegionModelChecker< ParametricType >::monotonicityBackend

protected

Definition at line 147 of file RegionModelChecker.h.

◆ specifiedRegionSplitEstimateKind

template<typename ParametricType >

std::optional<RegionSplitEstimateKind> storm::modelchecker::RegionModelChecker< ParametricType >::specifiedRegionSplitEstimateKind

protected

Definition at line 146 of file RegionModelChecker.h.

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

src/storm-pars/modelchecker/region/RegionModelChecker.h
src/storm-pars/modelchecker/region/RegionModelChecker.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ CoefficientType

◆ Valuation

◆ VariableType

Constructor & Destructor Documentation

◆ RegionModelChecker()

◆ ~RegionModelChecker()

Member Function Documentation

◆ analyzeRegion() [1/2]

◆ analyzeRegion() [2/2]

◆ analyzeRegions()

◆ canHandle()

◆ getAndEvaluateGoodPoint()

◆ getBoundAtInitState() [1/2]

◆ getBoundAtInitState() [2/2]

◆ getDefaultRegionSplitEstimateKind()

◆ getSpecifiedRegionSplitEstimateKind()

◆ isMonotonicitySupported()

◆ isRegionSplitEstimateKindSupported()

◆ obtainRegionSplitEstimates()

◆ specify()

◆ specifyMonotonicity()

◆ specifySplitEstimates()

Member Data Documentation

◆ lastCheckedRegion

◆ monotonicityBackend

◆ specifiedRegionSplitEstimateKind