storm::analysis::MonotonicityHelper< ValueType, ConstantType > Class Template Reference

#include <MonotonicityHelper.h>

Public Types
typedef utility::parametric::VariableType< ValueType >::type	VariableType
typedef utility::parametric::CoefficientType< ValueType >::type	CoefficientType
typedef MonotonicityResult< VariableType >::Monotonicity	Monotonicity
typedef storage::ParameterRegion< ValueType >	Region

Public Member Functions
	MonotonicityHelper (std::shared_ptr< models::sparse::Model< ValueType > > model, std::vector< std::shared_ptr< logic::Formula const > > formulas, std::vector< storage::ParameterRegion< ValueType > > regions, uint_fast64_t numberOfSamples=0, double const &precision=0.000001, bool dotOutput=false)
	Constructor of MonotonicityHelper.
std::map< std::shared_ptr< Order >, std::pair< std::shared_ptr< MonotonicityResult< VariableType > >, std::vector< std::shared_ptr< expressions::BinaryRelationExpression > > > >	checkMonotonicityInBuild (std::ostream &outfile, bool usePLA=false, std::string dotOutfileName="dotOutput")
	Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity.
std::shared_ptr< LocalMonotonicityResult< VariableType > >	createLocalMonotonicityResult (std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region)
	Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity.
Monotonicity	checkLocalMonotonicity (std::shared_ptr< Order > order, uint_fast64_t state, VariableType var, storage::ParameterRegion< ValueType > region)
	Checks for local monotonicity at the given state.

Static Public Member Functions
static std::pair< bool, bool >	checkDerivative (ValueType derivative, storage::ParameterRegion< ValueType > reg)
	Checks if a derivative >=0 or/and <=0.

Detailed Description

template<typename ValueType, typename ConstantType>
class storm::analysis::MonotonicityHelper< ValueType, ConstantType >

Definition at line 32 of file MonotonicityHelper.h.

Member Typedef Documentation

CoefficientType

template<typename ValueType , typename ConstantType >

typedef utility::parametric::CoefficientType<ValueType>::type storm::analysis::MonotonicityHelper< ValueType, ConstantType >::CoefficientType

Definition at line 35 of file MonotonicityHelper.h.

Monotonicity

template<typename ValueType , typename ConstantType >

typedef MonotonicityResult<VariableType>::Monotonicity storm::analysis::MonotonicityHelper< ValueType, ConstantType >::Monotonicity

Definition at line 36 of file MonotonicityHelper.h.

Region

template<typename ValueType , typename ConstantType >

typedef storage::ParameterRegion<ValueType> storm::analysis::MonotonicityHelper< ValueType, ConstantType >::Region

Definition at line 37 of file MonotonicityHelper.h.

VariableType

template<typename ValueType , typename ConstantType >

typedef utility::parametric::VariableType<ValueType>::type storm::analysis::MonotonicityHelper< ValueType, ConstantType >::VariableType

Definition at line 34 of file MonotonicityHelper.h.

Constructor & Destructor Documentation

MonotonicityHelper()

template<typename ValueType , typename ConstantType >

storm::analysis::MonotonicityHelper< ValueType, ConstantType >::MonotonicityHelper	(	std::shared_ptr< models::sparse::Model< ValueType > >	model,
		std::vector< std::shared_ptr< logic::Formula const > >	formulas,
		std::vector< storage::ParameterRegion< ValueType > >	regions,
		uint_fast64_t	numberOfSamples = 0,
		double const &	precision = 0.000001,
		bool	dotOutput = false
	)

Constructor of MonotonicityHelper.

Parameters

model	The model considered.
formulas	The formulas considered.
regions	The regions to consider.
numberOfSamples	Number of samples taken for monotonicity checking, default 0, if 0 then no check on samples is executed.
precision	Precision on which the samples are compared
dotOutput	Whether or not dot output should be generated for the ROs.

Definition at line 20 of file MonotonicityHelper.cpp.

Member Function Documentation

checkDerivative()

template<typename ValueType , typename ConstantType >

static std::pair< bool, bool > storm::analysis::MonotonicityHelper< ValueType, ConstantType >::checkDerivative ( ValueType  derivative, storage::ParameterRegion< ValueType >  reg  )

inlinestatic

Checks if a derivative >=0 or/and <=0.

Parameters

derivative

The derivative you want to check

Returns

pair of bools, >= 0 and <= 0

Definition at line 60 of file MonotonicityHelper.h.

checkLocalMonotonicity()

template<typename ValueType , typename ConstantType >

Monotonicity storm::analysis::MonotonicityHelper< ValueType, ConstantType >::checkLocalMonotonicity	(	std::shared_ptr< Order >	order,
		uint_fast64_t	state,
		VariableType	var,
		storage::ParameterRegion< ValueType >	region
	)

Checks for local monotonicity at the given state.

Parameters

order	the order on which the monotonicity should be checked
state	the considerd state
var	the variable in which we check for monotonicity
region	the region on which we check the monotonicity

Returns

Incr, Decr, Constant, Unknown or Not

checkMonotonicityInBuild()

template<typename ValueType , typename ConstantType >

std::map< std::shared_ptr< Order >, std::pair< std::shared_ptr< MonotonicityResult< typename MonotonicityHelper< ValueType, ConstantType >::VariableType > >, std::vector< std::shared_ptr< expressions::BinaryRelationExpression > > > > storm::analysis::MonotonicityHelper< ValueType, ConstantType >::checkMonotonicityInBuild	(	std::ostream &	outfile,
		bool	usePLA = false,
		std::string	dotOutfileName = "dotOutput"
	)

Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity.

Parameters

outfile	Outfile to which results are written.
dotOutfileName	Name for the files of the dot outputs should they be generated

Returns

Map which maps each order to its Reachability Order and used assumptions.

Definition at line 82 of file MonotonicityHelper.cpp.

createLocalMonotonicityResult()

template<typename ValueType , typename ConstantType >

std::shared_ptr< LocalMonotonicityResult< typename MonotonicityHelper< ValueType, ConstantType >::VariableType > > storm::analysis::MonotonicityHelper< ValueType, ConstantType >::createLocalMonotonicityResult	(	std::shared_ptr< Order >	order,
		storage::ParameterRegion< ValueType >	region
	)

Builds Reachability Orders for the given model and simultaneously uses them to check for Monotonicity.

Definition at line 159 of file MonotonicityHelper.cpp.

---

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

• src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.h
• src/storm-pars/modelchecker/region/monotonicity/MonotonicityHelper.cpp