This class lifts parameter choices to nondeterminism: For each row in the given matrix that considerd par parameters, the resulting matrix will have one row group consisting of 2^par rows. More...

#include <RobustParameterLifter.h>

Classes
class	RobustAbstractValuation

Public Types
typedef storm::utility::parametric::VariableType< ParametricType >::type	VariableType

typedef storm::utility::parametric::CoefficientType< ParametricType >::type	CoefficientType

typedef storm::analysis::MonotonicityResult< VariableType >::Monotonicity	Monotonicity

Public Member Functions
	RobustParameterLifter (storm::storage::SparseMatrix< ParametricType > const &pMatrix, std::vector< ParametricType > const &pVector, storm::storage::BitVector const &selectedRows, storm::storage::BitVector const &selectedColumns, bool generateRowLabels=false, bool useMonotonicity=false)
	Lifts the parameter choices to nondeterminisim.

void	specifyRegion (storm::storage::ParameterRegion< ParametricType > const &region, storm::solver::OptimizationDirection const &dirForParameters)

void	specifyRegion (storm::storage::ParameterRegion< ParametricType > const &region, storm::solver::OptimizationDirection const &dirForParameters, storm::storage::BitVector const &selectedRows)
	Specifies the region for the parameterlifter, the Bitvector works as a fixed (partial) scheduler, this might not give sound results!

void	specifyRegion (storm::storage::ParameterRegion< ParametricType > const &region, storm::solver::OptimizationDirection const &dirForParameters, std::shared_ptr< storm::analysis::Order > reachabilityOrder, std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > > localMonotonicityResult)
	Specifies the region for the parameterlifter, the reachability order is used to see if there is local monotonicity, such that a fixed (partial) scheduler can be used.

storm::storage::SparseMatrix< Interval > const &	getMatrix () const

std::vector< Interval > const &	getVector () const

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

std::map< VariableType, std::set< uint_fast64_t > > const &	getOccuringStatesAtVariable () const

bool	isCurrentRegionAllIllDefined () const

Detailed Description

template<typename ParametricType, typename ConstantType>
class storm::transformer::RobustParameterLifter< ParametricType, ConstantType >

This class lifts parameter choices to nondeterminism: For each row in the given matrix that considerd par parameters, the resulting matrix will have one row group consisting of 2^par rows.

When specifying a region, each row within the row group is evaluated w.r.t. one vertex of the region. The given vector is handled similarly. However, if a vector entry considers a parameter that does not occur in the corresponding matrix row, the parameter is directly set such that the vector entry is maximized (or minimized, depending on the specified optimization direction).

Note: The row grouping of the original matrix is ignored.

Definition at line 41 of file RobustParameterLifter.h.

Member Typedef Documentation

◆ CoefficientType

template<typename ParametricType , typename ConstantType >

typedef storm::utility::parametric::CoefficientType<ParametricType>::type storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::CoefficientType

Definition at line 44 of file RobustParameterLifter.h.

◆ Monotonicity

template<typename ParametricType , typename ConstantType >

typedef storm::analysis::MonotonicityResult<VariableType>::Monotonicity storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::Monotonicity

Definition at line 45 of file RobustParameterLifter.h.

◆ VariableType

template<typename ParametricType , typename ConstantType >

typedef storm::utility::parametric::VariableType<ParametricType>::type storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::VariableType

Definition at line 43 of file RobustParameterLifter.h.

Constructor & Destructor Documentation

◆ RobustParameterLifter()

template<typename ParametricType , typename ConstantType >

storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::RobustParameterLifter	(	storm::storage::SparseMatrix< ParametricType > const &	pMatrix,
		std::vector< ParametricType > const &	pVector,
		storm::storage::BitVector const &	selectedRows,
		storm::storage::BitVector const &	selectedColumns,
		bool	generateRowLabels = `false`,
		bool	useMonotonicity = `false`
	)

Lifts the parameter choices to nondeterminisim.

The computation is performed on the submatrix specified by the selected rows and columns

