storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType > Class Template Reference

#include <HybridQuantitativeCheckResult.h>

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

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

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< double >
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
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, typename ValueType = double>
class storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >

Definition at line 13 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 15 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< double >.

Definition at line 267 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 30 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< double >.

Definition at line 36 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 211 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 95 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 105 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< double >.

Definition at line 247 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< double >.

Definition at line 232 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 100 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 85 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 90 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 70 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 80 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 75 of file HybridQuantitativeCheckResult.cpp.

oneMinus()

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

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

overridevirtual

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

Definition at line 272 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< double >.

Definition at line 258 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 60 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 155 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