#include <OrderExtender.h>

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

typedef utility::parametric::VariableType< ValueType >::type	VariableType

typedef MonotonicityResult< VariableType >::Monotonicity	Monotonicity

Public Member Functions
	OrderExtender (std::shared_ptr< models::sparse::Model< ValueType > > model, std::shared_ptr< logic::Formula const > formula)
	Constructs a new OrderExtender.

	OrderExtender (storm::storage::BitVector topStates, storm::storage::BitVector bottomStates, storm::storage::SparseMatrix< ValueType > matrix)
	Constructs a new OrderExtender.

std::tuple< std::shared_ptr< Order >, uint_fast64_t, uint_fast64_t >	toOrder (storage::ParameterRegion< ValueType > region, std::shared_ptr< MonotonicityResult< VariableType > > monRes=nullptr)
	Creates an order based on the given formula.

std::tuple< std::shared_ptr< Order >, uint_fast64_t, uint_fast64_t >	extendOrder (std::shared_ptr< Order > order, storm::storage::ParameterRegion< ValueType > region, std::shared_ptr< MonotonicityResult< VariableType > > monRes=nullptr, std::shared_ptr< expressions::BinaryRelationExpression > assumption=nullptr)
	Extends the order for the given region.

void	setMinMaxValues (std::shared_ptr< Order > order, std::vector< ConstantType > &minValues, std::vector< ConstantType > &maxValues)

void	setMinValues (std::shared_ptr< Order > order, std::vector< ConstantType > &minValues)

void	setMaxValues (std::shared_ptr< Order > order, std::vector< ConstantType > &maxValues)

void	setMinValuesInit (std::vector< ConstantType > &minValues)

void	setMaxValuesInit (std::vector< ConstantType > &minValues)

void	setUnknownStates (std::shared_ptr< Order > order, uint_fast64_t state1, uint_fast64_t state2)

std::pair< uint_fast64_t, uint_fast64_t >	getUnknownStates (std::shared_ptr< Order > order) const

void	setUnknownStates (std::shared_ptr< Order > orderOriginal, std::shared_ptr< Order > orderCopy)

void	copyMinMax (std::shared_ptr< Order > orderOriginal, std::shared_ptr< Order > orderCopy)

void	initializeMinMaxValues (storage::ParameterRegion< ValueType > region)

void	checkParOnStateMonRes (uint_fast64_t s, std::shared_ptr< Order > order, typename OrderExtender< ValueType, ConstantType >::VariableType param, std::shared_ptr< MonotonicityResult< VariableType > > monResult)

bool	isHope (std::shared_ptr< Order > order)

MonotonicityChecker< ValueType > &	getMonotoncityChecker ()

std::vector< std::set< VariableType > > const &	getVariablesOccuringAtState ()

Detailed Description

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

Definition at line 20 of file OrderExtender.h.

Member Typedef Documentation

◆ CoefficientType

template<typename ValueType , typename ConstantType >

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

Definition at line 22 of file OrderExtender.h.

◆ Monotonicity

template<typename ValueType , typename ConstantType >

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

Definition at line 24 of file OrderExtender.h.

◆ VariableType

template<typename ValueType , typename ConstantType >

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

Definition at line 23 of file OrderExtender.h.

Constructor & Destructor Documentation

◆ OrderExtender() [1/2]

template<typename ValueType , typename ConstantType >

storm::analysis::OrderExtender< ValueType, ConstantType >::OrderExtender	(	std::shared_ptr< models::sparse::Model< ValueType > >	model,
		std::shared_ptr< logic::Formula const >	formula
	)

Constructs a new OrderExtender.

Parameters

model	The model for which the order should be extended.
formula	The considered formula.
region	The Region of the model's parameters.

Definition at line 23 of file OrderExtender.cpp.

◆ OrderExtender() [2/2]

template<typename ValueType , typename ConstantType >

storm::analysis::OrderExtender< ValueType, ConstantType >::OrderExtender	(	storm::storage::BitVector *	topStates,
		storm::storage::BitVector *	bottomStates,
		storm::storage::SparseMatrix< ValueType >	matrix
	)

Constructs a new OrderExtender.

Parameters

topStates	The top states of the order.
bottomStates	The bottom states of the order.
matrix	The matrix of the considered model.

Definition at line 33 of file OrderExtender.cpp.

Member Function Documentation

◆ checkParOnStateMonRes()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::checkParOnStateMonRes	(	uint_fast64_t	s,
		std::shared_ptr< Order >	order,
		typename OrderExtender< ValueType, ConstantType >::VariableType	param,
		std::shared_ptr< MonotonicityResult< VariableType > >	monResult
	)

Definition at line 777 of file OrderExtender.cpp.

◆ copyMinMax()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::copyMinMax	(	std::shared_ptr< Order >	orderOriginal,
		std::shared_ptr< Order >	orderCopy
	)

Definition at line 805 of file OrderExtender.cpp.

◆ extendOrder()

template<typename ValueType , typename ConstantType >

std::tuple< std::shared_ptr< Order >, uint_fast64_t, uint_fast64_t > storm::analysis::OrderExtender< ValueType, ConstantType >::extendOrder	(	std::shared_ptr< Order >	order,
		storm::storage::ParameterRegion< ValueType >	region,
		std::shared_ptr< MonotonicityResult< VariableType > >	monRes = `nullptr`,
		std::shared_ptr< expressions::BinaryRelationExpression >	assumption = `nullptr`
	)

Extends the order for the given region.

Parameters

order	pointer to the order.
region	The region on which the order needs to be extended.

Returns: Two states of which the current place in the order is unknown but needed. When the states have as number the number of states, no states are unplaced or needed.

Definition at line 234 of file OrderExtender.cpp.

◆ getMonotoncityChecker()

template<typename ValueType , typename ConstantType >

MonotonicityChecker< ValueType > & storm::analysis::OrderExtender< ValueType, ConstantType >::getMonotoncityChecker ( )

Definition at line 841 of file OrderExtender.cpp.

◆ getUnknownStates()

template<typename ValueType , typename ConstantType >

std::pair< uint_fast64_t, uint_fast64_t > storm::analysis::OrderExtender< ValueType, ConstantType >::getUnknownStates ( std::shared_ptr< Order > order ) const

Definition at line 791 of file OrderExtender.cpp.

◆ getVariablesOccuringAtState()

template<typename ValueType , typename ConstantType >

const std::vector< std::set< typename OrderExtender< ValueType, ConstantType >::VariableType > > & storm::analysis::OrderExtender< ValueType, ConstantType >::getVariablesOccuringAtState ( )

Definition at line 846 of file OrderExtender.cpp.

◆ initializeMinMaxValues()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::initializeMinMaxValues ( storage::ParameterRegion< ValueType > region )

Definition at line 673 of file OrderExtender.cpp.

◆ isHope()

template<typename ValueType , typename ConstantType >

bool storm::analysis::OrderExtender< ValueType, ConstantType >::isHope ( std::shared_ptr< Order > order )

Definition at line 833 of file OrderExtender.cpp.

◆ setMaxValues()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::setMaxValues	(	std::shared_ptr< Order >	order,
		std::vector< ConstantType > &	maxValues
	)

Definition at line 745 of file OrderExtender.cpp.

◆ setMaxValuesInit()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::setMaxValuesInit ( std::vector< ConstantType > & minValues )

Definition at line 771 of file OrderExtender.cpp.

◆ setMinMaxValues()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::setMinMaxValues	(	std::shared_ptr< Order >	order,
		std::vector< ConstantType > &	minValues,
		std::vector< ConstantType > &	maxValues
	)

Definition at line 703 of file OrderExtender.cpp.

◆ setMinValues()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::setMinValues	(	std::shared_ptr< Order >	order,
		std::vector< ConstantType > &	minValues
	)

Definition at line 724 of file OrderExtender.cpp.

◆ setMinValuesInit()

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::setMinValuesInit ( std::vector< ConstantType > & minValues )

Definition at line 765 of file OrderExtender.cpp.

◆ setUnknownStates() [1/2]

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::setUnknownStates	(	std::shared_ptr< Order >	order,
		uint_fast64_t	state1,
		uint_fast64_t	state2
	)

Definition at line 785 of file OrderExtender.cpp.

◆ setUnknownStates() [2/2]

template<typename ValueType , typename ConstantType >

void storm::analysis::OrderExtender< ValueType, ConstantType >::setUnknownStates	(	std::shared_ptr< Order >	orderOriginal,
		std::shared_ptr< Order >	orderCopy
	)

Definition at line 799 of file OrderExtender.cpp.

◆ toOrder()

template<typename ValueType , typename ConstantType >

std::tuple< std::shared_ptr< Order >, uint_fast64_t, uint_fast64_t > storm::analysis::OrderExtender< ValueType, ConstantType >::toOrder	(	storage::ParameterRegion< ValueType >	region,
		std::shared_ptr< MonotonicityResult< VariableType > >	monRes = `nullptr`
	)

Creates an order based on the given formula.

Parameters

monRes The monotonicity result so far.

Returns: A triple with a pointer to the order and two states of which the current place in the order is unknown but needed. When the states have as number the number of states, no states are unplaced but needed.

Definition at line 186 of file OrderExtender.cpp.

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

src/storm-pars/analysis/OrderExtender.h
src/storm-pars/analysis/OrderExtender.cpp

Public Types

Public Member Functions

Detailed Description

Member Typedef Documentation

◆ CoefficientType

◆ Monotonicity

◆ VariableType

Constructor & Destructor Documentation

◆ OrderExtender() [1/2]

◆ OrderExtender() [2/2]

Member Function Documentation

◆ checkParOnStateMonRes()

◆ copyMinMax()

◆ extendOrder()

◆ getMonotoncityChecker()

◆ getUnknownStates()

◆ getVariablesOccuringAtState()

◆ initializeMinMaxValues()

◆ isHope()

◆ setMaxValues()

◆ setMaxValuesInit()

◆ setMinMaxValues()

◆ setMinValues()

◆ setMinValuesInit()

◆ setUnknownStates() [1/2]

◆ setUnknownStates() [2/2]

◆ toOrder()