#include <SymbolicQualitativeCheckResult.h>

Inheritance diagram for storm::modelchecker::SymbolicQualitativeCheckResult< Type >:

[legend]

Collaboration diagram for storm::modelchecker::SymbolicQualitativeCheckResult< Type >:

[legend]

Public Member Functions
	SymbolicQualitativeCheckResult ()=default
	SymbolicQualitativeCheckResult (storm::dd::Bdd< Type > const &reachableStates, storm::dd::Bdd< Type > const &truthValues)
	SymbolicQualitativeCheckResult (storm::dd::Bdd< Type > const &reachableStates, storm::dd::Bdd< Type > const &states, storm::dd::Bdd< Type > const &truthValues)
	SymbolicQualitativeCheckResult (SymbolicQualitativeCheckResult const &other)=default
SymbolicQualitativeCheckResult &	operator= (SymbolicQualitativeCheckResult const &other)=default
	SymbolicQualitativeCheckResult (SymbolicQualitativeCheckResult &&other)=default
SymbolicQualitativeCheckResult &	operator= (SymbolicQualitativeCheckResult &&other)=default
virtual std::unique_ptr< CheckResult >	clone () const override
virtual bool	isSymbolic () const override
virtual bool	isResultForAllStates () const override
virtual bool	isSymbolicQualitativeCheckResult () const override
virtual QualitativeCheckResult &	operator&= (QualitativeCheckResult const &other) override
virtual QualitativeCheckResult &	operator\|= (QualitativeCheckResult const &other) override
virtual void	complement () override
virtual bool	existsTrue () const override
virtual bool	forallTrue () const override
virtual uint64_t	count () const override
storm::dd::Bdd< Type > const &	getTruthValuesVector () const
storm::dd::Bdd< Type > const &	getStates () const
storm::dd::Bdd< Type > const &	getReachableStates () const
virtual std::ostream &	writeToStream (std::ostream &out) const override
virtual void	filter (QualitativeCheckResult const &filter) override
	Filters the current result wrt.
Public Member Functions inherited from storm::modelchecker::QualitativeCheckResult
virtual	~QualitativeCheckResult ()=default
virtual bool	isQualitative () const override
Public Member Functions inherited from storm::modelchecker::CheckResult
virtual	~CheckResult ()=default
virtual bool	isExplicit () const
virtual bool	isHybrid () const
virtual bool	isQuantitative () const
virtual bool	isParetoCurveCheckResult () const
virtual bool	isLexicographicCheckResult () const
virtual bool	isExplicitQualitativeCheckResult () const
virtual bool	isExplicitQuantitativeCheckResult () const
virtual bool	isExplicitParetoCurveCheckResult () const
virtual bool	isSymbolicQuantitativeCheckResult () const
virtual bool	isSymbolicParetoCurveCheckResult () const
virtual bool	isHybridQuantitativeCheckResult () const
QualitativeCheckResult &	asQualitativeCheckResult ()
QualitativeCheckResult const &	asQualitativeCheckResult () const
template<typename ValueType>
QuantitativeCheckResult< ValueType > &	asQuantitativeCheckResult ()
template<typename ValueType>
QuantitativeCheckResult< ValueType > const &	asQuantitativeCheckResult () const
template<typename ValueType>
ExplicitQualitativeCheckResult< ValueType > &	asExplicitQualitativeCheckResult ()
template<typename ValueType>
ExplicitQualitativeCheckResult< ValueType > const &	asExplicitQualitativeCheckResult () const
template<typename ValueType>
ExplicitQuantitativeCheckResult< ValueType > &	asExplicitQuantitativeCheckResult ()
template<typename ValueType>
ExplicitQuantitativeCheckResult< ValueType > const &	asExplicitQuantitativeCheckResult () const
template<typename ValueType>
ExplicitParetoCurveCheckResult< ValueType > &	asExplicitParetoCurveCheckResult ()
template<typename ValueType>
ExplicitParetoCurveCheckResult< ValueType > const &	asExplicitParetoCurveCheckResult () const
template<typename ValueType>
LexicographicCheckResult< ValueType > &	asLexicographicCheckResult ()
template<typename ValueType>
LexicographicCheckResult< ValueType > const &	asLexicographicCheckResult () const
template<storm::dd::DdType Type>
SymbolicQualitativeCheckResult< Type > &	asSymbolicQualitativeCheckResult ()
template<storm::dd::DdType Type>
SymbolicQualitativeCheckResult< Type > const &	asSymbolicQualitativeCheckResult () const
template<storm::dd::DdType Type, typename ValueType>
SymbolicQuantitativeCheckResult< Type, ValueType > &	asSymbolicQuantitativeCheckResult ()
template<storm::dd::DdType Type, typename ValueType>
SymbolicQuantitativeCheckResult< Type, ValueType > const &	asSymbolicQuantitativeCheckResult () const
template<storm::dd::DdType Type, typename ValueType>
HybridQuantitativeCheckResult< Type, ValueType > &	asHybridQuantitativeCheckResult ()
template<storm::dd::DdType Type, typename ValueType>
HybridQuantitativeCheckResult< Type, ValueType > const &	asHybridQuantitativeCheckResult () const
template<storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult< Type, ValueType > &	asSymbolicParetoCurveCheckResult ()
template<storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult< Type, ValueType > const &	asSymbolicParetoCurveCheckResult () const
virtual bool	hasScheduler () const
template<typename T>
bool	hasValueType () const
	Checks whether the ValueType of the result matches the given type.
