#include <LexicographicCheckResult.h>

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

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

Public Member Functions
	LexicographicCheckResult ()=default
	LexicographicCheckResult (std::vector< ValueType > const &values, storm::storage::sparse::state_type state)
virtual	~LexicographicCheckResult ()=default
std::vector< ValueType > const &	getInitialStateValue () const
storm::storage::sparse::state_type const &	getState () const
virtual bool	isLexicographicCheckResult () const override
virtual std::unique_ptr< CheckResult >	clone () const override
virtual bool	isExplicit () const override
virtual void	filter (QualitativeCheckResult const &filter) override
	Filters the current result wrt.
virtual std::ostream &	writeToStream (std::ostream &out) const override
Public Member Functions inherited from storm::modelchecker::CheckResult
virtual	~CheckResult ()=default
virtual bool	isSymbolic () const
virtual bool	isHybrid () const
virtual bool	isQuantitative () const
virtual bool	isQualitative () const
virtual bool	isParetoCurveCheckResult () 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

Detailed Description

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

Definition at line 11 of file LexicographicCheckResult.h.

Constructor & Destructor Documentation

◆ LexicographicCheckResult() [1/2]

template<typename ValueType>

storm::modelchecker::LexicographicCheckResult< ValueType >::LexicographicCheckResult ( )

default

◆ LexicographicCheckResult() [2/2]

template<typename ValueType>

storm::modelchecker::LexicographicCheckResult< ValueType >::LexicographicCheckResult	(	std::vector< ValueType > const &	values,
		storm::storage::sparse::state_type	state )

Definition at line 13 of file LexicographicCheckResult.cpp.

◆ ~LexicographicCheckResult()

template<typename ValueType>

virtual storm::modelchecker::LexicographicCheckResult< ValueType >::~LexicographicCheckResult ( )

virtualdefault

Member Function Documentation

◆ clone()

template<typename ValueType>

std::unique_ptr< CheckResult > storm::modelchecker::LexicographicCheckResult< ValueType >::clone ( ) const

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 32 of file LexicographicCheckResult.cpp.

◆ filter()

template<typename ValueType>

void storm::modelchecker::LexicographicCheckResult< 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 42 of file LexicographicCheckResult.cpp.