Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | Friends | List of all members
storm::dd::DdMetaVariable< LibraryType > Class Template Reference

#include <DdMetaVariable.h>

Public Member Functions

std::string const & getName () const
 Retrieves the name of the meta variable.
 
MetaVariableType getType () const
 Retrieves the type of the meta variable.
 
int_fast64_t getLow () const
 Retrieves the lowest value of the range of the variable.
 
bool hasHigh () const
 Retrieves whether the variable has an upper bound.
 
int_fast64_t getHigh () const
 Retrieves the highest value of the range of the variable.
 
bool canRepresent (int_fast64_t value) const
 Retrieves whether the meta variable can represent the given value.
 
std::size_t getNumberOfDdVariables () const
 Retrieves the number of DD variables for this meta variable.
 
Bdd< LibraryType > const & getCube () const
 Retrieves the cube of all variables that encode this meta variable.
 
uint64_t getLowestIndex () const
 Retrieves the highest index of all DD variables belonging to this meta variable.
 
uint64_t getHighestLevel () const
 Retrieves the highest level of all DD variables belonging to this meta variable.
 
std::vector< uint64_t > getIndices (bool sortedByLevel=true) const
 Retrieves the indices of the DD variables associated with this meta variable.
 
std::vector< std::pair< uint64_t, uint64_t > > getIndicesAndLevels () const
 Retrieves the indices and levels of the DD variables associated with this meta variable.
 

Friends

class DdManager< LibraryType >
 
class Bdd< LibraryType >
 
template<DdType LibraryTypePrime, typename ValueTypePrime >
class Add
 
template<DdType LibraryTypePrime, typename ValueTypePrime >
class AddIterator
 

Detailed Description

template<DdType LibraryType>
class storm::dd::DdMetaVariable< LibraryType >

Definition at line 23 of file DdMetaVariable.h.

Member Function Documentation

◆ canRepresent()

template<DdType LibraryType>
bool storm::dd::DdMetaVariable< LibraryType >::canRepresent ( int_fast64_t  value) const

Retrieves whether the meta variable can represent the given value.

Parameters
valueThe value to check for legality.
Returns
True iff the value is legal.

Definition at line 57 of file DdMetaVariable.cpp.

◆ getCube()

template<DdType LibraryType>
Bdd< LibraryType > const & storm::dd::DdMetaVariable< LibraryType >::getCube ( ) const

Retrieves the cube of all variables that encode this meta variable.

Returns
The cube of all variables that encode this meta variable.

Definition at line 76 of file DdMetaVariable.cpp.

◆ getHigh()

template<DdType LibraryType>
int_fast64_t storm::dd::DdMetaVariable< LibraryType >::getHigh ( ) const

Retrieves the highest value of the range of the variable.

Returns
The highest value of the range of the variable.

Definition at line 47 of file DdMetaVariable.cpp.

◆ getHighestLevel()

template<DdType LibraryType>
uint64_t storm::dd::DdMetaVariable< LibraryType >::getHighestLevel ( ) const

Retrieves the highest level of all DD variables belonging to this meta variable.

Definition at line 107 of file DdMetaVariable.cpp.

◆ getIndices()

template<DdType LibraryType>
std::vector< uint64_t > storm::dd::DdMetaVariable< LibraryType >::getIndices ( bool  sortedByLevel = true) const

Retrieves the indices of the DD variables associated with this meta variable.

Parameters
sortedByLevelIf true, the indices are sorted by their level.

Definition at line 81 of file DdMetaVariable.cpp.

◆ getIndicesAndLevels()

template<DdType LibraryType>
std::vector< std::pair< uint64_t, uint64_t > > storm::dd::DdMetaVariable< LibraryType >::getIndicesAndLevels ( ) const

Retrieves the indices and levels of the DD variables associated with this meta variable.

Definition at line 97 of file DdMetaVariable.cpp.

◆ getLow()

template<DdType LibraryType>
int_fast64_t storm::dd::DdMetaVariable< LibraryType >::getLow ( ) const

Retrieves the lowest value of the range of the variable.

Returns
The lowest value of the range of the variable.

Definition at line 42 of file DdMetaVariable.cpp.

◆ getLowestIndex()

template<DdType LibraryType>
uint64_t storm::dd::DdMetaVariable< LibraryType >::getLowestIndex ( ) const

Retrieves the highest index of all DD variables belonging to this meta variable.

Definition at line 122 of file DdMetaVariable.cpp.

◆ getName()

template<DdType LibraryType>
std::string const & storm::dd::DdMetaVariable< LibraryType >::getName ( ) const

Retrieves the name of the meta variable.

Returns
The name of the variable.

Definition at line 32 of file DdMetaVariable.cpp.

◆ getNumberOfDdVariables()

template<DdType LibraryType>
std::size_t storm::dd::DdMetaVariable< LibraryType >::getNumberOfDdVariables ( ) const

Retrieves the number of DD variables for this meta variable.

Returns
The number of DD variables for this meta variable.

Definition at line 66 of file DdMetaVariable.cpp.

◆ getType()

template<DdType LibraryType>
MetaVariableType storm::dd::DdMetaVariable< LibraryType >::getType ( ) const

Retrieves the type of the meta variable.

Returns
The type of the meta variable.

Definition at line 37 of file DdMetaVariable.cpp.

◆ hasHigh()

template<DdType LibraryType>
bool storm::dd::DdMetaVariable< LibraryType >::hasHigh ( ) const

Retrieves whether the variable has an upper bound.

Returns
True iff the variable has an upper bound.

Definition at line 52 of file DdMetaVariable.cpp.

Friends And Related Symbol Documentation

◆ Add

template<DdType LibraryType>
template<DdType LibraryTypePrime, typename ValueTypePrime >
friend class Add
friend

Definition at line 29 of file DdMetaVariable.h.

◆ AddIterator

template<DdType LibraryType>
template<DdType LibraryTypePrime, typename ValueTypePrime >
friend class AddIterator
friend

Definition at line 32 of file DdMetaVariable.h.

◆ Bdd< LibraryType >

template<DdType LibraryType>
friend class Bdd< LibraryType >
friend

Definition at line 1 of file DdMetaVariable.h.

◆ DdManager< LibraryType >

template<DdType LibraryType>
friend class DdManager< LibraryType >
friend

Definition at line 1 of file DdMetaVariable.h.

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