#include <RegionRefinementChecker.h>

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

using	VariableType = typename storm::storage::ParameterRegion< ParametricType >::VariableType

using	Valuation = typename storm::storage::ParameterRegion< ParametricType >::Valuation

Public Member Functions
	RegionRefinementChecker (std::unique_ptr< RegionModelChecker< ParametricType > > &&regionChecker)

	~RegionRefinementChecker ()=default

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

void	specify (Environment const &env, std::shared_ptr< storm::models::ModelBase > parametricModel, CheckTask< storm::logic::Formula, ParametricType > const &checkTask, RegionSplittingStrategy splittingStrategy=RegionSplittingStrategy(), std::set< VariableType > const &discreteVariables={}, std::shared_ptr< MonotonicityBackend< ParametricType > > monotonicityBackend={}, bool allowModelSimplifications=true, bool graphPreserving=true)

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

std::pair< CoefficientType, Valuation >	computeExtremalValueHelper (Environment const &env, storm::storage::ParameterRegion< ParametricType > const &region, storm::solver::OptimizationDirection const &dir, std::function< bool(CoefficientType, CoefficientType)> acceptGlobalBound, std::function< bool(CoefficientType)> rejectInstance)
	Finds the extremal value within the given region and with the given precision.

std::pair< CoefficientType, 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)
	Finds the extremal value within the given region and with the given precision.

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.

Detailed Description

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

Definition at line 30 of file RegionRefinementChecker.h.

Member Typedef Documentation

◆ CoefficientType

template<typename ParametricType >

using storm::modelchecker::RegionRefinementChecker< ParametricType >::CoefficientType = typename storm::storage::ParameterRegion<ParametricType>::CoefficientType

Definition at line 32 of file RegionRefinementChecker.h.

◆ Valuation

template<typename ParametricType >

using storm::modelchecker::RegionRefinementChecker< ParametricType >::Valuation = typename storm::storage::ParameterRegion<ParametricType>::Valuation

Definition at line 34 of file RegionRefinementChecker.h.

◆ VariableType

template<typename ParametricType >

using storm::modelchecker::RegionRefinementChecker< ParametricType >::VariableType = typename storm::storage::ParameterRegion<ParametricType>::VariableType

Definition at line 33 of file RegionRefinementChecker.h.

Constructor & Destructor Documentation

◆ RegionRefinementChecker()

template<typename ParametricType >

storm::modelchecker::RegionRefinementChecker< ParametricType >::RegionRefinementChecker ( std::unique_ptr< RegionModelChecker< ParametricType > > && regionChecker )

Definition at line 24 of file RegionRefinementChecker.cpp.

◆ ~RegionRefinementChecker()

template<typename ParametricType >

storm::modelchecker::RegionRefinementChecker< ParametricType >::~RegionRefinementChecker ( )

default

Member Function Documentation

◆ canHandle()

template<typename ParametricType >

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

Definition at line 30 of file RegionRefinementChecker.cpp.

◆ computeExtremalValue()

template<typename ParametricType >

std::pair< typename storm::storage::ParameterRegion< ParametricType >::CoefficientType, typename storm::storage::ParameterRegion< ParametricType >::Valuation > storm::modelchecker::RegionRefinementChecker< 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
	)

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

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

Returns

Definition at line 306 of file RegionRefinementChecker.cpp.

◆ computeExtremalValueHelper()

template<typename ParametricType >

std::pair< typename storm::storage::ParameterRegion< ParametricType >::CoefficientType, typename storm::storage::ParameterRegion< ParametricType >::Valuation > storm::modelchecker::RegionRefinementChecker< ParametricType >::computeExtremalValueHelper	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		storm::solver::OptimizationDirection const &	dir,
		std::function< bool(CoefficientType, CoefficientType)>	acceptGlobalBound,
		std::function< bool(CoefficientType)>	rejectInstance
	)

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

Parameters

env
region	The region in which to optimize
dir	The direction in which to optimize
acceptGlobalBound	input is a (1) proposed global bound on the value and (2) a new value, output whether we will accept the new value if the global bound holds
rejectInstance	input some value from the parameter space, output whether we will reject because this exists

Returns

Definition at line 212 of file RegionRefinementChecker.cpp.

◆ performRegionPartitioning()

template<typename ParametricType >

std::unique_ptr< storm::modelchecker::RegionRefinementCheckResult< ParametricType > > storm::modelchecker::RegionRefinementChecker< ParametricType >::performRegionPartitioning	(	Environment const &	env,
		storm::storage::ParameterRegion< ParametricType > const &	region,
		std::optional< ParametricType >	coverageThreshold,
		std::optional< uint64_t >	depthThreshold = `std::nullopt`,
		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 122 of file RegionRefinementChecker.cpp.

◆ specify()

template<typename ParametricType >

void storm::modelchecker::RegionRefinementChecker< ParametricType >::specify	(	Environment const &	env,
		std::shared_ptr< storm::models::ModelBase >	parametricModel,
		CheckTask< storm::logic::Formula, ParametricType > const &	checkTask,
		RegionSplittingStrategy	splittingStrategy = `RegionSplittingStrategy()`,
		std::set< VariableType > const &	discreteVariables = `{}`,
		std::shared_ptr< MonotonicityBackend< ParametricType > >	monotonicityBackend = `{}`,
		bool	allowModelSimplifications = `true`,
		bool	graphPreserving = `true`
	)

Definition at line 36 of file RegionRefinementChecker.cpp.

◆ verifyRegion()

template<typename ParametricType >

bool storm::modelchecker::RegionRefinementChecker< ParametricType >::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.

Returns

Definition at line 325 of file RegionRefinementChecker.cpp.

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

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

Public Types

Public Member Functions

Detailed Description

Member Typedef Documentation

◆ CoefficientType

◆ Valuation

◆ VariableType

Constructor & Destructor Documentation

◆ RegionRefinementChecker()

◆ ~RegionRefinementChecker()

Member Function Documentation

◆ canHandle()

◆ computeExtremalValue()

◆ computeExtremalValueHelper()

◆ performRegionPartitioning()

◆ specify()

◆ verifyRegion()