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

#include <AssumptionMaker.h>

Public Member Functions
	AssumptionMaker (storage::SparseMatrix< ValueType > matrix)
	Constructs AssumptionMaker based on the matrix of the model.
std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus >	createAndCheckAssumptions (uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region) const
	Creates assumptions, and checks them, only VALID and UNKNOWN assumptions are returned.
std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus >	createAndCheckAssumptions (uint_fast64_t val1, uint_fast64_t val2, std::shared_ptr< Order > order, storage::ParameterRegion< ValueType > region, std::vector< ConstantType > const minValues, std::vector< ConstantType > const maxValue) const
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 > > const &samples)
	Sets the sample values to the given vector.

Detailed Description

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

Definition at line 15 of file AssumptionMaker.h.

Constructor & Destructor Documentation

AssumptionMaker()

template<typename ValueType , typename ConstantType >

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

(

storage::SparseMatrix< ValueType >

matrix

)

Constructs AssumptionMaker based on the matrix of the model.

Parameters

matrix

The matrix of the model.

Definition at line 6 of file AssumptionMaker.cpp.

Member Function Documentation

createAndCheckAssumptions() [1/2]

template<typename ValueType , typename ConstantType >

std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus > storm::analysis::AssumptionMaker< ValueType, ConstantType >::createAndCheckAssumptions	(	uint_fast64_t	val1,
		uint_fast64_t	val2,
		std::shared_ptr< Order >	order,
		storage::ParameterRegion< ValueType >	region
	)		const

Creates assumptions, and checks them, only VALID and UNKNOWN assumptions are returned.

If one assumption is VALID, this assumption will be returned as only assumption. Possible results: AssumptionStatus::VALID, AssumptionStatus::UNKNOWN.

Parameters

val1	First state number.
val2	Second state number.
order	The order on which the assumptions are checked.
region	The region for the parameters.

Returns

Map with at most three assumptions, and the validation.

Definition at line 15 of file AssumptionMaker.cpp.

createAndCheckAssumptions() [2/2]

template<typename ValueType , typename ConstantType >

std::map< std::shared_ptr< expressions::BinaryRelationExpression >, AssumptionStatus > storm::analysis::AssumptionMaker< ValueType, ConstantType >::createAndCheckAssumptions	(	uint_fast64_t	val1,
		uint_fast64_t	val2,
		std::shared_ptr< Order >	order,
		storage::ParameterRegion< ValueType >	region,
		std::vector< ConstantType > const	minValues,
		std::vector< ConstantType > const	maxValue
	)		const

Definition at line 23 of file AssumptionMaker.cpp.

initializeCheckingOnSamples()

template<typename ValueType , typename ConstantType >

void storm::analysis::AssumptionMaker< 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 71 of file AssumptionMaker.cpp.

setSampleValues()

template<typename ValueType , typename ConstantType >

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

(

std::vector< std::vector< ConstantType > > const &

samples

)

Sets the sample values to the given vector.

Parameters

samples

The new value for samples.

Definition at line 78 of file AssumptionMaker.cpp.

---

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

• src/storm-pars/analysis/AssumptionMaker.h
• src/storm-pars/analysis/AssumptionMaker.cpp