Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::modelchecker::RegionCheckResult< ValueType > Class Template Reference

#include <RegionCheckResult.h>

Inheritance diagram for storm::modelchecker::RegionCheckResult< ValueType >:
Inheritance graph
[legend]
Collaboration diagram for storm::modelchecker::RegionCheckResult< ValueType >:
Collaboration graph
[legend]

Public Member Functions

 RegionCheckResult (std::vector< std::pair< storm::storage::ParameterRegion< ValueType >, storm::modelchecker::RegionResult > > const &regionResults)
 RegionCheckResult (std::vector< std::pair< storm::storage::ParameterRegion< ValueType >, storm::modelchecker::RegionResult > > &&regionResults)
virtual ~RegionCheckResult ()=default
virtual bool isRegionCheckResult () const
virtual bool isRegionRefinementCheckResult () const
std::vector< std::pair< storm::storage::ParameterRegion< ValueType >, storm::modelchecker::RegionResult > > const & getRegionResults () const
storm::storage::ParameterRegion< ValueType >::CoefficientType const & getSatFraction () const
storm::storage::ParameterRegion< ValueType >::CoefficientType const & getUnsatFraction () const
storm::storage::ParameterRegion< ValueType >::CoefficientType const & getIllDefinedFraction () const
virtual std::ostream & writeToStream (std::ostream &out) const override
virtual std::ostream & writeCondensedToStream (std::ostream &out) const
virtual std::ostream & writeIllustrationToStream (std::ostream &out) const
virtual void filter (QualitativeCheckResult const &filter) override
 Filters the current result wrt.
virtual std::unique_ptr< CheckResult > clone () const override
Public Member Functions inherited from storm::modelchecker::CheckResult
virtual ~CheckResult ()=default
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.
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

Protected Member Functions

virtual void initFractions (typename storm::storage::ParameterRegion< ValueType >::CoefficientType const &overallArea)

Protected Attributes

std::vector< std::pair< storm::storage::ParameterRegion< ValueType >, storm::modelchecker::RegionResult > > regionResults
storm::storage::ParameterRegion< ValueType >::CoefficientType satFraction
storm::storage::ParameterRegion< ValueType >::CoefficientType unsatFraction
storm::storage::ParameterRegion< ValueType >::CoefficientType illDefinedFraction

Detailed Description

template<typename ValueType>
class storm::modelchecker::RegionCheckResult< ValueType >

Definition at line 12 of file RegionCheckResult.h.

Constructor & Destructor Documentation

◆ RegionCheckResult() [1/2]

template<typename ValueType>
storm::modelchecker::RegionCheckResult< ValueType >::RegionCheckResult ( std::vector< std::pair< storm::storage::ParameterRegion< ValueType >, storm::modelchecker::RegionResult > > const & regionResults)

Definition at line 13 of file RegionCheckResult.cpp.

◆ RegionCheckResult() [2/2]

template<typename ValueType>
storm::modelchecker::RegionCheckResult< ValueType >::RegionCheckResult ( std::vector< std::pair< storm::storage::ParameterRegion< ValueType >, storm::modelchecker::RegionResult > > && regionResults)

Definition at line 24 of file RegionCheckResult.cpp.

◆ ~RegionCheckResult()

template<typename ValueType>
virtual storm::modelchecker::RegionCheckResult< ValueType >::~RegionCheckResult ( )
virtualdefault

Member Function Documentation

◆ clone()

template<typename ValueType>
std::unique_ptr< CheckResult > storm::modelchecker::RegionCheckResult< ValueType >::clone ( ) const
overridevirtual

Implements storm::modelchecker::CheckResult.

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

Definition at line 35 of file RegionCheckResult.cpp.

◆ filter()

template<typename ValueType>
void storm::modelchecker::RegionCheckResult< 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
filterA qualitative result that serves as a filter.

Implements storm::modelchecker::CheckResult.

