#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, boost::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler=boost::none)

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

	ExplicitQuantitativeCheckResult (ExplicitQuantitativeCheckResult const &other)=default

ExplicitQuantitativeCheckResult &	operator= (ExplicitQuantitativeCheckResult const &other)=default

	ExplicitQuantitativeCheckResult (ExplicitQuantitativeCheckResult &&other)=default

ExplicitQuantitativeCheckResult &	operator= (ExplicitQuantitativeCheckResult &&other)=default

	ExplicitQuantitativeCheckResult (ExplicitQualitativeCheckResult 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

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

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

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,
		boost::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > >	scheduler = `boost::none`
	)

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,
		boost::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > >	scheduler = `boost::none`
	)

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

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 337 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 152 of file ExplicitQuantitativeCheckResult.cpp.

◆ getMin()

template<typename ValueType >

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

overridevirtual

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

Definition at line 141 of file ExplicitQuantitativeCheckResult.cpp.

◆ getMinMax()

template<typename ValueType >

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

virtual

Definition at line 163 of file ExplicitQuantitativeCheckResult.cpp.

◆ getScheduler() [1/2]

template<typename ValueType >

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

Definition at line 233 of file ExplicitQuantitativeCheckResult.cpp.

◆ getScheduler() [2/2]

template<typename ValueType >

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

Definition at line 227 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 217 of file ExplicitQuantitativeCheckResult.cpp.

◆ isExplicit()

template<typename ValueType >

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 433 of file ExplicitQuantitativeCheckResult.cpp.

◆ isExplicitQuantitativeCheckResult()

template<typename ValueType >

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 443 of file ExplicitQuantitativeCheckResult.cpp.

◆ isResultForAllStates()

template<typename ValueType >

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 438 of file ExplicitQuantitativeCheckResult.cpp.

◆ oneMinus()

template<typename ValueType >

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

overridevirtual

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

Definition at line 448 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 412 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 421 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 222 of file ExplicitQuantitativeCheckResult.cpp.

◆ sum()

template<typename ValueType >

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

overridevirtual

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

Definition at line 174 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 497 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 479 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 284 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()

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