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

#include <ExplicitQuantitativeCheckResult.h>

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

[legend]

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

[legend]

Public Types
typedef QuantitativeCheckResult< ValueType >::ExtendedValueType	ExtendedValueType
typedef std::vector< ExtendedValueType >	vector_type
Public Types inherited from storm::modelchecker::QuantitativeCheckResult< ValueType >
typedef storm::utility::ExtendedValueType< ValueType >	ExtendedValueType

Public Member Functions
	ExplicitQuantitativeCheckResult (storm::storage::sparse::state_type const &state, ExtendedValueType const &value)
	Creates a result that holds the given value for the given state only.
	ExplicitQuantitativeCheckResult (vector_type const &values, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	Creates a result for all states of a model with the given number of states.
	ExplicitQuantitativeCheckResult (vector_type &&values, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	ExplicitQuantitativeCheckResult (storm::storage::BitVector states, vector_type &&values, std::optional< std::shared_ptr< storm::storage::Scheduler< ValueType > > > scheduler={})
	Creates a result for the given states only.
	ExplicitQuantitativeCheckResult (std::vector< ValueType > const &values)
	Takes over values that are still expressed in the plain value type, which are taken to be finite.
	ExplicitQuantitativeCheckResult (std::vector< ValueType > &&values)
	ExplicitQuantitativeCheckResult (storm::storage::BitVector states, std::vector< ValueType > &&values)
	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
ExtendedValueType &	operator[] (storm::storage::sparse::state_type state)
	Retrieves the value of the given state.
ExtendedValueType 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
bool	hasValueForState (storm::storage::sparse::state_type state) const
	Retrieves whether the result holds a value for the given state.
storm::storage::BitVector const &	getStates () const
	Retrieves the states this result holds values for.
vector_type const &	getValueVector () const
	Retrieves the values, one per state this result is for.
vector_type &	getValueVector ()
std::vector< ValueType >	getFiniteValueVector () const
std::vector< ValueType >	getSentinelValueVector () const
bool	hasLowerBounds () const
	Retrieves whether sound lower resp.
bool	hasUpperBounds () const
vector_type const &	getLowerBoundVector () const
	Retrieves the sound lower resp.
vector_type const &	getUpperBoundVector () const
storm::solver::SolutionBounds< ExtendedValueType > const &	getSolutionBounds () const
	Retrieves both bounds at once, either of which may be unset.
void	setLowerBounds (vector_type lowerBounds)
	Sets sound bounds on the actual values.
void	setUpperBounds (vector_type upperBounds)
void	setBounds (storm::solver::SolutionBounds< ExtendedValueType > bounds)
void	setBounds (storm::solver::SolutionBounds< ValueType > bounds)
	Sets bounds that are still expressed in the plain value type, which are taken to be finite.
void	setValuesExact ()
	States that the values of this result are the exact ones, i.e.
void	clearBounds ()
	Drops all bounds, e.g.
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 ExtendedValueType	getMin () const override
virtual ExtendedValueType	getMax () const override
virtual std::pair< ExtendedValueType, ExtendedValueType >	getMinMax () const
virtual ExtendedValueType	average () const override
virtual ExtendedValueType	sum () const override
virtual AggregatedValue< ExtendedValueType >	aggregate (FilterType filter) const override
	Aggregates the values of this result with the given filter, and each bound it carries alongside.
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::Valuations > 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::Valuations > 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 >

A quantitative 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 values are stored compressed, i.e. the i-th value belongs to the i-th state selected by that bit vector.

Definition at line 30 of file ExplicitQuantitativeCheckResult.h.

Member Typedef Documentation

◆ ExtendedValueType

template<typename ValueType>

typedef QuantitativeCheckResult<ValueType>::ExtendedValueType storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExtendedValueType

Definition at line 32 of file ExplicitQuantitativeCheckResult.h.

◆ vector_type

template<typename ValueType>

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

Definition at line 33 of file ExplicitQuantitativeCheckResult.h.

Constructor & Destructor Documentation

◆ ExplicitQuantitativeCheckResult() [1/10]

template<typename ValueType>

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

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

Definition at line 20 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [2/10]

template<typename ValueType>

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

Creates a result for all states of a model with the given number of states.

Definition at line 26 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [3/10]

template<typename ValueType>

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

Definition at line 33 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [4/10]

template<typename ValueType>

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult	(	storm::storage::BitVector	states,
		vector_type &&	values,
		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.
values	One value per state selected by `states`, in the order of the selected states.

Definition at line 40 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [5/10]

template<typename ValueType>
requires (!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>)

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

Takes over values that are still expressed in the plain value type, which are taken to be finite.

A computation that can produce an infinite value hands over the extended type instead.

Definition at line 47 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [6/10]

template<typename ValueType>
requires (!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>)

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult ( std::vector< ValueType > && values )

Definition at line 54 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [7/10]

template<typename ValueType>
requires (!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>)

storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::ExplicitQuantitativeCheckResult	(	storm::storage::BitVector	states,
		std::vector< ValueType > &&	values )

Definition at line 61 of file ExplicitQuantitativeCheckResult.cpp.

◆ ExplicitQuantitativeCheckResult() [8/10]

template<typename ValueType>

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

default

◆ ExplicitQuantitativeCheckResult() [9/10]

template<typename ValueType>

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

default

◆ ExplicitQuantitativeCheckResult() [10/10]

template<typename ValueType>

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

explicit

Definition at line 68 of file ExplicitQuantitativeCheckResult.cpp.

◆ ~ExplicitQuantitativeCheckResult()

template<typename ValueType>

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

virtualdefault

Member Function Documentation

◆ aggregate()

template<typename ValueType>

AggregatedValue< typename ExplicitQuantitativeCheckResult< ValueType >::ExtendedValueType > storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::aggregate ( FilterType filter ) const

overridevirtual

Aggregates the values of this result with the given filter, and each bound it carries alongside.

Every aggregation offered here is monotone in each value, so aggregating a bound bounds the aggregate.

Parameters

filter One of MIN, MAX, SUM or AVG.

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

Definition at line 309 of file ExplicitQuantitativeCheckResult.cpp.

◆ average()

template<typename ValueType>

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

overridevirtual

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

Definition at line 256 of file ExplicitQuantitativeCheckResult.cpp.

◆ clearBounds()

template<typename ValueType>

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

Drops all bounds, e.g.

after an operation that cannot maintain them.

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 80 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 509 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 472 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 200 of file ExplicitQuantitativeCheckResult.cpp.

◆ getFiniteValueVector()

template<typename ValueType>

std::vector< ValueType > storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getFiniteValueVector ( ) const

Precondition: no value is infinite

Returns: the values, narrowed back to the plain value type.

Definition at line 111 of file ExplicitQuantitativeCheckResult.cpp.

◆ getLowerBoundVector()

template<typename ValueType>

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

Retrieves the sound lower resp.

upper bounds on the actual values. These have the same shape as the values, i.e. they are indexed in the same way.

Precondition: The respective bounds are known.

Definition at line 140 of file ExplicitQuantitativeCheckResult.cpp.

◆ getMax()

template<typename ValueType>

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

overridevirtual

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

Definition at line 237 of file ExplicitQuantitativeCheckResult.cpp.

◆ getMin()

template<typename ValueType>

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

overridevirtual

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

Definition at line 231 of file ExplicitQuantitativeCheckResult.cpp.

◆ getMinMax()

template<typename ValueType>

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

virtual

Definition at line 244 of file ExplicitQuantitativeCheckResult.cpp.

◆ getScheduler() [1/2]

template<typename ValueType>

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

Definition at line 338 of file ExplicitQuantitativeCheckResult.cpp.

◆ getScheduler() [2/2]

template<typename ValueType>

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

Definition at line 332 of file ExplicitQuantitativeCheckResult.cpp.

◆ getSentinelValueVector()

template<typename ValueType>

std::vector< ValueType > storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getSentinelValueVector ( ) const

Returns: the values, with every infinite one written as the value that storm::utility::infinity yields for the plain value type.

Definition at line 116 of file ExplicitQuantitativeCheckResult.cpp.

◆ getSolutionBounds()

template<typename ValueType>

storm::solver::SolutionBounds< typename ExplicitQuantitativeCheckResult< ValueType >::ExtendedValueType > const & storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::getSolutionBounds ( ) const

Retrieves both bounds at once, either of which may be unset.

Definition at line 153 of file ExplicitQuantitativeCheckResult.cpp.

◆ getStates()

template<typename ValueType>

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

Retrieves the states this result holds values for.

Definition at line 96 of file ExplicitQuantitativeCheckResult.cpp.

◆ getUpperBoundVector()

template<typename ValueType>

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

Definition at line 146 of file ExplicitQuantitativeCheckResult.cpp.

◆ getValueVector() [1/2]

template<typename ValueType>

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

Definition at line 106 of file ExplicitQuantitativeCheckResult.cpp.

◆ getValueVector() [2/2]

template<typename ValueType>

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

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

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

Definition at line 101 of file ExplicitQuantitativeCheckResult.cpp.

◆ hasLowerBounds()

template<typename ValueType>

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

Retrieves whether sound lower resp.

upper bounds on the actual values are known.

Definition at line 130 of file ExplicitQuantitativeCheckResult.cpp.

◆ hasScheduler()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 322 of file ExplicitQuantitativeCheckResult.cpp.

◆ hasUpperBounds()

template<typename ValueType>

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

Definition at line 135 of file ExplicitQuantitativeCheckResult.cpp.

◆ hasValueForState()

template<typename ValueType>

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

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

Definition at line 85 of file ExplicitQuantitativeCheckResult.cpp.

◆ isExplicit()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 528 of file ExplicitQuantitativeCheckResult.cpp.

◆ isExplicitQuantitativeCheckResult()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 538 of file ExplicitQuantitativeCheckResult.cpp.

◆ isResultForAllStates()

template<typename ValueType>

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

overridevirtual

Reimplemented from storm::modelchecker::CheckResult.

Definition at line 533 of file ExplicitQuantitativeCheckResult.cpp.

◆ oneMinus()

template<typename ValueType>

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

overridevirtual

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

Definition at line 543 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>

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

Retrieves the value of the given state.

Precondition: The result holds a value for that state.

Definition at line 516 of file ExplicitQuantitativeCheckResult.cpp.

◆ operator[]() [2/2]

template<typename ValueType>

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

Definition at line 522 of file ExplicitQuantitativeCheckResult.cpp.

◆ setBounds() [1/2]

template<typename ValueType>

void storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::setBounds ( storm::solver::SolutionBounds< ExtendedValueType > bounds )

Definition at line 170 of file ExplicitQuantitativeCheckResult.cpp.

◆ setBounds() [2/2]

template<typename ValueType>
requires (!std::is_same_v<storm::utility::ExtendedValueType<ValueType>, ValueType>)

void storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::setBounds ( storm::solver::SolutionBounds< ValueType > bounds )

Sets bounds that are still expressed in the plain value type, which are taken to be finite.

An algorithm that can bound a value by infinity hands over the extended type instead.

Definition at line 176 of file ExplicitQuantitativeCheckResult.cpp.

◆ setLowerBounds()

template<typename ValueType>

void storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::setLowerBounds ( vector_type lowerBounds )

Sets sound bounds on the actual values.

Each bound must have the same shape as the values, i.e. hold one entry per state this result is for.

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

◆ setUpperBounds()

template<typename ValueType>

void storm::modelchecker::ExplicitQuantitativeCheckResult< ValueType >::setUpperBounds ( vector_type upperBounds )

Definition at line 164 of file ExplicitQuantitativeCheckResult.cpp.

◆ setValuesExact()

template<typename ValueType>

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

States that the values of this result are the exact ones, i.e.

bounds each of them by itself.

Definition at line 190 of file ExplicitQuantitativeCheckResult.cpp.

◆ sum()

template<typename ValueType>

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

overridevirtual

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

Definition at line 250 of file ExplicitQuantitativeCheckResult.cpp.

◆ toJson() [1/2]

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

Definition at line 612 of file ExplicitQuantitativeCheckResult.cpp.

◆ toJson() [2/2]

template<typename ValueType>

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

Definition at line 598 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 439 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

◆ ExtendedValueType

◆ vector_type

Constructor & Destructor Documentation

◆ ExplicitQuantitativeCheckResult() [1/10]

◆ ExplicitQuantitativeCheckResult() [2/10]

◆ ExplicitQuantitativeCheckResult() [3/10]

◆ ExplicitQuantitativeCheckResult() [4/10]

◆ ExplicitQuantitativeCheckResult() [5/10]

◆ ExplicitQuantitativeCheckResult() [6/10]

◆ ExplicitQuantitativeCheckResult() [7/10]

◆ ExplicitQuantitativeCheckResult() [8/10]

◆ ExplicitQuantitativeCheckResult() [9/10]

◆ ExplicitQuantitativeCheckResult() [10/10]

◆ ~ExplicitQuantitativeCheckResult()

Member Function Documentation

◆ aggregate()

◆ average()

◆ clearBounds()

◆ clone()

◆ compareAgainstBound() [1/2]

◆ compareAgainstBound() [2/2]

◆ filter()

◆ getFiniteValueVector()

◆ getLowerBoundVector()

◆ getMax()

◆ getMin()

◆ getMinMax()

◆ getScheduler() [1/2]

◆ getScheduler() [2/2]

◆ getSentinelValueVector()

◆ getSolutionBounds()

◆ getStates()

◆ getUpperBoundVector()

◆ getValueVector() [1/2]

◆ getValueVector() [2/2]

◆ hasLowerBounds()

◆ hasScheduler()

◆ hasUpperBounds()

◆ hasValueForState()

◆ isExplicit()

◆ isExplicitQuantitativeCheckResult()

◆ isResultForAllStates()

◆ oneMinus()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ operator[]() [1/2]

◆ operator[]() [2/2]

◆ setBounds() [1/2]

◆ setBounds() [2/2]

◆ setLowerBounds()

◆ setScheduler()

◆ setUpperBounds()

◆ setValuesExact()

◆ sum()

◆ toJson() [1/2]

◆ toJson() [2/2]

◆ writeToStream()