#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

ExplicitQualitativeCheckResult &	asExplicitQualitativeCheckResult ()

ExplicitQualitativeCheckResult 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 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()