#include <SymbolicQuantitativeCheckResult.h>

Inheritance diagram for storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >:

[legend]

Collaboration diagram for storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >:

[legend]

Public Member Functions
	SymbolicQuantitativeCheckResult ()=default

	SymbolicQuantitativeCheckResult (storm::dd::Bdd< Type > const &reachableStates, storm::dd::Add< Type, ValueType > const &values)

	SymbolicQuantitativeCheckResult (storm::dd::Bdd< Type > const &reachableStates, storm::dd::Bdd< Type > const &states, storm::dd::Add< Type, ValueType > const &values)

	SymbolicQuantitativeCheckResult (SymbolicQuantitativeCheckResult const &other)=default

SymbolicQuantitativeCheckResult &	operator= (SymbolicQuantitativeCheckResult const &other)=default

	SymbolicQuantitativeCheckResult (SymbolicQuantitativeCheckResult &&other)=default

SymbolicQuantitativeCheckResult &	operator= (SymbolicQuantitativeCheckResult &&other)=default

	SymbolicQuantitativeCheckResult (SymbolicQualitativeCheckResult< Type > const &other)

virtual std::unique_ptr< CheckResult >	clone () const override

virtual std::unique_ptr< CheckResult >	compareAgainstBound (storm::logic::ComparisonType comparisonType, ValueType const &bound) const override

virtual bool	isSymbolic () const override

virtual bool	isResultForAllStates () const override

virtual bool	isSymbolicQuantitativeCheckResult () const override

storm::dd::Add< Type, ValueType > const &	getValueVector () 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.

virtual ValueType	getMin () const override

virtual ValueType	getMax () const override

virtual ValueType	average () const override

virtual ValueType	sum () const override

virtual void	oneMinus () override

Public Member Functions inherited from storm::modelchecker::QuantitativeCheckResult< ValueType >
virtual	~QuantitativeCheckResult ()=default

virtual bool	isQuantitative () const override

Public Member Functions inherited from storm::modelchecker::CheckResult
virtual	~CheckResult ()=default

virtual bool	isExplicit () const

virtual bool	isHybrid () const

virtual bool	isQualitative () const

virtual bool	isParetoCurveCheckResult () const

virtual bool	isLexicographicCheckResult () const

virtual bool	isExplicitQualitativeCheckResult () const

virtual bool	isExplicitQuantitativeCheckResult () const

virtual bool	isExplicitParetoCurveCheckResult () const

virtual bool	isSymbolicQualitativeCheckResult () 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, typename ValueType = double>
class storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >

Definition at line 15 of file SymbolicQuantitativeCheckResult.h.

Constructor & Destructor Documentation

◆ SymbolicQuantitativeCheckResult() [1/6]

template<storm::dd::DdType Type, typename ValueType = double>

storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::SymbolicQuantitativeCheckResult ( )

default

◆ SymbolicQuantitativeCheckResult() [2/6]

template<storm::dd::DdType Type, typename ValueType >

storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::SymbolicQuantitativeCheckResult	(	storm::dd::Bdd< Type > const &	reachableStates,
		storm::dd::Add< Type, ValueType > const &	values
	)

Definition at line 18 of file SymbolicQuantitativeCheckResult.cpp.

◆ SymbolicQuantitativeCheckResult() [3/6]

template<storm::dd::DdType Type, typename ValueType >

storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::SymbolicQuantitativeCheckResult	(	storm::dd::Bdd< Type > const &	reachableStates,
		storm::dd::Bdd< Type > const &	states,
		storm::dd::Add< Type, ValueType > const &	values
	)

Definition at line 25 of file SymbolicQuantitativeCheckResult.cpp.

◆ SymbolicQuantitativeCheckResult() [4/6]

template<storm::dd::DdType Type, typename ValueType = double>

storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::SymbolicQuantitativeCheckResult ( SymbolicQuantitativeCheckResult< Type, ValueType > const & other )

default

◆ SymbolicQuantitativeCheckResult() [5/6]

template<storm::dd::DdType Type, typename ValueType = double>

storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::SymbolicQuantitativeCheckResult ( SymbolicQuantitativeCheckResult< Type, ValueType > && other )

default

◆ SymbolicQuantitativeCheckResult() [6/6]

template<storm::dd::DdType Type, typename ValueType >

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

Definition at line 33 of file SymbolicQuantitativeCheckResult.cpp.

Member Function Documentation

◆ average()

template<storm::dd::DdType Type, typename ValueType >

ValueType storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::average ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 192 of file SymbolicQuantitativeCheckResult.cpp.

◆ clone()

template<storm::dd::DdType Type, typename ValueType >

std::unique_ptr< CheckResult > storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::clone ( ) const

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 39 of file SymbolicQuantitativeCheckResult.cpp.

◆ compareAgainstBound()

template<storm::dd::DdType Type, typename ValueType >

std::unique_ptr< CheckResult > storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::compareAgainstBound	(	storm::logic::ComparisonType	comparisonType,
		ValueType const &	bound
	)		const

overridevirtual

Reimplemented from storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 44 of file SymbolicQuantitativeCheckResult.cpp.

◆ filter()

template<storm::dd::DdType Type, typename ValueType >

void storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::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 172 of file SymbolicQuantitativeCheckResult.cpp.

◆ getMax()

template<storm::dd::DdType Type, typename ValueType >

ValueType storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::getMax ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 187 of file SymbolicQuantitativeCheckResult.cpp.

◆ getMin()

template<storm::dd::DdType Type, typename ValueType >

ValueType storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::getMin ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 180 of file SymbolicQuantitativeCheckResult.cpp.

◆ getReachableStates()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Bdd< Type > const & storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::getReachableStates ( ) const

Definition at line 85 of file SymbolicQuantitativeCheckResult.cpp.

◆ getStates()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Bdd< Type > const & storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::getStates ( ) const

Definition at line 80 of file SymbolicQuantitativeCheckResult.cpp.

◆ getValueVector()

template<storm::dd::DdType Type, typename ValueType >

storm::dd::Add< Type, ValueType > const & storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::getValueVector ( ) const

Definition at line 75 of file SymbolicQuantitativeCheckResult.cpp.

◆ isResultForAllStates()

template<storm::dd::DdType Type, typename ValueType >

bool storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::isResultForAllStates ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 65 of file SymbolicQuantitativeCheckResult.cpp.

◆ isSymbolic()

template<storm::dd::DdType Type, typename ValueType >

bool storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::isSymbolic ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 60 of file SymbolicQuantitativeCheckResult.cpp.

◆ isSymbolicQuantitativeCheckResult()

template<storm::dd::DdType Type, typename ValueType >

bool storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::isSymbolicQuantitativeCheckResult ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 70 of file SymbolicQuantitativeCheckResult.cpp.

◆ oneMinus()

template<storm::dd::DdType Type, typename ValueType >

void storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::oneMinus ( )

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 202 of file SymbolicQuantitativeCheckResult.cpp.

◆ operator=() [1/2]

template<storm::dd::DdType Type, typename ValueType = double>

SymbolicQuantitativeCheckResult & storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::operator= ( SymbolicQuantitativeCheckResult< Type, ValueType > && other )

default

◆ operator=() [2/2]

template<storm::dd::DdType Type, typename ValueType = double>

SymbolicQuantitativeCheckResult & storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::operator= ( SymbolicQuantitativeCheckResult< Type, ValueType > const & other )

default

◆ sum()

template<storm::dd::DdType Type, typename ValueType >

ValueType storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::sum ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 197 of file SymbolicQuantitativeCheckResult.cpp.

◆ writeToStream()

template<storm::dd::DdType Type, typename ValueType >

std::ostream & storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >::writeToStream ( std::ostream & out ) const

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 135 of file SymbolicQuantitativeCheckResult.cpp.

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

src/storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h
src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.h
src/storm/modelchecker/results/SymbolicQuantitativeCheckResult.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ SymbolicQuantitativeCheckResult() [1/6]

◆ SymbolicQuantitativeCheckResult() [2/6]

◆ SymbolicQuantitativeCheckResult() [3/6]

◆ SymbolicQuantitativeCheckResult() [4/6]

◆ SymbolicQuantitativeCheckResult() [5/6]

◆ SymbolicQuantitativeCheckResult() [6/6]

Member Function Documentation

◆ average()

◆ clone()

◆ compareAgainstBound()

◆ filter()

◆ getMax()

◆ getMin()

◆ getReachableStates()

◆ getStates()

◆ getValueVector()

◆ isResultForAllStates()

◆ isSymbolic()

◆ isSymbolicQuantitativeCheckResult()

◆ oneMinus()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ sum()

◆ writeToStream()