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

#include <MonotonicityHelper.h>

Classes
struct	ExpectedMonotonicityResult
	The result of the order-based monotonicity analysis for one reachability order: the order itself, the monotonicity result computed from it, and the assumptions the order was built on. More...

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 (Environment const &env, 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::vector< ExpectedMonotonicityResult >	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.

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 31 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 34 of file MonotonicityHelper.h.

Monotonicity

template<typename ValueType, typename ConstantType>

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

Definition at line 35 of file MonotonicityHelper.h.

Region

template<typename ValueType, typename ConstantType>

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

Definition at line 36 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 33 of file MonotonicityHelper.h.

Constructor & Destructor Documentation

MonotonicityHelper()

template<typename ValueType, typename ConstantType>

storm::analysis::MonotonicityHelper< ValueType, ConstantType >::MonotonicityHelper	(	Environment const &	env,
		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

env	The environment used for checking the samples.
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 21 of file MonotonicityHelper.cpp.

Member Function Documentation

checkDerivative()

template<typename ValueType, typename ConstantType>

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 70 of file MonotonicityHelper.h.

checkMonotonicityInBuild()

template<typename ValueType, typename ConstantType>

std::vector< typename MonotonicityHelper< ValueType, ConstantType >::ExpectedMonotonicityResult > 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

The reachability orders built, together with the monotonicity result and the assumptions used for each.

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 164 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