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

#include <AssumptionChecker.h>

Public Types
typedef utility::parametric::VariableType< ValueType >::type	VariableType
typedef utility::parametric::CoefficientType< ValueType >::type	CoefficientType

Public Member Functions
	AssumptionChecker (storage::SparseMatrix< ValueType > matrix)
	Constructs an AssumptionChecker.
	AssumptionChecker (std::shared_ptr< logic::Formula const > formula, std::shared_ptr< models::sparse::Mdp< ValueType > > model, uint_fast64_t const numberOfSamples)
	Constructs an AssumptionChecker based on the number of samples, for the given formula and model.
void	initializeCheckingOnSamples (Environment const &env, std::shared_ptr< logic::Formula const > formula, std::shared_ptr< models::sparse::Dtmc< ValueType > > model, storage::ParameterRegion< ValueType > region, uint_fast64_t numberOfSamples)
	Initializes the given number of sample points for a given model, formula and region.
void	setSampleValues (std::vector< std::vector< ConstantType > > samples)
	Sets the sample values to the given vector and useSamples to true.
AssumptionStatus	validateAssumption (Assumption const &assumption, std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region, std::vector< ConstantType > const minValues, std::vector< ConstantType > const maxValue) const
	Tries to validate an assumption based on the order and underlying transition matrix.
AssumptionStatus	validateAssumption (Assumption const &assumption, std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region) const

Detailed Description

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

Definition at line 25 of file AssumptionChecker.h.

Member Typedef Documentation

CoefficientType

template<typename ValueType, typename ConstantType>

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

Definition at line 28 of file AssumptionChecker.h.

VariableType

template<typename ValueType, typename ConstantType>

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

Definition at line 27 of file AssumptionChecker.h.

Constructor & Destructor Documentation

AssumptionChecker() [1/2]

template<typename ValueType, typename ConstantType>

storm::analysis::AssumptionChecker< ValueType, ConstantType >::AssumptionChecker

(

storage::SparseMatrix< ValueType >

matrix

)

Constructs an AssumptionChecker.

Parameters

matrix

The matrix of the considered model.

Definition at line 17 of file AssumptionChecker.cpp.

AssumptionChecker() [2/2]

template<typename ValueType, typename ConstantType>

storm::analysis::AssumptionChecker< ValueType, ConstantType >::AssumptionChecker	(	std::shared_ptr< logic::Formula const >	formula,
		std::shared_ptr< models::sparse::Mdp< ValueType > >	model,
		uint_fast64_t const	numberOfSamples )

Constructs an AssumptionChecker based on the number of samples, for the given formula and model.

Parameters

formula	The formula to check.
model	The mdp model to check the formula on.
numberOfSamples	Number of sample points.

Definition at line 68 of file AssumptionChecker.cpp.

Member Function Documentation

initializeCheckingOnSamples()

template<typename ValueType, typename ConstantType>

void storm::analysis::AssumptionChecker< ValueType, ConstantType >::initializeCheckingOnSamples	(	Environment const &	env,
		std::shared_ptr< logic::Formula const >	formula,
		std::shared_ptr< models::sparse::Dtmc< ValueType > >	model,
		storage::ParameterRegion< ValueType >	region,
		uint_fast64_t	numberOfSamples )

Initializes the given number of sample points for a given model, formula and region.

Parameters

env	The environment used for checking the samples.
formula	The formula to compute the samples for.
model	The considered model.
region	The region of the model's parameters.
numberOfSamples	Number of sample points.

Definition at line 23 of file AssumptionChecker.cpp.

setSampleValues()

template<typename ValueType, typename ConstantType>

void storm::analysis::AssumptionChecker< ValueType, ConstantType >::setSampleValues

(

std::vector< std::vector< ConstantType > >

samples

)

Sets the sample values to the given vector and useSamples to true.

Parameters

samples

The new value for samples.

Definition at line 62 of file AssumptionChecker.cpp.

validateAssumption() [1/2]

template<typename ValueType, typename ConstantType>

AssumptionStatus storm::analysis::AssumptionChecker< ValueType, ConstantType >::validateAssumption	(	Assumption const &	assumption,
		std::shared_ptr< Order >	order,
		storage::ParameterRegion< ValueType >	region ) const

Definition at line 297 of file AssumptionChecker.cpp.

validateAssumption() [2/2]

template<typename ValueType, typename ConstantType>

AssumptionStatus storm::analysis::AssumptionChecker< ValueType, ConstantType >::validateAssumption	(	Assumption const &	assumption,
		std::shared_ptr< Order >	order,
		storage::ParameterRegion< ValueType >	region,
		std::vector< ConstantType > const	minValues,
		std::vector< ConstantType > const	maxValue ) const

Tries to validate an assumption based on the order and underlying transition matrix.

Parameters

assumption	The assumption to validate.
order	The order.
region	The region of the considered model.

Returns

AssumptionStatus::VALID, or AssumptionStatus::UNKNOWN, or AssumptionStatus::INVALID

Definition at line 74 of file AssumptionChecker.cpp.

---

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

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