storm::bisimulation::Signatures< ValueType, Mode > Class Template Reference

Computes and caches the state signatures and provides state-based order / condition for splitting in signature refinement. More...

#include <Signatures.h>

Classes
class	SplitOrder
	Represents a strict weak order over state indices based on their signature. More...
struct	SplitCondition
	Represents a condition for splitting two states based on their signature. More...

Public Member Functions
	Signatures (storm::models::sparse::Model< ValueType > const &model, std::optional< std::vector< uint64_t > > const &choiceClasses, storm::bisimulation::Partition const &partition)
	Signatures (storm::models::sparse::Model< ValueType > const &model, std::optional< std::vector< uint64_t > > const &choiceClasses, storm::bisimulation::Partition const &partition, ValueType const &tolerance)
void	updateStateSignature (uint64_t const stateIndex)
	Updates the state signature of the given state index.
SplitOrder	getEquivalenceSplitOrder () const
	Instantiates a SplitOrder whose ties exactly coincide with true signature equality (operator==).
SplitOrder	getStructuralSplitOrder () const
	Instantiates a SplitOrder that only compares with respect to structural equality of the state signature (ChoiceSignature::compareStructure).
SplitCondition	getApproximateSplitCondition () const
	Instantiates a SplitCondition.
void	extendQuotientData (QuotientData< ValueType > &quotientData, bool const createQuotientChoiceMapping) const
	Fills in the choice mappings of the given (already state-mapped) quotient data: for every quotient state, the choices of its representative state are deduplicated (exactly or up to tolerance, depending on Mode) into the quotient choices.

Detailed Description

template<typename ValueType, SignatureMode Mode>
class storm::bisimulation::Signatures< ValueType, Mode >

Computes and caches the state signatures and provides state-based order / condition for splitting in signature refinement.

Template Parameters

ValueType	the type of the transition values in the model
Mode	the mode of the signature computation (exact or approximate)

Definition at line 24 of file Signatures.h.

Constructor & Destructor Documentation

Signatures() [1/2]

template<typename ValueType, SignatureMode Mode>
requires (Mode == SignatureMode::Exact)

storm::bisimulation::Signatures< ValueType, Mode >::Signatures	(	storm::models::sparse::Model< ValueType > const &	model,
		std::optional< std::vector< uint64_t > > const &	choiceClasses,
		storm::bisimulation::Partition const &	partition )

Definition at line 258 of file Signatures.cpp.

Signatures() [2/2]

template<typename ValueType, SignatureMode Mode>
requires (Mode == SignatureMode::Approximative)

storm::bisimulation::Signatures< ValueType, Mode >::Signatures	(	storm::models::sparse::Model< ValueType > const &	model,
		std::optional< std::vector< uint64_t > > const &	choiceClasses,
		storm::bisimulation::Partition const &	partition,
		ValueType const &	tolerance )

Definition at line 270 of file Signatures.cpp.

Member Function Documentation

extendQuotientData()

template<typename ValueType, SignatureMode Mode>

void storm::bisimulation::Signatures< ValueType, Mode >::extendQuotientData	(	QuotientData< ValueType > &	quotientData,
		bool const	createQuotientChoiceMapping ) const

Fills in the choice mappings of the given (already state-mapped) quotient data: for every quotient state, the choices of its representative state are deduplicated (exactly or up to tolerance, depending on Mode) into the quotient choices.

Parameters

createQuotientChoiceMapping

if set, every original model choice is additionally mapped to the quotient choice that represents it (SignatureData::toQuotientChoice). For each original model state, this mapping is surjective onto the choices of the corresponding quotient state, so that, e.g., a scheduler for the quotient can be translated back to the original model. If not set, that (comparatively expensive) mapping remains empty.

Exceptions

UnexpectedException

if the choices of a state cannot be related to the choices of the state representing it in the quotient, which can happen in approximative mode since approximate equality is not transitive.

Definition at line 463 of file Signatures.cpp.

getApproximateSplitCondition()

template<typename ValueType, SignatureMode Mode>

auto storm::bisimulation::Signatures< ValueType, Mode >::getApproximateSplitCondition

(

)

const

Instantiates a SplitCondition.

Definition at line 368 of file Signatures.cpp.

getEquivalenceSplitOrder()

template<typename ValueType, SignatureMode Mode>

auto storm::bisimulation::Signatures< ValueType, Mode >::getEquivalenceSplitOrder

(

)

const

Instantiates a SplitOrder whose ties exactly coincide with true signature equality (operator==).

Definition at line 329 of file Signatures.cpp.

getStructuralSplitOrder()

template<typename ValueType, SignatureMode Mode>

auto storm::bisimulation::Signatures< ValueType, Mode >::getStructuralSplitOrder

(

)

const

Instantiates a SplitOrder that only compares with respect to structural equality of the state signature (ChoiceSignature::compareStructure).

Definition at line 336 of file Signatures.cpp.

updateStateSignature()

template<typename ValueType, SignatureMode Mode>

void storm::bisimulation::Signatures< ValueType, Mode >::updateStateSignature

(

uint64_t const

stateIndex

)

Updates the state signature of the given state index.

Parameters

stateIndex

Definition at line 320 of file Signatures.cpp.

---

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

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