#include <RegionCheckResult.h>

Inheritance diagram for storm::modelchecker::RegionCheckResult< ValueType >:

[legend]

Collaboration diagram for storm::modelchecker::RegionCheckResult< ValueType >:

[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

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

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

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

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

filter A qualitative result that serves as a filter.

Implements storm::modelchecker::CheckResult.

Definition at line 117 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 102 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 76 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 96 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 66 of file RegionCheckResult.cpp.

Member Data Documentation

◆ regionResults

template<typename ValueType >

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

protected

Definition at line 36 of file RegionCheckResult.h.

◆ satFraction

template<typename ValueType >

storm::storage::ParameterRegion<ValueType>::CoefficientType storm::modelchecker::RegionCheckResult< ValueType >::satFraction

protected

Definition at line 37 of file RegionCheckResult.h.

◆ unsatFraction

template<typename ValueType >

storm::storage::ParameterRegion<ValueType>::CoefficientType storm::modelchecker::RegionCheckResult< ValueType >::unsatFraction

protected

Definition at line 37 of file RegionCheckResult.h.

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

src/storm-pars/modelchecker/results/RegionCheckResult.h
src/storm-pars/modelchecker/results/RegionCheckResult.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ RegionCheckResult() [1/2]

◆ RegionCheckResult() [2/2]

◆ ~RegionCheckResult()

Member Function Documentation

◆ clone()

◆ filter()

◆ getRegionResults()

◆ getSatFraction()

◆ getUnsatFraction()

◆ initFractions()

◆ isRegionCheckResult()

◆ isRegionRefinementCheckResult()

◆ writeCondensedToStream()

◆ writeIllustrationToStream()

◆ writeToStream()

Member Data Documentation

◆ regionResults

◆ satFraction

◆ unsatFraction