A qualitative check result over the states of a sparse model. More...

#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

Public Member Functions
	ExplicitQualitativeCheckResult (storm::storage::sparse::state_type state, bool value)
	Creates a result that holds the given truth value for the given state only.
	ExplicitQualitativeCheckResult (vector_type const &truthValues, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	Creates a result for all states of a model with as many states as the given bit vector has bits.
	ExplicitQualitativeCheckResult (vector_type &&truthValues, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	ExplicitQualitativeCheckResult (storm::storage::BitVector states, vector_type &&truthValues, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	Creates a result for the given states only.
virtual	~ExplicitQualitativeCheckResult ()=default
	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 state) const
	Retrieves the truth value of the given state.
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
bool	hasValueForState (storm::storage::sparse::state_type state) const
	Retrieves whether the result holds a truth value for the given state.
storm::storage::BitVector const &	getStates () const
	Retrieves the states this result holds truth values for.
vector_type const &	getTruthValuesVector () const
	Retrieves the truth values, one per state this result is for.
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::Valuations > 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 >

A qualitative check result over the states of a sparse model.

The states the result is for are recorded in a bit vector, which selects every state of the model unless the result was narrowed down, e.g. by filtering it to the initial states. The truth values are stored compressed, i.e. the i-th truth value belongs to the i-th state selected by that bit vector.

Definition at line 25 of file ExplicitQualitativeCheckResult.h.

Member Typedef Documentation

◆ vector_type

template<typename ValueType>

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

Definition at line 27 of file ExplicitQualitativeCheckResult.h.

Constructor & Destructor Documentation

◆ ExplicitQualitativeCheckResult() [1/6]

template<typename ValueType>

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

Creates a result that holds the given truth value for the given state only.

Definition at line 17 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [2/6]

template<typename ValueType>

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

Creates a result for all states of a model with as many states as the given bit vector has bits.

Definition at line 23 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [3/6]

template<typename ValueType>

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

Definition at line 30 of file ExplicitQualitativeCheckResult.cpp.

◆ ExplicitQualitativeCheckResult() [4/6]

template<typename ValueType>

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

Creates a result for the given states only.

Parameters

states	The states the result is for.
truthValues	One truth value per state selected by `states`, in the order of the selected states.

Definition at line 37 of file ExplicitQualitativeCheckResult.cpp.

◆ ~ExplicitQualitativeCheckResult()

template<typename ValueType>

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

virtualdefault

◆ ExplicitQualitativeCheckResult() [5/6]

template<typename ValueType>

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

default

◆ ExplicitQualitativeCheckResult() [6/6]

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 44 of file ExplicitQualitativeCheckResult.cpp.

◆ complement()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::QualitativeCheckResult.

Definition at line 117 of file ExplicitQualitativeCheckResult.cpp.

◆ count()

template<typename ValueType>

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

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 86 of file ExplicitQualitativeCheckResult.cpp.

◆ existsTrue()

template<typename ValueType>

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

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 76 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 151 of file ExplicitQualitativeCheckResult.cpp.

◆ forallTrue()

template<typename ValueType>

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

overridevirtual

Implements storm::modelchecker::QualitativeCheckResult.

Definition at line 81 of file ExplicitQualitativeCheckResult.cpp.

◆ getScheduler() [1/2]

template<typename ValueType>

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

Definition at line 189 of file ExplicitQualitativeCheckResult.cpp.

◆ getScheduler() [2/2]

template<typename ValueType>

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

Definition at line 183 of file ExplicitQualitativeCheckResult.cpp.

◆ getStates()

template<typename ValueType>

storm::storage::BitVector const & storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::getStates ( ) const

Retrieves the states this result holds truth values for.

Definition at line 107 of file ExplicitQualitativeCheckResult.cpp.

◆ getTruthValuesVector()

template<typename ValueType>

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

Retrieves the truth values, one per state this result is for.

The i-th truth value belongs to the i-th state selected by getStates().

Definition at line 112 of file ExplicitQualitativeCheckResult.cpp.

◆ hasScheduler()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 173 of file ExplicitQualitativeCheckResult.cpp.

◆ hasValueForState()

template<typename ValueType>

bool storm::modelchecker::ExplicitQualitativeCheckResult< ValueType >::hasValueForState ( storm::storage::sparse::state_type state ) const

Retrieves whether the result holds a truth value for the given state.

Definition at line 91 of file ExplicitQualitativeCheckResult.cpp.

◆ isExplicit()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 122 of file ExplicitQualitativeCheckResult.cpp.

◆ isExplicitQualitativeCheckResult()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 132 of file ExplicitQualitativeCheckResult.cpp.

◆ isResultForAllStates()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 127 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 64 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 state ) const

Retrieves the truth value of the given state.

Precondition: The result holds a truth value for that state.

Definition at line 102 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 70 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 178 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::Valuations > const &	stateValuations = std::nullopt,
		std::optional< storm::models::sparse::StateLabeling > const &	stateLabels = std::nullopt ) const

Definition at line 214 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 137 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

◆ vector_type

Constructor & Destructor Documentation

◆ ExplicitQualitativeCheckResult() [1/6]

◆ ExplicitQualitativeCheckResult() [2/6]

◆ ExplicitQualitativeCheckResult() [3/6]

◆ ExplicitQualitativeCheckResult() [4/6]

◆ ~ExplicitQualitativeCheckResult()

◆ ExplicitQualitativeCheckResult() [5/6]

◆ ExplicitQualitativeCheckResult() [6/6]

Member Function Documentation

◆ clone()

◆ complement()

◆ count()

◆ existsTrue()

◆ filter()

◆ forallTrue()

◆ getScheduler() [1/2]

◆ getScheduler() [2/2]

◆ getStates()

◆ getTruthValuesVector()

◆ hasScheduler()

◆ hasValueForState()

◆ isExplicit()

◆ isExplicitQualitativeCheckResult()

◆ isResultForAllStates()

◆ operator&=()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator[]()

◆ operator|=()

◆ setScheduler()

◆ toJson()

◆ writeToStream()