Definition at line 130 of file RegionCheckResult.cpp.

◆ getIllDefinedFraction()

template<typename ValueType>
storm::storage::ParameterRegion< ValueType >::CoefficientType const & storm::modelchecker::RegionCheckResult< ValueType >::getIllDefinedFraction ( ) const

Definition at line 66 of file RegionCheckResult.cpp.

◆ getRegionResults()

template<typename ValueType>
std::vector< std::pair< storm::storage::ParameterRegion< ValueType >, storm::modelchecker::RegionResult > > const & storm::modelchecker::RegionCheckResult< ValueType >::getRegionResults ( ) const

Definition at line 50 of file RegionCheckResult.cpp.

◆ getSatFraction()

template<typename ValueType>
storm::storage::ParameterRegion< ValueType >::CoefficientType const & storm::modelchecker::RegionCheckResult< ValueType >::getSatFraction ( ) const

Definition at line 56 of file RegionCheckResult.cpp.

◆ getUnsatFraction()

template<typename ValueType>
storm::storage::ParameterRegion< ValueType >::CoefficientType const & storm::modelchecker::RegionCheckResult< ValueType >::getUnsatFraction ( ) const

Definition at line 61 of file RegionCheckResult.cpp.

◆ initFractions()

template<typename ValueType>
void storm::modelchecker::RegionCheckResult< ValueType >::initFractions ( typename storm::storage::ParameterRegion< ValueType >::CoefficientType const & overallArea)
protectedvirtual

Definition at line 111 of file RegionCheckResult.cpp.

◆ isRegionCheckResult()

template<typename ValueType>
bool storm::modelchecker::RegionCheckResult< ValueType >::isRegionCheckResult ( ) const
virtual

Definition at line 40 of file RegionCheckResult.cpp.

◆ isRegionRefinementCheckResult()

template<typename ValueType>
bool storm::modelchecker::RegionCheckResult< ValueType >::isRegionRefinementCheckResult ( ) const
virtual

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

Definition at line 45 of file RegionCheckResult.cpp.

◆ writeCondensedToStream()

template<typename ValueType>
std::ostream & storm::modelchecker::RegionCheckResult< ValueType >::writeCondensedToStream ( std::ostream & out) const
virtual

Definition at line 81 of file RegionCheckResult.cpp.

◆ writeIllustrationToStream()

template<typename ValueType>
std::ostream & storm::modelchecker::RegionCheckResult< ValueType >::writeIllustrationToStream ( std::ostream & out) const
virtual

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

Definition at line 105 of file RegionCheckResult.cpp.

◆ writeToStream()

template<typename ValueType>
std::ostream & storm::modelchecker::RegionCheckResult< ValueType >::writeToStream ( std::ostream & out) const
overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 71 of file RegionCheckResult.cpp.

Member Data Documentation

◆ illDefinedFraction

template<typename ValueType>
storm::storage::ParameterRegion<ValueType>::CoefficientType storm::modelchecker::RegionCheckResult< ValueType >::illDefinedFraction
protected

Definition at line 38 of file RegionCheckResult.h.

◆ regionResults

template<typename ValueType>
std::vector<std::pair<storm::storage::ParameterRegion<ValueType>, storm::modelchecker::RegionResult> > storm::modelchecker::RegionCheckResult< ValueType >::regionResults
protected

Definition at line 37 of file RegionCheckResult.h.

◆ satFraction

template<typename ValueType>
storm::storage::ParameterRegion<ValueType>::CoefficientType storm::modelchecker::RegionCheckResult< ValueType >::satFraction
protected

Definition at line 38 of file RegionCheckResult.h.

◆ unsatFraction

template<typename ValueType>
storm::storage::ParameterRegion<ValueType>::CoefficientType storm::modelchecker::RegionCheckResult< ValueType >::unsatFraction
protected

Definition at line 38 of file RegionCheckResult.h.

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