#include <ExplicitQualitativeCheckResult.h>

Inheritance diagram for storm::modelchecker::ExplicitQualitativeCheckResult:

[legend]

Collaboration diagram for storm::modelchecker::ExplicitQualitativeCheckResult:

[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)

	ExplicitQualitativeCheckResult (boost::variant< vector_type, map_type > &&truthValues)

	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

void	setValue (storm::storage::sparse::state_type, bool value)

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.

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

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

Definition at line 18 of file ExplicitQualitativeCheckResult.h.

Member Typedef Documentation

◆ map_type

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

Definition at line 21 of file ExplicitQualitativeCheckResult.h.

◆ vector_type

typedef storm::storage::BitVector storm::modelchecker::ExplicitQualitativeCheckResult::vector_type

Definition at line 20 of file ExplicitQualitativeCheckResult.h.

Constructor & Destructor Documentation

◆ ExplicitQualitativeCheckResult() [1/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( )

Definition at line 11 of file ExplicitQualitativeCheckResult.cpp.

◆ ~ExplicitQualitativeCheckResult()

virtual storm::modelchecker::ExplicitQualitativeCheckResult::~ExplicitQualitativeCheckResult ( )

virtualdefault

◆ ExplicitQualitativeCheckResult() [2/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( map_type const & map )

Definition at line 15 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [3/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( map_type && map )

Definition at line 19 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [4/10]

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

Definition at line 23 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [5/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( vector_type const & truthValues )

Definition at line 27 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [6/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( vector_type && truthValues )

Definition at line 31 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [7/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( boost::variant< vector_type, map_type > const & truthValues )

Definition at line 35 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [8/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( boost::variant< vector_type, map_type > && truthValues )

Definition at line 39 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [9/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( ExplicitQualitativeCheckResult const & other )

default

◆ ExplicitQualitativeCheckResult() [10/10]

storm::modelchecker::ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult ( ExplicitQualitativeCheckResult && other )

default

Member Function Documentation

◆ clone()

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

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 43 of file ExplicitQualitativeCheckResult.cpp.

◆ complement()

void storm::modelchecker::ExplicitQualitativeCheckResult::complement ( )

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 149 of file ExplicitQualitativeCheckResult.cpp.

◆ count()

uint64_t storm::modelchecker::ExplicitQualitativeCheckResult::count ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 116 of file ExplicitQualitativeCheckResult.cpp.

◆ existsTrue()

bool storm::modelchecker::ExplicitQualitativeCheckResult::existsTrue ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 91 of file ExplicitQualitativeCheckResult.cpp.

◆ filter()

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

◆ forallTrue()

bool storm::modelchecker::ExplicitQualitativeCheckResult::forallTrue ( ) const

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 103 of file ExplicitQualitativeCheckResult.cpp.

◆ getTruthValuesMap()

ExplicitQualitativeCheckResult::map_type const & storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesMap ( ) const

Definition at line 145 of file ExplicitQualitativeCheckResult.cpp.

◆ getTruthValuesVector()

ExplicitQualitativeCheckResult::vector_type const & storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector ( ) const

Definition at line 141 of file ExplicitQualitativeCheckResult.cpp.

◆ isExplicit()

bool storm::modelchecker::ExplicitQualitativeCheckResult::isExplicit ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 159 of file ExplicitQualitativeCheckResult.cpp.

◆ isExplicitQualitativeCheckResult()

bool storm::modelchecker::ExplicitQualitativeCheckResult::isExplicitQualitativeCheckResult ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 167 of file ExplicitQualitativeCheckResult.cpp.

◆ isResultForAllStates()

bool storm::modelchecker::ExplicitQualitativeCheckResult::isResultForAllStates ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 163 of file ExplicitQualitativeCheckResult.cpp.

◆ operator&=()

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

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 81 of file ExplicitQualitativeCheckResult.cpp.

◆ operator=() [1/2]

ExplicitQualitativeCheckResult & storm::modelchecker::ExplicitQualitativeCheckResult::operator= ( ExplicitQualitativeCheckResult && other )

default

◆ operator=() [2/2]

ExplicitQualitativeCheckResult & storm::modelchecker::ExplicitQualitativeCheckResult::operator= ( ExplicitQualitativeCheckResult const & other )

default

◆ operator[]()

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

Definition at line 130 of file ExplicitQualitativeCheckResult.cpp.

◆ operator|=()

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

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 86 of file ExplicitQualitativeCheckResult.cpp.

◆ setValue()

void storm::modelchecker::ExplicitQualitativeCheckResult::setValue	(	storm::storage::sparse::state_type	,
		bool	value
	)

◆ toJson()

template<typename JsonRationalType >

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

Definition at line 263 of file ExplicitQualitativeCheckResult.cpp.

◆ writeToStream()

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

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 171 of file ExplicitQualitativeCheckResult.cpp.

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

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()

◆ getTruthValuesMap()

◆ getTruthValuesVector()

◆ isExplicit()

◆ isExplicitQualitativeCheckResult()

◆ isResultForAllStates()

◆ operator&=()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator[]()

◆ operator|=()

◆ setValue()

◆ toJson()

◆ writeToStream()