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 (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 (uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr< expressions::BinaryRelationExpression > 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 (std::shared_ptr< expressions::BinaryRelationExpression > 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 19 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 70 of file AssumptionChecker.cpp.

Member Function Documentation

initializeCheckingOnSamples()

template<typename ValueType , typename ConstantType >

void storm::analysis::AssumptionChecker< ValueType, ConstantType >::initializeCheckingOnSamples	(	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

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 25 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 64 of file AssumptionChecker.cpp.

validateAssumption() [1/2]

template<typename ValueType , typename ConstantType >

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

Definition at line 315 of file AssumptionChecker.cpp.

validateAssumption() [2/2]

template<typename ValueType , typename ConstantType >

AssumptionStatus storm::analysis::AssumptionChecker< ValueType, ConstantType >::validateAssumption	(	uint_fast64_t	val1,
		uint_fast64_t	val2,
		std::shared_ptr< expressions::BinaryRelationExpression >	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 76 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