template<typename ValueType>
ExplicitQualitativeCheckResult< ValueType > const &	asExplicitQualitativeCheckResult () const
template<typename ValueType>
ExplicitQuantitativeCheckResult< ValueType > const &	asExplicitQuantitativeCheckResult () const
template<typename ValueType>
ExplicitParetoCurveCheckResult< ValueType > const &	asExplicitParetoCurveCheckResult () const
template<typename ValueType>
LexicographicCheckResult< ValueType > const &	asLexicographicCheckResult () const
template<typename ValueType>
QuantitativeCheckResult< ValueType > const &	asQuantitativeCheckResult () const
template<storm::dd::DdType Type>
SymbolicQualitativeCheckResult< Type > const &	asSymbolicQualitativeCheckResult () const
template<storm::dd::DdType Type, typename ValueType>
SymbolicQuantitativeCheckResult< Type, ValueType > const &	asSymbolicQuantitativeCheckResult () const
template<storm::dd::DdType Type, typename ValueType>
HybridQuantitativeCheckResult< Type, ValueType > const &	asHybridQuantitativeCheckResult () const
template<storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult< Type, ValueType > const &	asSymbolicParetoCurveCheckResult () const

Detailed Description

template<storm::dd::DdType Type>
class storm::modelchecker::SymbolicQualitativeCheckResult< Type >

Definition at line 11 of file SymbolicQualitativeCheckResult.h.

Constructor & Destructor Documentation

◆ SymbolicQualitativeCheckResult() [1/5]

template<storm::dd::DdType Type>

storm::modelchecker::SymbolicQualitativeCheckResult< Type >::SymbolicQualitativeCheckResult ( )

default

◆ SymbolicQualitativeCheckResult() [2/5]

template<storm::dd::DdType Type>

storm::modelchecker::SymbolicQualitativeCheckResult< Type >::SymbolicQualitativeCheckResult	(	storm::dd::Bdd< Type > const &	reachableStates,
		storm::dd::Bdd< Type > const &	truthValues )

Definition at line 13 of file SymbolicQualitativeCheckResult.cpp.

◆ SymbolicQualitativeCheckResult() [3/5]

template<storm::dd::DdType Type>

storm::modelchecker::SymbolicQualitativeCheckResult< Type >::SymbolicQualitativeCheckResult	(	storm::dd::Bdd< Type > const &	reachableStates,
		storm::dd::Bdd< Type > const &	states,
		storm::dd::Bdd< Type > const &	truthValues )

Definition at line 19 of file SymbolicQualitativeCheckResult.cpp.

◆ SymbolicQualitativeCheckResult() [4/5]

template<storm::dd::DdType Type>

storm::modelchecker::SymbolicQualitativeCheckResult< Type >::SymbolicQualitativeCheckResult ( SymbolicQualitativeCheckResult< Type > const & other )

default

◆ SymbolicQualitativeCheckResult() [5/5]

template<storm::dd::DdType Type>

storm::modelchecker::SymbolicQualitativeCheckResult< Type >::SymbolicQualitativeCheckResult ( SymbolicQualitativeCheckResult< Type > && other )

default

Member Function Documentation

◆ clone()

template<storm::dd::DdType Type>

std::unique_ptr< CheckResult > storm::modelchecker::SymbolicQualitativeCheckResult< Type >::clone ( ) const

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 26 of file SymbolicQualitativeCheckResult.cpp.

◆ complement()

template<storm::dd::DdType Type>

void storm::modelchecker::SymbolicQualitativeCheckResult< Type >::complement ( )

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 62 of file SymbolicQualitativeCheckResult.cpp.

◆ count()

