Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Types | Public Member Functions | List of all members
storm::transformer::Product< Model > Class Template Reference

#include <Product.h>

Inheritance diagram for storm::transformer::Product< Model >:
Inheritance graph
[legend]

Public Types

typedef std::shared_ptr< Product< Model > > ptr
 
typedef storm::storage::sparse::state_type state_type
 
typedef std::pair< state_type, state_type > product_state_type
 
typedef std::map< product_state_type, state_type > product_state_to_product_index_map
 
typedef std::vector< product_state_type > product_index_to_product_state_vector
 

Public Member Functions

 Product (Model &&productModel, std::string &&productStateOfInterestLabel, product_state_to_product_index_map &&productStateToProductIndex, product_index_to_product_state_vector &&productIndexToProductState)
 
 Product (Product< Model > &&product)=default
 
Product & operator= (Product< Model > &&product)=default
 
Model & getProductModel ()
 
state_type getModelState (state_type productStateIndex) const
 
state_type getAutomatonState (state_type productStateIndex) const
 
state_type getProductStateIndex (state_type modelState, state_type automatonState) const
 
bool isValidProductState (state_type modelState, state_type automatonState) const
 
storm::storage::BitVector liftFromAutomaton (const storm::storage::BitVector &vector) const
 
storm::storage::BitVector liftFromModel (const storm::storage::BitVector &vector) const
 
template<typename ValueType >
std::vector< ValueType > projectToOriginalModel (const Model &originalModel, const std::vector< ValueType > &prodValues)
 
template<typename ValueType >
std::vector< ValueType > projectToOriginalModel (std::size_t numberOfStates, const std::vector< ValueType > &prodValues)
 
const storm::storage::BitVector & getStatesOfInterest () const
 
void printMapping (std::ostream &out) const
 

Detailed Description

template<typename Model>
class storm::transformer::Product< Model >

Definition at line 8 of file Product.h.

Member Typedef Documentation

◆ product_index_to_product_state_vector

template<typename Model >
typedef std::vector<product_state_type> storm::transformer::Product< Model >::product_index_to_product_state_vector

Definition at line 15 of file Product.h.

◆ product_state_to_product_index_map

template<typename Model >
typedef std::map<product_state_type, state_type> storm::transformer::Product< Model >::product_state_to_product_index_map

Definition at line 14 of file Product.h.

◆ product_state_type

template<typename Model >
typedef std::pair<state_type, state_type> storm::transformer::Product< Model >::product_state_type

Definition at line 13 of file Product.h.

◆ ptr

template<typename Model >
typedef std::shared_ptr<Product<Model> > storm::transformer::Product< Model >::ptr

Definition at line 10 of file Product.h.

◆ state_type

template<typename Model >
typedef storm::storage::sparse::state_type storm::transformer::Product< Model >::state_type

Definition at line 12 of file Product.h.

Constructor & Destructor Documentation

◆ Product() [1/2]

template<typename Model >
storm::transformer::Product< Model >::Product ( Model &&  productModel,
std::string &&  productStateOfInterestLabel,
product_state_to_product_index_map &&  productStateToProductIndex,
product_index_to_product_state_vector &&  productIndexToProductState 
)
inline

Definition at line 17 of file Product.h.

◆ Product() [2/2]

template<typename Model >
storm::transformer::Product< Model >::Product ( Product< Model > &&  product)
default

Member Function Documentation

◆ getAutomatonState()

template<typename Model >
state_type storm::transformer::Product< Model >::getAutomatonState ( state_type  productStateIndex) const
inline

Definition at line 35 of file Product.h.

◆ getModelState()

template<typename Model >
state_type storm::transformer::Product< Model >::getModelState ( state_type  productStateIndex) const
inline

Definition at line 31 of file Product.h.

◆ getProductModel()

template<typename Model >
Model & storm::transformer::Product< Model >::getProductModel ( )
inline

Definition at line 27 of file Product.h.

◆ getProductStateIndex()

template<typename Model >
state_type storm::transformer::Product< Model >::getProductStateIndex ( state_type  modelState,
state_type  automatonState 
) const
inline

Definition at line 39 of file Product.h.

◆ getStatesOfInterest()

template<typename Model >
const storm::storage::BitVector & storm::transformer::Product< Model >::getStatesOfInterest ( ) const
inline

Definition at line 84 of file Product.h.

◆ isValidProductState()

template<typename Model >
bool storm::transformer::Product< Model >::isValidProductState ( state_type  modelState,
state_type  automatonState 
) const
inline

Definition at line 43 of file Product.h.

◆ liftFromAutomaton()

template<typename Model >
storm::storage::BitVector storm::transformer::Product< Model >::liftFromAutomaton ( const storm::storage::BitVector &  vector) const
inline

Definition at line 47 of file Product.h.

◆ liftFromModel()

template<typename Model >
storm::storage::BitVector storm::transformer::Product< Model >::liftFromModel ( const storm::storage::BitVector &  vector) const
inline

Definition at line 58 of file Product.h.

◆ operator=()

template<typename Model >
Product & storm::transformer::Product< Model >::operator= ( Product< Model > &&  product)
default

◆ printMapping()

template<typename Model >
void storm::transformer::Product< Model >::printMapping ( std::ostream &  out) const
inline

Definition at line 88 of file Product.h.

◆ projectToOriginalModel() [1/2]

template<typename Model >
template<typename ValueType >
std::vector< ValueType > storm::transformer::Product< Model >::projectToOriginalModel ( const Model &  originalModel,
const std::vector< ValueType > &  prodValues 
)
inline

Definition at line 70 of file Product.h.

◆ projectToOriginalModel() [2/2]

template<typename Model >
template<typename ValueType >
std::vector< ValueType > storm::transformer::Product< Model >::projectToOriginalModel ( std::size_t  numberOfStates,
const std::vector< ValueType > &  prodValues 
)
inline

Definition at line 75 of file Product.h.

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