Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::modelchecker::CheckResult Class Referenceabstract

#include <CheckResult.h>

Inheritance diagram for storm::modelchecker::CheckResult:
Inheritance graph
[legend]

Public Member Functions

virtual ~CheckResult ()=default
virtual std::unique_ptr< CheckResult > clone () const =0
virtual void filter (QualitativeCheckResult const &filter)=0
 Filters the current result wrt.
virtual bool isExplicit () const
virtual bool isSymbolic () const
virtual bool isHybrid () const
virtual bool isQuantitative () 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
virtual bool isHybridQuantitativeCheckResult () const
virtual bool isResultForAllStates () 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.
virtual std::ostream & writeToStream (std::ostream &out) const =0
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

Definition at line 41 of file CheckResult.h.

Constructor & Destructor Documentation

◆ ~CheckResult()

virtual storm::modelchecker::CheckResult::~CheckResult ( )
virtualdefault

Member Function Documentation

◆ asExplicitParetoCurveCheckResult() [1/3]

template<typename ValueType>
template ExplicitParetoCurveCheckResult< storm::RationalNumber > & storm::modelchecker::CheckResult::asExplicitParetoCurveCheckResult ( )

Definition at line 106 of file CheckResult.cpp.

◆ asExplicitParetoCurveCheckResult() [2/3]

template<typename ValueType>
template ExplicitParetoCurveCheckResult< storm::RationalNumber > const & storm::modelchecker::CheckResult::asExplicitParetoCurveCheckResult ( ) const

Definition at line 111 of file CheckResult.cpp.

◆ asExplicitParetoCurveCheckResult() [3/3]

template<typename ValueType>
ExplicitParetoCurveCheckResult< ValueType > const & storm::modelchecker::CheckResult::asExplicitParetoCurveCheckResult ( ) const

◆ asExplicitQualitativeCheckResult() [1/3]

template<typename ValueType>
template ExplicitQualitativeCheckResult< storm::Interval > & storm::modelchecker::CheckResult::asExplicitQualitativeCheckResult ( )

Definition at line 82 of file CheckResult.cpp.

◆ asExplicitQualitativeCheckResult() [2/3]

template<typename ValueType>
template ExplicitQualitativeCheckResult< storm::Interval > const & storm::modelchecker::CheckResult::asExplicitQualitativeCheckResult ( ) const

Definition at line 88 of file CheckResult.cpp.

◆ asExplicitQualitativeCheckResult() [3/3]

template<typename ValueType>
ExplicitQualitativeCheckResult< ValueType > const & storm::modelchecker::CheckResult::asExplicitQualitativeCheckResult ( ) const

◆ asExplicitQuantitativeCheckResult() [1/3]

template<typename ValueType>
template ExplicitQuantitativeCheckResult< storm::RationalFunction > & storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult ( )

Definition at line 94 of file CheckResult.cpp.

◆ asExplicitQuantitativeCheckResult() [2/3]

template<typename ValueType>
template ExplicitQuantitativeCheckResult< storm::RationalFunction > const & storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult ( ) const

Definition at line 100 of file CheckResult.cpp.

◆ asExplicitQuantitativeCheckResult() [3/3]

template<typename ValueType>
ExplicitQuantitativeCheckResult< ValueType > const & storm::modelchecker::CheckResult::asExplicitQuantitativeCheckResult ( ) const

◆ asHybridQuantitativeCheckResult() [1/3]

template<storm::dd::DdType Type, typename ValueType>
template HybridQuantitativeCheckResult< storm::dd::DdType::Sylvan, double > & storm::modelchecker::CheckResult::asHybridQuantitativeCheckResult ( )

Definition at line 166 of file CheckResult.cpp.

◆ asHybridQuantitativeCheckResult() [2/3]

template<storm::dd::DdType Type, typename ValueType>
template HybridQuantitativeCheckResult< storm::dd::DdType::Sylvan, double > const & storm::modelchecker::CheckResult::asHybridQuantitativeCheckResult ( ) const

Definition at line 171 of file CheckResult.cpp.

◆ asHybridQuantitativeCheckResult() [3/3]

template<storm::dd::DdType Type, typename ValueType>
HybridQuantitativeCheckResult< Type, ValueType > const & storm::modelchecker::CheckResult::asHybridQuantitativeCheckResult ( ) const

◆ asLexicographicCheckResult() [1/3]

template<typename ValueType>
template LexicographicCheckResult< storm::RationalNumber > & storm::modelchecker::CheckResult::asLexicographicCheckResult ( )

Definition at line 116 of file CheckResult.cpp.

◆ asLexicographicCheckResult() [2/3]

template<typename ValueType>
template LexicographicCheckResult< storm::RationalNumber > const & storm::modelchecker::CheckResult::asLexicographicCheckResult ( ) const

Definition at line 121 of file CheckResult.cpp.

◆ asLexicographicCheckResult() [3/3]

template<typename ValueType>
LexicographicCheckResult< ValueType > const & storm::modelchecker::CheckResult::asLexicographicCheckResult ( ) const

◆ asQualitativeCheckResult() [1/2]

QualitativeCheckResult & storm::modelchecker::CheckResult::asQualitativeCheckResult ( )

Definition at line 125 of file CheckResult.cpp.

◆ asQualitativeCheckResult() [2/2]

QualitativeCheckResult const & storm::modelchecker::CheckResult::asQualitativeCheckResult ( ) const

Definition at line 129 of file CheckResult.cpp.

◆ asQuantitativeCheckResult() [1/3]

template<typename ValueType>
template QuantitativeCheckResult< storm::RationalFunction > & storm::modelchecker::CheckResult::asQuantitativeCheckResult ( )

Definition at line 134 of file CheckResult.cpp.

◆ asQuantitativeCheckResult() [2/3]

template<typename ValueType>
template QuantitativeCheckResult< storm::RationalFunction > const & storm::modelchecker::CheckResult::asQuantitativeCheckResult ( ) const

Definition at line 140 of file CheckResult.cpp.

◆ asQuantitativeCheckResult() [3/3]

template<typename ValueType>
QuantitativeCheckResult< ValueType > const & storm::modelchecker::CheckResult::asQuantitativeCheckResult ( ) const

◆ asSymbolicParetoCurveCheckResult() [1/3]

template<storm::dd::DdType Type, typename ValueType>
template SymbolicParetoCurveCheckResult< storm::dd::DdType::Sylvan, double > & storm::modelchecker::CheckResult::asSymbolicParetoCurveCheckResult ( )

Definition at line 176 of file CheckResult.cpp.

◆ asSymbolicParetoCurveCheckResult() [2/3]

template<storm::dd::DdType Type, typename ValueType>
template SymbolicParetoCurveCheckResult< storm::dd::DdType::Sylvan, double > const & storm::modelchecker::CheckResult::asSymbolicParetoCurveCheckResult ( ) const

Definition at line 181 of file CheckResult.cpp.

◆ asSymbolicParetoCurveCheckResult() [3/3]

template<storm::dd::DdType Type, typename ValueType>
SymbolicParetoCurveCheckResult< Type, ValueType > const & storm::modelchecker::CheckResult::asSymbolicParetoCurveCheckResult ( ) const

◆ asSymbolicQualitativeCheckResult() [1/3]

template<storm::dd::DdType Type>
template SymbolicQualitativeCheckResult< storm::dd::DdType::Sylvan > & storm::modelchecker::CheckResult::asSymbolicQualitativeCheckResult ( )

Definition at line 146 of file CheckResult.cpp.

◆ asSymbolicQualitativeCheckResult() [2/3]

template<storm::dd::DdType Type>
template SymbolicQualitativeCheckResult< storm::dd::DdType::Sylvan > const & storm::modelchecker::CheckResult::asSymbolicQualitativeCheckResult ( ) const

Definition at line 151 of file CheckResult.cpp.

◆ asSymbolicQualitativeCheckResult() [3/3]

template<storm::dd::DdType Type>
SymbolicQualitativeCheckResult< Type > const & storm::modelchecker::CheckResult::asSymbolicQualitativeCheckResult ( ) const

◆ asSymbolicQuantitativeCheckResult() [1/3]

template<storm::dd::DdType Type, typename ValueType>
template SymbolicQuantitativeCheckResult< storm::dd::DdType::Sylvan, storm::RationalFunction > & storm::modelchecker::CheckResult::asSymbolicQuantitativeCheckResult ( )

Definition at line 156 of file CheckResult.cpp.

◆ asSymbolicQuantitativeCheckResult() [2/3]

template<storm::dd::DdType Type, typename ValueType>
template SymbolicQuantitativeCheckResult< storm::dd::DdType::Sylvan, storm::RationalFunction > const & storm::modelchecker::CheckResult::asSymbolicQuantitativeCheckResult ( ) const

Definition at line 161 of file CheckResult.cpp.

◆ asSymbolicQuantitativeCheckResult() [3/3]

template<storm::dd::DdType Type, typename ValueType>
SymbolicQuantitativeCheckResult< Type, ValueType > const & storm::modelchecker::CheckResult::asSymbolicQuantitativeCheckResult ( ) const

◆ clone()

virtual std::unique_ptr< CheckResult > storm::modelchecker::CheckResult::clone ( ) const
pure virtual

Implemented in storm::modelchecker::ExplicitParetoCurveCheckResult< ValueType >, storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >, storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >, storm::modelchecker::LexicographicCheckResult< ValueType >, storm::modelchecker::RegionCheckResult< ValueType >, storm::modelchecker::RegionRefinementCheckResult< ValueType >, storm::modelchecker::SymbolicParetoCurveCheckResult< Type, ValueType >, storm::modelchecker::SymbolicQualitativeCheckResult< Type >, and storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >.

◆ filter()

virtual void storm::modelchecker::CheckResult::filter ( QualitativeCheckResult const & filter)
pure virtual

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
filterA qualitative result that serves as a filter.

Implemented in storm::modelchecker::ExplicitParetoCurveCheckResult< ValueType >, storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >, storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >, storm::modelchecker::LexicographicCheckResult< ValueType >, storm::modelchecker::RegionCheckResult< ValueType >, storm::modelchecker::SymbolicParetoCurveCheckResult< Type, ValueType >, storm::modelchecker::SymbolicQualitativeCheckResult< Type >, and storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >.

◆ hasScheduler()

bool storm::modelchecker::CheckResult::hasScheduler ( ) const
virtual

Reimplemented in storm::modelchecker::ExplicitParetoCurveCheckResult< ValueType >, storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, and storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >.

Definition at line 185 of file CheckResult.cpp.

◆ hasValueType()

template<typename T>
bool storm::modelchecker::CheckResult::hasValueType ( ) const
inline

Checks whether the ValueType of the result matches the given type.

Template Parameters
Ttype to match
Returns

Definition at line 137 of file CheckResult.h.

◆ isExplicit()

bool storm::modelchecker::CheckResult::isExplicit ( ) const
virtual

Reimplemented in storm::modelchecker::ExplicitParetoCurveCheckResult< ValueType >, storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >, and storm::modelchecker::LexicographicCheckResult< ValueType >.

Definition at line 16 of file CheckResult.cpp.

◆ isExplicitParetoCurveCheckResult()

bool storm::modelchecker::CheckResult::isExplicitParetoCurveCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::ExplicitParetoCurveCheckResult< ValueType >.

Definition at line 61 of file CheckResult.cpp.

◆ isExplicitQualitativeCheckResult()

bool storm::modelchecker::CheckResult::isExplicitQualitativeCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >.

Definition at line 53 of file CheckResult.cpp.

◆ isExplicitQuantitativeCheckResult()

bool storm::modelchecker::CheckResult::isExplicitQuantitativeCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >.

Definition at line 57 of file CheckResult.cpp.

◆ isHybrid()

bool storm::modelchecker::CheckResult::isHybrid ( ) const
virtual

Reimplemented in storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >.

Definition at line 24 of file CheckResult.cpp.

◆ isHybridQuantitativeCheckResult()

bool storm::modelchecker::CheckResult::isHybridQuantitativeCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >.

Definition at line 77 of file CheckResult.cpp.

◆ isLexicographicCheckResult()

bool storm::modelchecker::CheckResult::isLexicographicCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::LexicographicCheckResult< ValueType >.

Definition at line 40 of file CheckResult.cpp.

◆ isParetoCurveCheckResult()

bool storm::modelchecker::CheckResult::isParetoCurveCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::ParetoCurveCheckResult< ValueType >, and storm::modelchecker::ParetoCurveCheckResult< double >.

Definition at line 36 of file CheckResult.cpp.

◆ isQualitative()

bool storm::modelchecker::CheckResult::isQualitative ( ) const
virtual

Reimplemented in storm::modelchecker::QualitativeCheckResult.

Definition at line 32 of file CheckResult.cpp.

◆ isQuantitative()

bool storm::modelchecker::CheckResult::isQuantitative ( ) const
virtual

Reimplemented in storm::modelchecker::QuantitativeCheckResult< ValueType >, and storm::modelchecker::QuantitativeCheckResult< double >.

Definition at line 28 of file CheckResult.cpp.

◆ isResultForAllStates()

bool storm::modelchecker::CheckResult::isResultForAllStates ( ) const
virtual

Reimplemented in storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >, storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >, storm::modelchecker::SymbolicQualitativeCheckResult< Type >, and storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >.

Definition at line 44 of file CheckResult.cpp.

◆ isSymbolic()

bool storm::modelchecker::CheckResult::isSymbolic ( ) const
virtual

Reimplemented in storm::modelchecker::SymbolicParetoCurveCheckResult< Type, ValueType >, storm::modelchecker::SymbolicQualitativeCheckResult< Type >, and storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >.

Definition at line 20 of file CheckResult.cpp.

◆ isSymbolicParetoCurveCheckResult()

bool storm::modelchecker::CheckResult::isSymbolicParetoCurveCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::SymbolicParetoCurveCheckResult< Type, ValueType >.

Definition at line 73 of file CheckResult.cpp.

◆ isSymbolicQualitativeCheckResult()

bool storm::modelchecker::CheckResult::isSymbolicQualitativeCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::SymbolicQualitativeCheckResult< Type >.

Definition at line 65 of file CheckResult.cpp.

◆ isSymbolicQuantitativeCheckResult()

bool storm::modelchecker::CheckResult::isSymbolicQuantitativeCheckResult ( ) const
virtual

Reimplemented in storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >.

Definition at line 69 of file CheckResult.cpp.

◆ writeToStream()

virtual std::ostream & storm::modelchecker::CheckResult::writeToStream ( std::ostream & out) const
pure virtual

Implemented in storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >, storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >, storm::modelchecker::LexicographicCheckResult< ValueType >, storm::modelchecker::ParetoCurveCheckResult< ValueType >, storm::modelchecker::ParetoCurveCheckResult< double >, storm::modelchecker::RegionCheckResult< ValueType >, storm::modelchecker::SymbolicQualitativeCheckResult< Type >, and storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >.

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