#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

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

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.