#include <ExplicitQualitativeCheckResult.h>

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

[legend]

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

[legend]

Public Types
typedef storm::storage::BitVector	vector_type
typedef std::map< storm::storage::sparse::state_type, bool >	map_type

Public Member Functions
	ExplicitQualitativeCheckResult ()
virtual	~ExplicitQualitativeCheckResult ()=default
	ExplicitQualitativeCheckResult (map_type const &map)
	ExplicitQualitativeCheckResult (map_type &&map)
	ExplicitQualitativeCheckResult (storm::storage::sparse::state_type state, bool value)
	ExplicitQualitativeCheckResult (vector_type const &truthValues)
	ExplicitQualitativeCheckResult (vector_type &&truthValues)
	ExplicitQualitativeCheckResult (boost::variant< vector_type, map_type > const &truthValues, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	ExplicitQualitativeCheckResult (boost::variant< vector_type, map_type > &&truthValues, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	ExplicitQualitativeCheckResult (ExplicitQualitativeCheckResult const &other)=default
ExplicitQualitativeCheckResult &	operator= (ExplicitQualitativeCheckResult const &other)=default
	ExplicitQualitativeCheckResult (ExplicitQualitativeCheckResult &&other)=default
ExplicitQualitativeCheckResult &	operator= (ExplicitQualitativeCheckResult &&other)=default
virtual std::unique_ptr< CheckResult >	clone () const override
bool	operator[] (storm::storage::sparse::state_type index) const
virtual bool	isExplicit () const override
virtual bool	isResultForAllStates () const override
virtual bool	isExplicitQualitativeCheckResult () const override
virtual QualitativeCheckResult &	operator&= (QualitativeCheckResult const &other) override
virtual QualitativeCheckResult &	operator\|= (QualitativeCheckResult const &other) override
virtual void	complement () override
vector_type const &	getTruthValuesVector () const
map_type const &	getTruthValuesMap () const
virtual bool	existsTrue () const override
virtual bool	forallTrue () const override
virtual uint64_t	count () const override
virtual std::ostream &	writeToStream (std::ostream &out) const override
virtual void	filter (QualitativeCheckResult const &filter) override
	Filters the current result wrt.
virtual bool	hasScheduler () const override
void	setScheduler (std::unique_ptr< storm::storage::Scheduler< ValueType > > &&scheduler)
storm::storage::Scheduler< ValueType > const &	getScheduler () const
storm::storage::Scheduler< ValueType > &	getScheduler ()
template<typename JsonRationalType>
storm::json< JsonRationalType >	toJson (std::optional< storm::storage::sparse::StateValuations > const &stateValuations=std::nullopt, std::optional< storm::models::sparse::StateLabeling > const &stateLabels=std::nullopt) const
Public Member Functions inherited from storm::modelchecker::QualitativeCheckResult
virtual	~QualitativeCheckResult ()=default
virtual bool	isQualitative () 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	isParetoCurveCheckResult () const
virtual bool	isLexicographicCheckResult () 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
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
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::ExplicitQualitativeCheckResult< ValueType >

Definition at line 20 of file ExplicitQualitativeCheckResult.h.

Member Typedef Documentation

◆ map_type

template<typename ValueType>

typedef std::map<storm::storage::sparse::state_type, bool> storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::map_type

Definition at line 23 of file ExplicitQualitativeCheckResult.h.

◆ vector_type

template<typename ValueType>

typedef storm::storage::BitVector storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::vector_type

Definition at line 22 of file ExplicitQualitativeCheckResult.h.

Constructor & Destructor Documentation

◆ ExplicitQualitativeCheckResult() [1/10]

template<typename ValueType>

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

Definition at line 15 of file ExplicitQualitativeCheckResult.cpp.

◆ ~ExplicitQualitativeCheckResult()

template<typename ValueType>

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

virtualdefault

◆ ExplicitQualitativeCheckResult() [2/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult ( map_type const & map )

Definition at line 20 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [3/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult ( map_type && map )

Definition at line 25 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [4/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult	(	storm::storage::sparse::state_type	state,
		bool	value )

Definition at line 30 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [5/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult ( vector_type const & truthValues )

Definition at line 35 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [6/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult ( vector_type && truthValues )

Definition at line 40 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [7/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult	(	boost::variant< vector_type, map_type > const &	truthValues,
		std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > >	scheduler = {} )

Definition at line 45 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [8/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult	(	boost::variant< vector_type, map_type > &&	truthValues,
		std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > >	scheduler = {} )

Definition at line 52 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [9/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult ( ExplicitQualitativeCheckResult< ValueType > const & other )

default

◆ ExplicitQualitativeCheckResult() [10/10]

template<typename ValueType>

storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::ExplicitQualitativeCheckResult ( ExplicitQualitativeCheckResult< ValueType > && other )

default

Member Function Documentation

◆ clone()

template<typename ValueType>

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

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 59 of file ExplicitQualitativeCheckResult.cpp.

◆ complement()

template<typename ValueType>

void storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::complement ( )

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 177 of file ExplicitQualitativeCheckResult.cpp.

◆ count()

template<typename ValueType>

uint64_t storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::count ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 140 of file ExplicitQualitativeCheckResult.cpp.

◆ existsTrue()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::existsTrue ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 112 of file ExplicitQualitativeCheckResult.cpp.

◆ filter()

template<typename ValueType>

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

◆ forallTrue()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::forallTrue ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 126 of file ExplicitQualitativeCheckResult.cpp.

◆ getScheduler() [1/2]

template<typename ValueType>

storm::storage::Scheduler< ValueType > & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::getScheduler ( )

Definition at line 294 of file ExplicitQualitativeCheckResult.cpp.

◆ getScheduler() [2/2]

template<typename ValueType>

storm::storage::Scheduler< ValueType > const & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::getScheduler ( ) const

Definition at line 288 of file ExplicitQualitativeCheckResult.cpp.

◆ getTruthValuesMap()

template<typename ValueType>

ExplicitQualitativeCheckResult< ValueType >::map_type const & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::getTruthValuesMap ( ) const

Definition at line 172 of file ExplicitQualitativeCheckResult.cpp.

◆ getTruthValuesVector()

template<typename ValueType>

ExplicitQualitativeCheckResult< ValueType >::vector_type const & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::getTruthValuesVector ( ) const

Definition at line 167 of file ExplicitQualitativeCheckResult.cpp.

◆ hasScheduler()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::hasScheduler ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 278 of file ExplicitQualitativeCheckResult.cpp.

◆ isExplicit()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::isExplicit ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 188 of file ExplicitQualitativeCheckResult.cpp.

◆ isExplicitQualitativeCheckResult()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::isExplicitQualitativeCheckResult ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 198 of file ExplicitQualitativeCheckResult.cpp.

◆ isResultForAllStates()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::isResultForAllStates ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 193 of file ExplicitQualitativeCheckResult.cpp.

◆ operator&=()

template<typename ValueType>

QualitativeCheckResult & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::operator&= ( QualitativeCheckResult const & other )

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 100 of file ExplicitQualitativeCheckResult.cpp.

◆ operator=() [1/2]

template<typename ValueType>

ExplicitQualitativeCheckResult & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::operator= ( ExplicitQualitativeCheckResult< ValueType > && other )

default

◆ operator=() [2/2]

template<typename ValueType>

ExplicitQualitativeCheckResult & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::operator= ( ExplicitQualitativeCheckResult< ValueType > const & other )

default

◆ operator[]()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::operator[] ( storm::storage::sparse::state_type index ) const

Definition at line 155 of file ExplicitQualitativeCheckResult.cpp.

◆ operator|=()

template<typename ValueType>

QualitativeCheckResult & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::operator|= ( QualitativeCheckResult const & other )

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 106 of file ExplicitQualitativeCheckResult.cpp.

◆ setScheduler()

template<typename ValueType>

void storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::setScheduler ( std::unique_ptr< storm::storage::Scheduler< ValueType > > && scheduler )

Definition at line 283 of file ExplicitQualitativeCheckResult.cpp.

◆ toJson()

template<typename ValueType>

template<typename JsonRationalType>

template storm::json< storm::RationalNumber > storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::toJson< storm::RationalNumber >	(	std::optional< storm::storage::sparse::StateValuations > const &	stateValuations = std::nullopt,
		std::optional< storm::models::sparse::StateLabeling > const &	stateLabels = std::nullopt ) const

Definition at line 319 of file ExplicitQualitativeCheckResult.cpp.

◆ writeToStream()

template<typename ValueType>

std::ostream & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::writeToStream ( std::ostream & out ) const

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 203 of file ExplicitQualitativeCheckResult.cpp.

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

src/storm/modelchecker/results/CheckResult.h
src/storm/modelchecker/results/ExplicitQualitativeCheckResult.h
src/storm/modelchecker/results/ExplicitQualitativeCheckResult.cpp

Public Types

Public Member Functions

Detailed Description

Member Typedef Documentation

◆ map_type

◆ vector_type

Constructor & Destructor Documentation

◆ ExplicitQualitativeCheckResult() [1/10]

◆ ~ExplicitQualitativeCheckResult()

◆ ExplicitQualitativeCheckResult() [2/10]

◆ ExplicitQualitativeCheckResult() [3/10]

◆ ExplicitQualitativeCheckResult() [4/10]

◆ ExplicitQualitativeCheckResult() [5/10]

◆ ExplicitQualitativeCheckResult() [6/10]

◆ ExplicitQualitativeCheckResult() [7/10]

◆ ExplicitQualitativeCheckResult() [8/10]

◆ ExplicitQualitativeCheckResult() [9/10]

◆ ExplicitQualitativeCheckResult() [10/10]

Member Function Documentation

◆ clone()

◆ complement()

◆ count()

◆ existsTrue()

◆ filter()

◆ forallTrue()

◆ getScheduler() [1/2]

◆ getScheduler() [2/2]

◆ getTruthValuesMap()

◆ getTruthValuesVector()

◆ hasScheduler()

◆ isExplicit()

◆ isExplicitQualitativeCheckResult()

◆ isResultForAllStates()

◆ operator&=()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator[]()

◆ operator|=()

◆ setScheduler()

◆ toJson()

◆ writeToStream()