#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 const &topStates, storm::storage::BitVector const &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 19 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 21 of file OrderExtender.h.

◆ Monotonicity

template<typename ValueType, typename ConstantType>

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

Definition at line 23 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 22 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 24 of file OrderExtender.cpp.

◆ OrderExtender() [2/2]

template<typename ValueType, typename ConstantType>

storm::analysis::OrderExtender< ValueType, ConstantType >::OrderExtender	(	storm::storage::BitVector const &	topStates,
		storm::storage::BitVector const &	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 34 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 786 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 814 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 235 of file OrderExtender.cpp.

◆ getMonotoncityChecker()

template<typename ValueType, typename ConstantType>

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

Definition at line 850 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 800 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 855 of file OrderExtender.cpp.

◆ initializeMinMaxValues()

template<typename ValueType, typename ConstantType>

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

Definition at line 680 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 842 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 754 of file OrderExtender.cpp.

◆ setMaxValuesInit()

template<typename ValueType, typename ConstantType>

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

Definition at line 780 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 712 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 733 of file OrderExtender.cpp.

◆ setMinValuesInit()

template<typename ValueType, typename ConstantType>

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

Definition at line 774 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 794 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 808 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 187 of file OrderExtender.cpp.

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

src/storm-pars/modelchecker/region/monotonicity/OrderExtender.h
src/storm-pars/modelchecker/region/monotonicity/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()