#include <HybridQuantitativeCheckResult.h>

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

[legend]

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

[legend]

Public Member Functions
	HybridQuantitativeCheckResult ()=default

	HybridQuantitativeCheckResult (storm::dd::Bdd< Type > const &reachableStates, storm::dd::Bdd< Type > const &symbolicStates, storm::dd::Add< Type, ValueType > const &symbolicValues, storm::dd::Bdd< Type > const &explicitStates, storm::dd::Odd const &odd, std::vector< ValueType > const &explicitValues)

	HybridQuantitativeCheckResult (HybridQuantitativeCheckResult const &other)=default

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

	HybridQuantitativeCheckResult (HybridQuantitativeCheckResult &&other)=default

HybridQuantitativeCheckResult &	operator= (HybridQuantitativeCheckResult &&other)=default

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

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

std::unique_ptr< CheckResult >	toExplicitQuantitativeCheckResult () const

virtual bool	isHybrid () const override

virtual bool	isResultForAllStates () const override

virtual bool	isHybridQuantitativeCheckResult () const override

storm::dd::Bdd< Type > const &	getSymbolicStates () const

storm::dd::Add< Type, ValueType > const &	getSymbolicValueVector () const

storm::dd::Bdd< Type > const &	getExplicitStates () const

storm::dd::Odd const &	getOdd () const

std::vector< ValueType > const &	getExplicitValueVector () 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	sum () const override

virtual ValueType	average () 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	isSymbolic () 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	isSymbolicQuantitativeCheckResult () const

virtual bool	isSymbolicParetoCurveCheckResult () 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::HybridQuantitativeCheckResult< Type, ValueType >

Definition at line 14 of file HybridQuantitativeCheckResult.h.

Constructor & Destructor Documentation

◆ HybridQuantitativeCheckResult() [1/4]

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

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

default

◆ HybridQuantitativeCheckResult() [2/4]

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

storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::HybridQuantitativeCheckResult	(	storm::dd::Bdd< Type > const &	reachableStates,
		storm::dd::Bdd< Type > const &	symbolicStates,
		storm::dd::Add< Type, ValueType > const &	symbolicValues,
		storm::dd::Bdd< Type > const &	explicitStates,
		storm::dd::Odd const &	odd,
		std::vector< ValueType > const &	explicitValues
	)

Definition at line 18 of file HybridQuantitativeCheckResult.cpp.

◆ HybridQuantitativeCheckResult() [3/4]

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

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

default

◆ HybridQuantitativeCheckResult() [4/4]

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

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

default

Member Function Documentation

◆ average()

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

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

overridevirtual

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

Definition at line 270 of file HybridQuantitativeCheckResult.cpp.

◆ clone()

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

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

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 33 of file HybridQuantitativeCheckResult.cpp.

◆ compareAgainstBound()

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

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

overridevirtual

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

Definition at line 39 of file HybridQuantitativeCheckResult.cpp.

◆ filter()

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

void storm::modelchecker::HybridQuantitativeCheckResult< 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 214 of file HybridQuantitativeCheckResult.cpp.

◆ getExplicitStates()

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

storm::dd::Bdd< Type > const & storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::getExplicitStates ( ) const

Definition at line 98 of file HybridQuantitativeCheckResult.cpp.

◆ getExplicitValueVector()

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

std::vector< ValueType > const & storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::getExplicitValueVector ( ) const

Definition at line 108 of file HybridQuantitativeCheckResult.cpp.

◆ getMax()

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

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

overridevirtual

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

Definition at line 250 of file HybridQuantitativeCheckResult.cpp.

◆ getMin()

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

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

overridevirtual

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

Definition at line 235 of file HybridQuantitativeCheckResult.cpp.

◆ getOdd()

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

storm::dd::Odd const & storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::getOdd ( ) const

Definition at line 103 of file HybridQuantitativeCheckResult.cpp.

◆ getSymbolicStates()

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

storm::dd::Bdd< Type > const & storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::getSymbolicStates ( ) const

Definition at line 88 of file HybridQuantitativeCheckResult.cpp.

◆ getSymbolicValueVector()

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

storm::dd::Add< Type, ValueType > const & storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::getSymbolicValueVector ( ) const

Definition at line 93 of file HybridQuantitativeCheckResult.cpp.

◆ isHybrid()

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

bool storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::isHybrid ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 73 of file HybridQuantitativeCheckResult.cpp.

◆ isHybridQuantitativeCheckResult()

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

bool storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::isHybridQuantitativeCheckResult ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 83 of file HybridQuantitativeCheckResult.cpp.

◆ isResultForAllStates()

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

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 78 of file HybridQuantitativeCheckResult.cpp.

◆ oneMinus()

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

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

overridevirtual

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

Definition at line 275 of file HybridQuantitativeCheckResult.cpp.

◆ operator=() [1/2]

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

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

default

◆ operator=() [2/2]

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

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

default

◆ sum()

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

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

overridevirtual

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

Definition at line 261 of file HybridQuantitativeCheckResult.cpp.

◆ toExplicitQuantitativeCheckResult()

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

std::unique_ptr< CheckResult > storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >::toExplicitQuantitativeCheckResult ( ) const

Definition at line 63 of file HybridQuantitativeCheckResult.cpp.

◆ writeToStream()

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

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

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 158 of file HybridQuantitativeCheckResult.cpp.

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

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

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ HybridQuantitativeCheckResult() [1/4]

◆ HybridQuantitativeCheckResult() [2/4]

◆ HybridQuantitativeCheckResult() [3/4]

◆ HybridQuantitativeCheckResult() [4/4]

Member Function Documentation

◆ average()

◆ clone()

◆ compareAgainstBound()

◆ filter()

◆ getExplicitStates()

◆ getExplicitValueVector()

◆ getMax()

◆ getMin()

◆ getOdd()

◆ getSymbolicStates()

◆ getSymbolicValueVector()

◆ isHybrid()

◆ isHybridQuantitativeCheckResult()

◆ isResultForAllStates()

◆ oneMinus()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ sum()

◆ toExplicitQuantitativeCheckResult()

◆ writeToStream()