storm::dft::utility::RelevantEvents Class Reference

#include <RelevantEvents.h>

Public Member Functions
	RelevantEvents ()=default
	Constructs empty RelevantEvents object.
	RelevantEvents (std::initializer_list< std::string > init)
	Create relevant events from given event names in an initializer list.
template<typename ForwardIt >
	RelevantEvents (ForwardIt first, ForwardIt last)
	Create relevant events from given event names in a range.
bool	operator== (RelevantEvents const &rhs) const
bool	operator!= (RelevantEvents const &rhs) const
template<typename ValueType >
size_t	count (std::shared_ptr< storm::dft::storage::DFT< ValueType > > const dft) const
	Count the events that are relevant in the given DFT.
template<typename ForwardIt >
void	insertNamesFromProperties (ForwardIt first, ForwardIt last)
	Add relevant event names required by the labels in properties of a range.
void	insert (std::string const &name)
	Add relevant event.
template<typename ForwardIt >
void	insert (ForwardIt first, ForwardIt last)
	Add relevant event names from a range.
template<typename ValueType >
bool	checkRelevantNames (storm::dft::storage::DFT< ValueType > const &dft) const
	Check that the relevant names correspond to existing elements in the DFT.
bool	isRelevant (std::string const &name) const
RelevantEvents &	merge (RelevantEvents const &other)
	Merge the given RelevantEvents with *this.

Detailed Description

Definition at line 17 of file RelevantEvents.h.

Constructor & Destructor Documentation

RelevantEvents() [1/3]

storm::dft::utility::RelevantEvents::RelevantEvents ( )

default

Constructs empty RelevantEvents object.

RelevantEvents() [2/3]

storm::dft::utility::RelevantEvents::RelevantEvents ( std::initializer_list< std::string >  init )

inline

Create relevant events from given event names in an initializer list.

If name 'all' occurs, all elements are stored as relevant.

Allows syntactic sugar like: RelevantEvents e = {}; and RelevantEvents e{"a"};

Parameters

init	The initializer list.

Definition at line 35 of file RelevantEvents.h.

RelevantEvents() [3/3]

template<typename ForwardIt >

storm::dft::utility::RelevantEvents::RelevantEvents ( ForwardIt  first, ForwardIt  last  )

inline

Create relevant events from given event names in a range.

If name 'all' occurs, all elements are stored as relevant.

Parameters

first	Iterator pointing to the start of a range of names.
last	Iterator pointing to the end of a range of names.

Definition at line 47 of file RelevantEvents.h.

Member Function Documentation

checkRelevantNames()

template<typename ValueType >

bool storm::dft::utility::RelevantEvents::checkRelevantNames ( storm::dft::storage::DFT< ValueType > const &  dft ) const

inline

Check that the relevant names correspond to existing elements in the DFT.

Parameters

dft

DFT.

Returns

True iff the relevant names are consistent with the given DFT.

Definition at line 156 of file RelevantEvents.h.

count()

template<typename ValueType >

size_t storm::dft::utility::RelevantEvents::count ( std::shared_ptr< storm::dft::storage::DFT< ValueType > > const  dft ) const

inline

Count the events that are relevant in the given DFT.

Note

Can be very slow. Uses a naiive O(n^2) implementation.

Parameters

dft	The DFT to count on.

Definition at line 66 of file RelevantEvents.h.

insert() [1/2]

template<typename ForwardIt >

void storm::dft::utility::RelevantEvents::insert ( ForwardIt  first, ForwardIt  last  )

inline

Add relevant event names from a range.

If name 'all' occurs, all elements are stored as relevant.

Parameters

first	Iterator pointing to the start of a range of names.
last	Iterator pointing to the end of a range of names.

Definition at line 140 of file RelevantEvents.h.

insert() [2/2]

void storm::dft::utility::RelevantEvents::insert ( std::string const &  name )

inline

Add relevant event.

If name 'all' occurs, all elements are stored as relevant.

Parameters

name	Name of relevant event.

Definition at line 125 of file RelevantEvents.h.

insertNamesFromProperties()

template<typename ForwardIt >

void storm::dft::utility::RelevantEvents::insertNamesFromProperties ( ForwardIt  first, ForwardIt  last  )

inline

Add relevant event names required by the labels in properties of a range.

Parameters

first	Iterator pointing to the start of a std::shared_ptr<storm::logic::Formula const> range.
last	Iterator pointing to the end of a std::shared_ptr<storm::logic::Formula const> range.

Definition at line 86 of file RelevantEvents.h.

isRelevant()

bool storm::dft::utility::RelevantEvents::isRelevant ( std::string const &  name ) const

inline

Returns

True iff the given name is the name of a relevant Event

Definition at line 168 of file RelevantEvents.h.

merge()

RelevantEvents & storm::dft::utility::RelevantEvents::merge ( RelevantEvents const &  other )

inline

Merge the given RelevantEvents with *this.

Returns

A reference to *this, allowing chaining i.e. e.merge(a).merge(b)

Definition at line 181 of file RelevantEvents.h.

operator!=()

bool storm::dft::utility::RelevantEvents::operator!= ( RelevantEvents const &  rhs ) const

inline

Definition at line 55 of file RelevantEvents.h.

operator==()

bool storm::dft::utility::RelevantEvents::operator== ( RelevantEvents const &  rhs ) const

inline

Definition at line 51 of file RelevantEvents.h.

---

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

• src/storm-dft/utility/RelevantEvents.h