#include <RegionModelChecker.h>

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

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

Public Member Functions
	RegionModelChecker ()

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, bool generateRegionSplitEstimates, bool allowModelSimplifications=true)=0

virtual RegionResult	analyzeRegion (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, RegionResultHypothesis const &hypothesis=RegionResultHypothesis::Unknown, RegionResult const &initialResult=RegionResult::Unknown, bool sampleVerticesOfRegion=false, std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonotonicityResult=nullptr)=0
	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 ParametricType	getBoundAtInitState (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, storm::solver::OptimizationDirection const &dirForParameters)

std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ParametricType > >	performRegionRefinement (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, boost::optional< ParametricType > const &coverageThreshold, boost::optional< uint64_t > depthThreshold=boost::none, RegionResultHypothesis const &hypothesis=RegionResultHypothesis::Unknown, uint64_t monThresh=0)
	Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated).

virtual std::pair< ParametricType, typename storm::storage::ParameterRegion< ParametricType >::Valuation >	computeExtremalValue (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, storm::solver::OptimizationDirection const &dir, ParametricType const &precision, bool absolutePrecision, std::optional< storm::logic::Bound > const &boundInvariant=std::nullopt)
	Finds the extremal value within the given region and with the given precision.

virtual bool	verifyRegion (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, storm::logic::Bound const &bound)
	Checks whether the bound is satisfied on the complete region.

virtual bool	isRegionSplitEstimateSupported () const
	Returns true if region split estimation (a) was enabled when model and check task have been specified and (b) is supported by this region model checker.

virtual std::map< VariableType, double >	getRegionSplitEstimate () const
	Returns an estimate of the benefit of splitting the last checked region with respect to each parameter.

virtual std::shared_ptr< storm::analysis::Order >	extendOrder (std::shared_ptr< storm::analysis::Order > order, storm::storage::ParameterRegion< ParametricType > region)

virtual void	setConstantEntries (std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonotonicityResult)

bool	isUseMonotonicitySet () const

bool	isUseBoundsSet ()

bool	isOnlyGlobalSet ()

void	setUseMonotonicity (bool monotonicity=true)

void	setUseBounds (bool bounds=true)

void	setUseOnlyGlobal (bool global=true)

virtual void	setMaxSplitDimensions (uint64_t)
	When splitting, split in at most this many dimensions.

virtual void	resetMaxSplitDimensions ()
	When splitting, split in every dimension.

void	setMonotoneParameters (std::pair< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > > monotoneParameters)

Protected Member Functions
virtual void	extendLocalMonotonicityResult (storm::storage::ParameterRegion< ParametricType > const &region, std::shared_ptr< storm::analysis::Order > order, std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonotonicityResult)

virtual void	splitSmart (storm::storage::ParameterRegion< ParametricType > &region, std::vector< storm::storage::ParameterRegion< ParametricType > > &regionVector, storm::analysis::MonotonicityResult< VariableType > &monRes, bool splitForExtremum) const

Protected Attributes
uint_fast64_t	numberOfRegionsKnownThroughMonotonicity

boost::optional< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > >	monotoneIncrParameters

boost::optional< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > >	monotoneDecrParameters

Detailed Description

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

Definition at line 25 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 27 of file RegionModelChecker.h.

◆ VariableType

template<typename ParametricType >

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

Definition at line 28 of file RegionModelChecker.h.

Constructor & Destructor Documentation

◆ RegionModelChecker()

template<typename ParametricType >

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

Definition at line 25 of file RegionModelChecker.cpp.

◆ ~RegionModelChecker()

template<typename ParametricType >

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

virtualdefault

Member Function Documentation

◆ analyzeRegion()

template<typename ParametricType >

virtual RegionResult storm::modelchecker::RegionModelChecker< ParametricType >::analyzeRegion	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		RegionResultHypothesis const &	hypothesis = `RegionResultHypothesis::Unknown`,
		RegionResult const &	initialResult = `RegionResult::Unknown`,
		bool	sampleVerticesOfRegion = `false`,
		std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > >	localMonotonicityResult = `nullptr`
	)

pure virtual

Analyzes the given region.

Parameters

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

◆ 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.

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 30 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::SparseMdpParameterLiftingModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, ImpreciseType >, storm::modelchecker::SparseMdpParameterLiftingModelChecker< SparseModelType, PreciseType >, storm::modelchecker::ValidatingSparseParameterLiftingModelChecker< SparseModelType, ImpreciseType, PreciseType >, storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ImpreciseType >, and storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, PreciseType >.

◆ computeExtremalValue()

template<typename ParametricType >

std::pair< ParametricType, typename storm::storage::ParameterRegion< ParametricType >::Valuation > storm::modelchecker::RegionModelChecker< ParametricType >::computeExtremalValue	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		storm::solver::OptimizationDirection const &	dir,
		ParametricType const &	precision,
		bool	absolutePrecision,
		std::optional< storm::logic::Bound > const &	boundInvariant = `std::nullopt`
	)

virtual

Finds the extremal value within the given region and with the given precision.

The returned value v corresponds to the value at the returned valuation. The actual maximum (minimum) lies in the interval [v, v'] ([v', v]) where v' is based on the precision. (With absolute precision, v' = v +/- precision). TODO: Check documentation, which was incomplete.

Parameters

env
region	The region in which to optimize
dir	The direction in which to optimize
precision	The required precision (unless boundInvariant is set).
absolutePrecision	true iff precision should be measured absolutely
boundInvariant	if this invariant on v is violated, the algorithm may return v while violating the precision requirements.

Returns

Definition at line 344 of file RegionModelChecker.cpp.

◆ extendLocalMonotonicityResult()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::extendLocalMonotonicityResult	(	storm::storage::ParameterRegion< ParametricType > const &	region,
		std::shared_ptr< storm::analysis::Order >	order,
		std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > >	localMonotonicityResult
	)

protectedvirtual

Definition at line 337 of file RegionModelChecker.cpp.

◆ extendOrder()

template<typename ParametricType >

std::shared_ptr< storm::analysis::Order > storm::modelchecker::RegionModelChecker< ParametricType >::extendOrder	(	std::shared_ptr< storm::analysis::Order >	order,
		storm::storage::ParameterRegion< ParametricType >	region
	)

virtual

Definition at line 369 of file RegionModelChecker.cpp.

◆ getBoundAtInitState()

template<typename ParametricType >

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

virtual

Definition at line 49 of file RegionModelChecker.cpp.

◆ getRegionSplitEstimate()

template<typename ParametricType >

std::map< typename RegionModelChecker< ParametricType >::VariableType, double > storm::modelchecker::RegionModelChecker< ParametricType >::getRegionSplitEstimate ( ) const

virtual

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

This method should only be called if region split estimation is supported and enabled. If a parameter is assigned a high value, we should prefer splitting with respect to this parameter.

Reimplemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ImpreciseType >, and storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, PreciseType >.

Definition at line 363 of file RegionModelChecker.cpp.

◆ isOnlyGlobalSet()

template<typename ParametricType >

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

Definition at line 403 of file RegionModelChecker.cpp.

◆ isRegionSplitEstimateSupported()

template<typename ParametricType >

bool storm::modelchecker::RegionModelChecker< ParametricType >::isRegionSplitEstimateSupported ( ) const

virtual

Returns true if region split estimation (a) was enabled when model and check task have been specified and (b) is supported by this region model checker.

Reimplemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ImpreciseType >, and storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, PreciseType >.

Definition at line 358 of file RegionModelChecker.cpp.

◆ isUseBoundsSet()

template<typename ParametricType >

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

Definition at line 398 of file RegionModelChecker.cpp.

◆ isUseMonotonicitySet()

template<typename ParametricType >

bool storm::modelchecker::RegionModelChecker< ParametricType >::isUseMonotonicitySet ( ) const

Definition at line 393 of file RegionModelChecker.cpp.

◆ performRegionRefinement()

template<typename ParametricType >

std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ParametricType > > storm::modelchecker::RegionModelChecker< ParametricType >::performRegionRefinement	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		boost::optional< ParametricType > const &	coverageThreshold,
		boost::optional< uint64_t >	depthThreshold = `boost::none`,
		RegionResultHypothesis const &	hypothesis = `RegionResultHypothesis::Unknown`,
		uint64_t	monThresh = `0`
	)

Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated).

Parameters

region	the considered region
coverageThreshold	if given, the refinement stops as soon as the fraction of the area of the subregions with inconclusive result is less then this threshold
depthThreshold	if given, the refinement stops at the given depth. depth=0 means no refinement.
hypothesis	if not 'unknown', it is only checked whether the hypothesis holds within the given region.
monThresh	if given, determines at which depth to start using monotonicity