template<storm::dd::DdType Type>

uint64_t storm::modelchecker::SymbolicQualitativeCheckResult< Type >::count ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 92 of file SymbolicQualitativeCheckResult.cpp.

◆ existsTrue()

template<storm::dd::DdType Type>

bool storm::modelchecker::SymbolicQualitativeCheckResult< Type >::existsTrue ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 82 of file SymbolicQualitativeCheckResult.cpp.

◆ filter()

template<storm::dd::DdType Type>

void storm::modelchecker::SymbolicQualitativeCheckResult< Type >::filter ( QualitativeCheckResult const & filter )

overridevirtual

Filters the current result wrt.

to the filter, i.e. only keeps the entries that are selected by the filter. This means that the filter must be a qualitative result of proper type (symbolic/explicit).

Parameters

filter A qualitative result that serves as a filter.

Implements storm::modelchecker::CheckResult.

Definition at line 117 of file SymbolicQualitativeCheckResult.cpp.

◆ forallTrue()

template<storm::dd::DdType Type>

bool storm::modelchecker::SymbolicQualitativeCheckResult< Type >::forallTrue ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 87 of file SymbolicQualitativeCheckResult.cpp.

◆ getReachableStates()

template<storm::dd::DdType Type>

storm::dd::Bdd< Type > const & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::getReachableStates ( ) const

Definition at line 77 of file SymbolicQualitativeCheckResult.cpp.

◆ getStates()

template<storm::dd::DdType Type>

storm::dd::Bdd< Type > const & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::getStates ( ) const

Definition at line 72 of file SymbolicQualitativeCheckResult.cpp.

◆ getTruthValuesVector()

template<storm::dd::DdType Type>

storm::dd::Bdd< Type > const & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::getTruthValuesVector ( ) const

Definition at line 67 of file SymbolicQualitativeCheckResult.cpp.

◆ isResultForAllStates()

template<storm::dd::DdType Type>

bool storm::modelchecker::SymbolicQualitativeCheckResult< Type >::isResultForAllStates ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 36 of file SymbolicQualitativeCheckResult.cpp.

◆ isSymbolic()

template<storm::dd::DdType Type>

bool storm::modelchecker::SymbolicQualitativeCheckResult< Type >::isSymbolic ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 31 of file SymbolicQualitativeCheckResult.cpp.

◆ isSymbolicQualitativeCheckResult()

template<storm::dd::DdType Type>

bool storm::modelchecker::SymbolicQualitativeCheckResult< Type >::isSymbolicQualitativeCheckResult ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 41 of file SymbolicQualitativeCheckResult.cpp.

◆ operator&=()

template<storm::dd::DdType Type>

QualitativeCheckResult & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::operator&= ( QualitativeCheckResult const & other )

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 46 of file SymbolicQualitativeCheckResult.cpp.

◆ operator=() [1/2]

template<storm::dd::DdType Type>

SymbolicQualitativeCheckResult & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::operator= ( SymbolicQualitativeCheckResult< Type > && other )

default

◆ operator=() [2/2]

template<storm::dd::DdType Type>

SymbolicQualitativeCheckResult & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::operator= ( SymbolicQualitativeCheckResult< Type > const & other )

default

◆ operator|=()

template<storm::dd::DdType Type>

QualitativeCheckResult & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::operator|= ( QualitativeCheckResult const & other )

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 54 of file SymbolicQualitativeCheckResult.cpp.

◆ writeToStream()

template<storm::dd::DdType Type>

std::ostream & storm::modelchecker::SymbolicQualitativeCheckResult< Type >::writeToStream ( std::ostream & out ) const

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 97 of file SymbolicQualitativeCheckResult.cpp.

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

src/storm/modelchecker/results/CheckResult.h
src/storm/modelchecker/results/SymbolicQualitativeCheckResult.h
src/storm/modelchecker/results/SymbolicQualitativeCheckResult.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ SymbolicQualitativeCheckResult() [1/5]

◆ SymbolicQualitativeCheckResult() [2/5]

◆ SymbolicQualitativeCheckResult() [3/5]

◆ SymbolicQualitativeCheckResult() [4/5]

◆ SymbolicQualitativeCheckResult() [5/5]

Member Function Documentation

◆ clone()

◆ complement()

◆ count()

◆ existsTrue()

◆ filter()

◆ forallTrue()

◆ getReachableStates()

◆ getStates()

◆ getTruthValuesVector()

◆ isResultForAllStates()

◆ isSymbolic()

◆ isSymbolicQualitativeCheckResult()

◆ operator&=()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator|=()

◆ writeToStream()