Storm
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
 
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
 
virtual std::ostream & writeToStream (std::ostream &out) const =0
 
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 40 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< double > & storm::modelchecker::CheckResult::asExplicitParetoCurveCheckResult ( )

Definition at line 104 of file CheckResult.cpp.

◆ asExplicitParetoCurveCheckResult() [2/3]

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

Definition at line 109 of file CheckResult.cpp.

◆ asExplicitParetoCurveCheckResult() [3/3]

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

◆ asExplicitQualitativeCheckResult() [1/2]

ExplicitQualitativeCheckResult & storm::modelchecker::CheckResult::asExplicitQualitativeCheckResult ( )

Definition at line 85 of file CheckResult.cpp.

◆ asExplicitQualitativeCheckResult() [2/2]

ExplicitQualitativeCheckResult const & storm::modelchecker::CheckResult::asExplicitQualitativeCheckResult ( ) const

Definition at line 89 of file CheckResult.cpp.

◆ asExplicitQuantitativeCheckResult() [1/3]

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

Definition at line 94 of file CheckResult.cpp.

◆ asExplicitQuantitativeCheckResult() [2/3]

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

Definition at line 99 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 162 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 167 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< double > & storm::modelchecker::CheckResult::asLexicographicCheckResult ( )

Definition at line 114 of file CheckResult.cpp.

◆ asLexicographicCheckResult() [2/3]

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

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

◆ asQualitativeCheckResult() [2/2]

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

Definition at line 127 of file CheckResult.cpp.

◆ asQuantitativeCheckResult() [1/3]

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

Definition at line 132 of file CheckResult.cpp.

◆ asQuantitativeCheckResult() [2/3]

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

Definition at line 137 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 172 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 177 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 142 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 147 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 152 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 157 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, 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, 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::ExplicitQuantitativeCheckResult< ValueType >.

Definition at line 181 of file CheckResult.cpp.

◆ isExplicit()

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

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

Definition at line 20 of file CheckResult.cpp.

◆ isExplicitParetoCurveCheckResult()

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

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

Definition at line 65 of file CheckResult.cpp.

◆ isExplicitQualitativeCheckResult()

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

Reimplemented in storm::modelchecker::ExplicitQualitativeCheckResult.

Definition at line 57 of file CheckResult.cpp.

◆ isExplicitQuantitativeCheckResult()

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

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

Definition at line 61 of file CheckResult.cpp.

◆ isHybrid()

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

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

Definition at line 28 of file CheckResult.cpp.

◆ isHybridQuantitativeCheckResult()

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

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

Definition at line 81 of file CheckResult.cpp.

◆ isLexicographicCheckResult()

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

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

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

◆ isQualitative()

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

Reimplemented in storm::modelchecker::QualitativeCheckResult.

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

◆ isResultForAllStates()

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

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

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

◆ isSymbolicParetoCurveCheckResult()

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

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

Definition at line 77 of file CheckResult.cpp.

◆ isSymbolicQualitativeCheckResult()

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

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

Definition at line 69 of file CheckResult.cpp.

◆ isSymbolicQuantitativeCheckResult()

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

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

Definition at line 73 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, 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: