Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | List of all members
storm::transformer::ParameterLifter< 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 <ParameterLifter.h>

Classes

class  AbstractValuation
 

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

 ParameterLifter (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< ConstantType > const & getMatrix () const
 
std::vector< ConstantType > const & getVector () const
 
std::vector< std::set< VariableType > > const & getOccurringVariablesAtState () const
 
std::map< VariableType, std::set< uint_fast64_t > > getOccuringStatesAtVariable () const
 
uint_fast64_t getRowGroupIndex (uint_fast64_t originalState) const
 
uint_fast64_t getOriginalStateNumber (uint_fast64_t newState) const
 
uint_fast64_t getRowGroupSize (uint_fast64_t originalState) const
 
uint_fast64_t getRowGroupCount () const
 
std::vector< AbstractValuation > const & getRowLabels () const
 

Detailed Description

template<typename ParametricType, typename ConstantType>
class storm::transformer::ParameterLifter< 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 31 of file ParameterLifter.h.

Member Typedef Documentation

◆ CoefficientType

template<typename ParametricType , typename ConstantType >
typedef storm::utility::parametric::CoefficientType<ParametricType>::type storm::transformer::ParameterLifter< ParametricType, ConstantType >::CoefficientType

Definition at line 34 of file ParameterLifter.h.

◆ Monotonicity

template<typename ParametricType , typename ConstantType >
typedef storm::analysis::MonotonicityResult<VariableType>::Monotonicity storm::transformer::ParameterLifter< ParametricType, ConstantType >::Monotonicity

Definition at line 35 of file ParameterLifter.h.

◆ VariableType

template<typename ParametricType , typename ConstantType >
typedef storm::utility::parametric::VariableType<ParametricType>::type storm::transformer::ParameterLifter< ParametricType, ConstantType >::VariableType

Definition at line 33 of file ParameterLifter.h.

Constructor & Destructor Documentation

◆ ParameterLifter()

template<typename ParametricType , typename ConstantType >
storm::transformer::ParameterLifter< ParametricType, ConstantType >::ParameterLifter ( 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
pMatrixthe parametric matrix
pVectorthe parametric vector (the vector size should equal the row count of the matrix)
selectedRowsa Bitvector that specifies which rows of the matrix and the vector are considered.
selectedColumnsa Bitvector that specifies which columns of the matrix are considered.

Definition at line 12 of file ParameterLifter.cpp.

Member Function Documentation

◆ getMatrix()

template<typename ParametricType , typename ConstantType >
storm::storage::SparseMatrix< ConstantType > const & storm::transformer::ParameterLifter< ParametricType, ConstantType >::getMatrix ( ) const

Definition at line 197 of file ParameterLifter.cpp.

◆ getOccuringStatesAtVariable()

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

Definition at line 243 of file ParameterLifter.cpp.

◆ getOccurringVariablesAtState()

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

Definition at line 237 of file ParameterLifter.cpp.

◆ getOriginalStateNumber()

template<typename ParametricType , typename ConstantType >
uint_fast64_t storm::transformer::ParameterLifter< ParametricType, ConstantType >::getOriginalStateNumber ( uint_fast64_t  newState) const

Definition at line 183 of file ParameterLifter.cpp.

◆ getRowGroupCount()

template<typename ParametricType , typename ConstantType >
uint_fast64_t storm::transformer::ParameterLifter< ParametricType, ConstantType >::getRowGroupCount ( ) const

Definition at line 192 of file ParameterLifter.cpp.

◆ getRowGroupIndex()

template<typename ParametricType , typename ConstantType >
uint_fast64_t storm::transformer::ParameterLifter< ParametricType, ConstantType >::getRowGroupIndex ( uint_fast64_t  originalState) const

Definition at line 178 of file ParameterLifter.cpp.

◆ getRowGroupSize()

template<typename ParametricType , typename ConstantType >
uint_fast64_t storm::transformer::ParameterLifter< ParametricType, ConstantType >::getRowGroupSize ( uint_fast64_t  originalState) const

Definition at line 188 of file ParameterLifter.cpp.

◆ getRowLabels()

template<typename ParametricType , typename ConstantType >
std::vector< typename ParameterLifter< ParametricType, ConstantType >::AbstractValuation > const & storm::transformer::ParameterLifter< ParametricType, ConstantType >::getRowLabels ( ) const

Definition at line 207 of file ParameterLifter.cpp.

◆ getVector()

template<typename ParametricType , typename ConstantType >
std::vector< ConstantType > const & storm::transformer::ParameterLifter< ParametricType, ConstantType >::getVector ( ) const

Definition at line 202 of file ParameterLifter.cpp.

◆ specifyRegion() [1/3]

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

Definition at line 157 of file ParameterLifter.cpp.

◆ specifyRegion() [2/3]

template<typename ParametricType , typename ConstantType >
void storm::transformer::ParameterLifter< 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
regionthe region
dirForParametersthe optimization direction
reachabilityOrdera (possibly insufficient) reachability order, used for local monotonicity

◆ specifyRegion() [3/3]

template<typename ParametricType , typename ConstantType >
void storm::transformer::ParameterLifter< 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
regionthe region
dirForParametersthe optimization direction
selectedRowsa Bitvector that specifies which rows of the matrix and the vector are considered.
The documentation for this class was generated from the following files: