Storm 1.12.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | List of all members
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
 
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 102 of file CheckResult.cpp.

◆ asExplicitParetoCurveCheckResult() [2/3]

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

Definition at line 107 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 87 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 92 of file CheckResult.cpp.

◆ asExplicitQuantitativeCheckResult() [2/3]

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

Definition at line 97 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 160 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 165 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 112 of file CheckResult.cpp.

◆ asLexicographicCheckResult() [2/3]

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

Definition at line 117 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 121 of file CheckResult.cpp.

◆ asQualitativeCheckResult() [2/2]

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

Definition at line 125 of file CheckResult.cpp.

◆ asQuantitativeCheckResult() [1/3]

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

Definition at line 130 of file CheckResult.cpp.

◆ asQuantitativeCheckResult() [2/3]

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

Definition at line 135 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 170 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 175 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 140 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 145 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 150 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 155 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::RegionCheckResult< ValueType >, storm::modelchecker::RegionRefinementCheckResult< ValueType >, storm::modelchecker::ExplicitParetoCurveCheckResult< ValueType >, storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >, storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >, storm::modelchecker::LexicographicCheckResult< 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::RegionCheckResult< ValueType >, storm::modelchecker::ExplicitParetoCurveCheckResult< ValueType >, storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >, storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >, storm::modelchecker::HybridQuantitativeCheckResult< Type, ValueType >, storm::modelchecker::LexicographicCheckResult< 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 179 of file CheckResult.cpp.

◆ 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::RegionCheckResult< ValueType >, 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::SymbolicQualitativeCheckResult< Type >, and storm::modelchecker::SymbolicQuantitativeCheckResult< Type, ValueType >.

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