storm::bisimulation::QuotientData< ValueType > Struct Template Reference

The index mappings between an input model and its bisimulation quotient, derived from a partition of the input model's states. More...

#include <QuotientData.h>

Classes
struct	SignatureData

Public Member Functions
	QuotientData (storm::bisimulation::Partition const &partition, storm::OptionalRef< storm::storage::BitVector const > preferredRepresentatives=storm::NullRef)
	Computes the state index mappings between the states (i.e., the elements of the given partition) and the quotient described by the partition.

Public Attributes
std::vector< uint64_t >	toQuotientState
std::vector< uint64_t >	toRepresentativeState
std::optional< std::vector< uint64_t > >	toQuotientChoice
std::optional< SignatureData >	signatureData
std::optional< WeakBisimulationData >	weakData

Detailed Description

template<typename ValueType>
struct storm::bisimulation::QuotientData< ValueType >

The index mappings between an input model and its bisimulation quotient, derived from a partition of the input model's states.

Definition at line 20 of file QuotientData.h.

Constructor & Destructor Documentation

QuotientData()

template<typename ValueType>

storm::bisimulation::QuotientData< ValueType >::QuotientData	(	storm::bisimulation::Partition const &	partition,
		storm::OptionalRef< storm::storage::BitVector const >	preferredRepresentatives = storm::NullRef )

Computes the state index mappings between the states (i.e., the elements of the given partition) and the quotient described by the partition.

Quotient states are numbered in the order of the smallest state of their block.

Parameters

preferredRepresentatives

if given, the representative of a block is picked among these states whenever the block contains such a state. Otherwise, the first state of the block (cf. Partition::Block) is its representative.

Note

does not compute any choice mappings, cf. below.

Definition at line 13 of file QuotientData.cpp.

Member Data Documentation

signatureData

template<typename ValueType>

std::optional<SignatureData> storm::bisimulation::QuotientData< ValueType >::signatureData

Definition at line 47 of file QuotientData.h.

toQuotientChoice

template<typename ValueType>

std::optional<std::vector<uint64_t> > storm::bisimulation::QuotientData< ValueType >::toQuotientChoice

Definition at line 34 of file QuotientData.h.

toQuotientState

template<typename ValueType>

std::vector<uint64_t> storm::bisimulation::QuotientData< ValueType >::toQuotientState

Definition at line 31 of file QuotientData.h.

toRepresentativeState

template<typename ValueType>

std::vector<uint64_t> storm::bisimulation::QuotientData< ValueType >::toRepresentativeState

Definition at line 32 of file QuotientData.h.

weakData

template<typename ValueType>

std::optional<WeakBisimulationData> storm::bisimulation::QuotientData< ValueType >::weakData

Definition at line 50 of file QuotientData.h.

---

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

• src/storm/transformer/bisimulation/QuotientData.h
• src/storm/transformer/bisimulation/QuotientData.cpp