#include <ExplicitQuantitativeCheckResult.h>

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

[legend]

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

[legend]

Public Types
typedef std::vector< ValueType >	vector_type
typedef std::map< storm::storage::sparse::state_type, ValueType >	map_type

Public Member Functions
	ExplicitQuantitativeCheckResult ()
	ExplicitQuantitativeCheckResult (map_type const &values)
	ExplicitQuantitativeCheckResult (map_type &&values)
	ExplicitQuantitativeCheckResult (storm::storage::sparse::state_type const &state, ValueType const &value)
	ExplicitQuantitativeCheckResult (vector_type const &values)
	ExplicitQuantitativeCheckResult (vector_type &&values)
	ExplicitQuantitativeCheckResult (boost::variant< vector_type, map_type > const &values, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	ExplicitQuantitativeCheckResult (boost::variant< vector_type, map_type > &&values, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	ExplicitQuantitativeCheckResult (ExplicitQuantitativeCheckResult const &other)=default
ExplicitQuantitativeCheckResult &	operator= (ExplicitQuantitativeCheckResult const &other)=default
	ExplicitQuantitativeCheckResult (ExplicitQuantitativeCheckResult &&other)=default
ExplicitQuantitativeCheckResult &	operator= (ExplicitQuantitativeCheckResult &&other)=default
	ExplicitQuantitativeCheckResult (ExplicitQualitativeCheckResult< ValueType > const &other)
virtual	~ExplicitQuantitativeCheckResult ()=default
virtual std::unique_ptr< CheckResult >	clone () const override
ValueType &	operator[] (storm::storage::sparse::state_type state)
ValueType const &	operator[] (storm::storage::sparse::state_type state) const
virtual std::unique_ptr< CheckResult >	compareAgainstBound (storm::logic::ComparisonType comparisonType, ValueType const &bound) const override
virtual bool	isExplicit () const override
virtual bool	isResultForAllStates () const override
virtual bool	isExplicitQuantitativeCheckResult () const override
vector_type const &	getValueVector () const
vector_type &	getValueVector ()
map_type const &	getValueMap () const
virtual std::ostream &	writeToStream (std::ostream &out) const override
virtual void	filter (QualitativeCheckResult const &filter) override
	Filters the current result wrt.
virtual void	oneMinus () override
virtual ValueType	getMin () const override
virtual ValueType	getMax () const override
virtual std::pair< ValueType, ValueType >	getMinMax () const
virtual ValueType	average () const override
virtual ValueType	sum () const override
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 ()
storm::json< ValueType >	toJson (std::optional< storm::storage::sparse::StateValuations > const &stateValuations=std::nullopt, std::optional< storm::models::sparse::StateLabeling > const &stateLabels=std::nullopt) const
std::unique_ptr< CheckResult >	compareAgainstBound (storm::logic::ComparisonType comparisonType, storm::RationalFunction const &bound) const
storm::json< storm::RationalFunction >	toJson (std::optional< storm::storage::sparse::StateValuations > const &, std::optional< storm::models::sparse::StateLabeling > const &) const
Public Member Functions inherited from storm::modelchecker::QuantitativeCheckResult< ValueType >
virtual	~QuantitativeCheckResult ()=default
virtual bool	isQuantitative () const override
Public Member Functions inherited from storm::modelchecker::CheckResult
virtual	~CheckResult ()=default
virtual bool	isSymbolic () const
virtual bool	isHybrid () const
virtual bool	isQualitative () const
virtual bool	isParetoCurveCheckResult () const
virtual bool	isLexicographicCheckResult () const
virtual bool	isExplicitQualitativeCheckResult () 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::ExplicitQuantitativeCheckResult< ValueType >

Definition at line 23 of file ExplicitQuantitativeCheckResult.h.

Member Typedef Documentation

◆ map_type

template<typename ValueType>

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

Definition at line 26 of file ExplicitQuantitativeCheckResult.h.

◆ vector_type

template<typename ValueType>

typedef std::vector<ValueType> storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::vector_type

Definition at line 25 of file ExplicitQuantitativeCheckResult.h.

Constructor & Destructor Documentation

◆ ExplicitQuantitativeCheckResult() [1/11]

template<typename ValueType>

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

Definition at line 19 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [2/11]

template<typename ValueType>

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult ( map_type const & values )

Definition at line 24 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [3/11]

template<typename ValueType>

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult ( map_type && values )

Definition at line 29 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [4/11]

template<typename ValueType>

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult	(	storm::storage::sparse::state_type const &	state,
		ValueType const &	value )

Definition at line 34 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [5/11]

template<typename ValueType>

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult ( vector_type const & values )

Definition at line 40 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [6/11]

template<typename ValueType>

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult ( vector_type && values )

Definition at line 45 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [7/11]

template<typename ValueType>

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

Definition at line 50 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [8/11]

template<typename ValueType>

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

Definition at line 57 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [9/11]

template<typename ValueType>

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

default

◆ ExplicitQuantitativeCheckResult() [10/11]

template<typename ValueType>

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

default

◆ ExplicitQuantitativeCheckResult() [11/11]

template<typename ValueType>

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

explicit

Definition at line 64 of file ExplicitQuantitativeCheckResult.cpp.

◆ ~ExplicitQuantitativeCheckResult()

template<typename ValueType>

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

virtualdefault

Member Function Documentation

◆ average()

template<typename ValueType>

ValueType storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::average ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 196 of file ExplicitQuantitativeCheckResult.cpp.

◆ clone()

template<typename ValueType>

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

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 88 of file ExplicitQuantitativeCheckResult.cpp.

◆ compareAgainstBound() [1/2]

std::unique_ptr< CheckResult > storm::modelchecker::ExplicitQuantitativeCheckResult< storm::RationalFunction >::compareAgainstBound	(	storm::logic::ComparisonType	comparisonType,
		storm::RationalFunction const &	bound ) const

Definition at line 404 of file ExplicitQuantitativeCheckResult.cpp.

◆ compareAgainstBound() [2/2]

template<typename ValueType>

std::unique_ptr< CheckResult > storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::compareAgainstBound	(	storm::logic::ComparisonType	comparisonType,
		ValueType const &	bound ) const

overridevirtual

Reimplemented from storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 338 of file ExplicitQuantitativeCheckResult.cpp.

◆ filter()

template<typename ValueType>

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

◆ getMax()

template<typename ValueType>

ValueType storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getMax ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 153 of file ExplicitQuantitativeCheckResult.cpp.

◆ getMin()

template<typename ValueType>

ValueType storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getMin ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 142 of file ExplicitQuantitativeCheckResult.cpp.

◆ getMinMax()

template<typename ValueType>

std::pair< ValueType, ValueType > storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getMinMax ( ) const

virtual

Definition at line 164 of file ExplicitQuantitativeCheckResult.cpp.

◆ getScheduler() [1/2]

template<typename ValueType>

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

Definition at line 234 of file ExplicitQuantitativeCheckResult.cpp.

◆ getScheduler() [2/2]

template<typename ValueType>

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

Definition at line 228 of file ExplicitQuantitativeCheckResult.cpp.

◆ getValueMap()

template<typename ValueType>

ExplicitQuantitativeCheckResult< ValueType >::map_type const & storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getValueMap ( ) const

Definition at line 103 of file ExplicitQuantitativeCheckResult.cpp.

◆ getValueVector() [1/2]

template<typename ValueType>

ExplicitQuantitativeCheckResult< ValueType >::vector_type & storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getValueVector ( )

Definition at line 98 of file ExplicitQuantitativeCheckResult.cpp.

◆ getValueVector() [2/2]

template<typename ValueType>

ExplicitQuantitativeCheckResult< ValueType >::vector_type const & storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getValueVector ( ) const

Definition at line 93 of file ExplicitQuantitativeCheckResult.cpp.

◆ hasScheduler()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 218 of file ExplicitQuantitativeCheckResult.cpp.

◆ isExplicit()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 432 of file ExplicitQuantitativeCheckResult.cpp.

◆ isExplicitQuantitativeCheckResult()

template<typename ValueType>

bool storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::isExplicitQuantitativeCheckResult ( ) const

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 442 of file ExplicitQuantitativeCheckResult.cpp.

◆ isResultForAllStates()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 437 of file ExplicitQuantitativeCheckResult.cpp.

◆ oneMinus()

template<typename ValueType>

void storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::oneMinus ( )

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 447 of file ExplicitQuantitativeCheckResult.cpp.

◆ operator=() [1/2]

template<typename ValueType>

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

default

◆ operator=() [2/2]

template<typename ValueType>

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

default

◆ operator[]() [1/2]

template<typename ValueType>

ValueType & storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::operator[] ( storm::storage::sparse::state_type state )

Definition at line 411 of file ExplicitQuantitativeCheckResult.cpp.

◆ operator[]() [2/2]

template<typename ValueType>

ValueType const & storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::operator[] ( storm::storage::sparse::state_type state ) const

Definition at line 420 of file ExplicitQuantitativeCheckResult.cpp.

◆ setScheduler()

template<typename ValueType>

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

Definition at line 223 of file ExplicitQuantitativeCheckResult.cpp.

◆ sum()

template<typename ValueType>

ValueType storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::sum ( ) const

overridevirtual

Implements storm::modelchecker::QuantitativeCheckResult< ValueType >.

Definition at line 175 of file ExplicitQuantitativeCheckResult.cpp.

◆ toJson() [1/2]

storm::json< storm::RationalFunction > storm::modelchecker::ExplicitQuantitativeCheckResult< storm::RationalFunction >::toJson	(	std::optional< storm::storage::sparse::StateValuations > const &	,
		std::optional< storm::models::sparse::StateLabeling > const &	) const

Definition at line 496 of file ExplicitQuantitativeCheckResult.cpp.

◆ toJson() [2/2]

template<typename ValueType>

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

Definition at line 478 of file ExplicitQuantitativeCheckResult.cpp.

◆ writeToStream()

template<typename ValueType>

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

overridevirtual

Implements storm::modelchecker::CheckResult.

Definition at line 285 of file ExplicitQuantitativeCheckResult.cpp.

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

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

Public Types

Public Member Functions

Detailed Description

Member Typedef Documentation

◆ map_type

◆ vector_type

Constructor & Destructor Documentation

◆ ExplicitQuantitativeCheckResult() [1/11]

◆ ExplicitQuantitativeCheckResult() [2/11]

◆ ExplicitQuantitativeCheckResult() [3/11]

◆ ExplicitQuantitativeCheckResult() [4/11]

◆ ExplicitQuantitativeCheckResult() [5/11]

◆ ExplicitQuantitativeCheckResult() [6/11]

◆ ExplicitQuantitativeCheckResult() [7/11]

◆ ExplicitQuantitativeCheckResult() [8/11]

◆ ExplicitQuantitativeCheckResult() [9/11]

◆ ExplicitQuantitativeCheckResult() [10/11]

◆ ExplicitQuantitativeCheckResult() [11/11]

◆ ~ExplicitQuantitativeCheckResult()

Member Function Documentation

◆ average()

◆ clone()

◆ compareAgainstBound() [1/2]

◆ compareAgainstBound() [2/2]

◆ filter()

◆ getMax()

◆ getMin()

◆ getMinMax()

◆ getScheduler() [1/2]

◆ getScheduler() [2/2]

◆ getValueMap()

◆ getValueVector() [1/2]

◆ getValueVector() [2/2]

◆ hasScheduler()

◆ isExplicit()

◆ isExplicitQuantitativeCheckResult()

◆ isResultForAllStates()

◆ oneMinus()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator[]() [1/2]

◆ operator[]() [2/2]

◆ setScheduler()

◆ sum()

◆ toJson() [1/2]

◆ toJson() [2/2]

◆ writeToStream()