Parameters

pMatrix	the parametric matrix
pVector	the parametric vector (the vector size should equal the row count of the matrix)
selectedRows	a Bitvector that specifies which rows of the matrix and the vector are considered.
selectedColumns	a Bitvector that specifies which columns of the matrix are considered.

Definition at line 49 of file RobustParameterLifter.cpp.

Member Function Documentation

◆ getMatrix()

template<typename ParametricType , typename ConstantType >

storm::storage::SparseMatrix< Interval > const & storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::getMatrix ( ) const

Definition at line 391 of file RobustParameterLifter.cpp.

◆ getOccuringStatesAtVariable()

template<typename ParametricType , typename ConstantType >

std::map< typename RobustParameterLifter< ParametricType, ConstantType >::VariableType, std::set< uint_fast64_t > > const & storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::getOccuringStatesAtVariable ( ) const

Definition at line 195 of file RobustParameterLifter.cpp.

◆ getOccurringVariablesAtState()

template<typename ParametricType , typename ConstantType >

const std::vector< std::set< typename RobustParameterLifter< ParametricType, ConstantType >::VariableType > > & storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::getOccurringVariablesAtState ( ) const

Definition at line 189 of file RobustParameterLifter.cpp.

◆ getVector()

template<typename ParametricType , typename ConstantType >

std::vector< Interval > const & storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::getVector ( ) const

Definition at line 396 of file RobustParameterLifter.cpp.

◆ isCurrentRegionAllIllDefined()

template<typename ParametricType , typename ConstantType >

bool storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::isCurrentRegionAllIllDefined ( ) const

Definition at line 401 of file RobustParameterLifter.cpp.

◆ specifyRegion() [1/3]

template<typename ParametricType , typename ConstantType >

void storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::specifyRegion	(	storm::storage::ParameterRegion< ParametricType > const &	region,
		storm::solver::OptimizationDirection const &	dirForParameters
	)

Definition at line 170 of file RobustParameterLifter.cpp.

◆ specifyRegion() [2/3]

template<typename ParametricType , typename ConstantType >

void storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::specifyRegion	(	storm::storage::ParameterRegion< ParametricType > const &	region,
		storm::solver::OptimizationDirection const &	dirForParameters,
		std::shared_ptr< storm::analysis::Order >	reachabilityOrder,
		std::shared_ptr< storm::analysis::LocalMonotonicityResult< VariableType > >	localMonotonicityResult
	)

Specifies the region for the parameterlifter, the reachability order is used to see if there is local monotonicity, such that a fixed (partial) scheduler can be used.

Parameters

region	the region
dirForParameters	the optimization direction
reachabilityOrder	a (possibly insufficient) reachability order, used for local monotonicity

◆ specifyRegion() [3/3]

template<typename ParametricType , typename ConstantType >

void storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::specifyRegion	(	storm::storage::ParameterRegion< ParametricType > const &	region,
		storm::solver::OptimizationDirection const &	dirForParameters,
		storm::storage::BitVector const &	selectedRows
	)

Specifies the region for the parameterlifter, the Bitvector works as a fixed (partial) scheduler, this might not give sound results!

Parameters

region	the region
dirForParameters	the optimization direction
selectedRows	a Bitvector that specifies which rows of the matrix and the vector are considered.

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

src/storm-pars/transformer/RobustParameterLifter.h
src/storm-pars/transformer/RobustParameterLifter.cpp

Classes

Public Types

Public Member Functions

Detailed Description

Member Typedef Documentation

◆ CoefficientType

◆ Monotonicity

◆ VariableType

Constructor & Destructor Documentation

◆ RobustParameterLifter()

Member Function Documentation

◆ getMatrix()

◆ getOccuringStatesAtVariable()

◆ getOccurringVariablesAtState()

◆ getVector()

◆ isCurrentRegionAllIllDefined()

◆ specifyRegion() [1/3]

◆ specifyRegion() [2/3]

◆ specifyRegion() [3/3]