storm::transformer::RobustParameterLifter< ParametricType, ConstantType > Class Template Reference

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)
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 40 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 43 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 44 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 42 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 34 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 376 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 180 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 174 of file RobustParameterLifter.cpp.

getVector()

template<typename ParametricType , typename ConstantType >

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

(

)

const

Definition at line 381 of file RobustParameterLifter.cpp.

isCurrentRegionAllIllDefined()

template<typename ParametricType , typename ConstantType >

bool storm::transformer::RobustParameterLifter< ParametricType, ConstantType >::isCurrentRegionAllIllDefined

(

)

const

Definition at line 386 of file RobustParameterLifter.cpp.

specifyRegion()

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 155 of file RobustParameterLifter.cpp.

---

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

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