#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, bool addLabelsClaiming)
	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 15 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 33 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 45 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 154 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 64 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 138 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 123 of file RelevantEvents.h.

◆ insertNamesFromProperties()

template<typename ForwardIt>

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

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.
addLabelsClaiming	Whether labels representing claiming operations are added to the model.

Definition at line 85 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 166 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 179 of file RelevantEvents.h.

◆ operator!=()

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

inline

Definition at line 53 of file RelevantEvents.h.

◆ operator==()

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

inline

Definition at line 49 of file RelevantEvents.h.

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

src/storm-dft/utility/RelevantEvents.h

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ RelevantEvents() [1/3]

◆ RelevantEvents() [2/3]

◆ RelevantEvents() [3/3]

Member Function Documentation

◆ checkRelevantNames()

◆ count()

◆ insert() [1/2]

◆ insert() [2/2]

◆ insertNamesFromProperties()

◆ isRelevant()

◆ merge()

◆ operator!=()

◆ operator==()