Definition at line 56 of file RegionModelChecker.cpp.

◆ resetMaxSplitDimensions()

template<typename ParametricType >

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

virtual

When splitting, split in every dimension.

Reimplemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ImpreciseType >, and storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, PreciseType >.

Definition at line 388 of file RegionModelChecker.cpp.

◆ setConstantEntries()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::setConstantEntries ( std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonotonicityResult )

virtual

Definition at line 377 of file RegionModelChecker.cpp.

◆ setMaxSplitDimensions()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::setMaxSplitDimensions ( uint64_t )

virtual

When splitting, split in at most this many dimensions.

Reimplemented in storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ConstantType >, storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, ImpreciseType >, and storm::modelchecker::SparseDtmcParameterLiftingModelChecker< SparseModelType, PreciseType >.

Definition at line 383 of file RegionModelChecker.cpp.

◆ setMonotoneParameters()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::setMonotoneParameters ( std::pair< std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType >, std::set< typename storm::storage::ParameterRegion< ParametricType >::VariableType > > monotoneParameters )

Definition at line 433 of file RegionModelChecker.cpp.

◆ setUseBounds()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::setUseBounds ( bool bounds = true )

Definition at line 413 of file RegionModelChecker.cpp.

◆ setUseMonotonicity()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::setUseMonotonicity ( bool monotonicity = true )

Definition at line 408 of file RegionModelChecker.cpp.

◆ setUseOnlyGlobal()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::setUseOnlyGlobal ( bool global = true )

Definition at line 419 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,
		bool	generateRegionSplitEstimates,
		bool	allowModelSimplifications = `true`
	)

pure virtual

◆ splitSmart()

template<typename ParametricType >

void storm::modelchecker::RegionModelChecker< ParametricType >::splitSmart	(	storm::storage::ParameterRegion< ParametricType > &	region,
		std::vector< storm::storage::ParameterRegion< ParametricType > > &	regionVector,
		storm::analysis::MonotonicityResult< VariableType > &	monRes,
		bool	splitForExtremum
	)		const

protectedvirtual

Definition at line 425 of file RegionModelChecker.cpp.

◆ verifyRegion()

template<typename ParametricType >

bool storm::modelchecker::RegionModelChecker< ParametricType >::verifyRegion	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		storm::logic::Bound const &	bound
	)

virtual

Checks whether the bound is satisfied on the complete region.

Returns

Definition at line 352 of file RegionModelChecker.cpp.

Member Data Documentation

◆ monotoneDecrParameters

template<typename ParametricType >

boost::optional<std::set<typename storm::storage::ParameterRegion<ParametricType>::VariableType> > storm::modelchecker::RegionModelChecker< ParametricType >::monotoneDecrParameters

protected

Definition at line 148 of file RegionModelChecker.h.

◆ monotoneIncrParameters

template<typename ParametricType >

boost::optional<std::set<typename storm::storage::ParameterRegion<ParametricType>::VariableType> > storm::modelchecker::RegionModelChecker< ParametricType >::monotoneIncrParameters

protected

Definition at line 147 of file RegionModelChecker.h.

◆ numberOfRegionsKnownThroughMonotonicity

template<typename ParametricType >

uint_fast64_t storm::modelchecker::RegionModelChecker< ParametricType >::numberOfRegionsKnownThroughMonotonicity

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

◆ VariableType

Constructor & Destructor Documentation

◆ RegionModelChecker()

◆ ~RegionModelChecker()

Member Function Documentation

◆ analyzeRegion()

◆ analyzeRegions()

◆ canHandle()

◆ computeExtremalValue()

◆ extendLocalMonotonicityResult()

◆ extendOrder()

◆ getBoundAtInitState()

◆ getRegionSplitEstimate()

◆ isOnlyGlobalSet()

◆ isRegionSplitEstimateSupported()

◆ isUseBoundsSet()

◆ isUseMonotonicitySet()

◆ performRegionRefinement()

◆ resetMaxSplitDimensions()

◆ setConstantEntries()

◆ setMaxSplitDimensions()

◆ setMonotoneParameters()

◆ setUseBounds()

◆ setUseMonotonicity()

◆ setUseOnlyGlobal()

◆ specify()

◆ splitSmart()

◆ verifyRegion()

Member Data Documentation

◆ monotoneDecrParameters

◆ monotoneIncrParameters

◆ numberOfRegionsKnownThroughMonotonicity