storm::bisimulation::Initialization< ValueType > Class Template Reference

#include <Initialization.h>

Public Member Functions
	Initialization (storm::models::sparse::Model< ValueType > const &model, Options const &options, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)
PreservationInformation	getPreservationInformation () const
std::optional< std::vector< uint64_t > >	getChoiceClasses () const
Partition	getInitialStatePartition (std::optional< std::vector< uint64_t > > const &choiceClasses={}) const
WeakBisimulationData	getWeakBisimulationData (Partition &partition, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, PreservationInformation const &preservationInformation) const
	Computes the state-level information that weak bisimulation requires on top of the partition, and refines the given (initial) partition so that it becomes homogeneous with respect to that information.

Detailed Description

template<typename ValueType>
class storm::bisimulation::Initialization< ValueType >

Definition at line 24 of file Initialization.h.

Constructor & Destructor Documentation

Initialization()

template<typename ValueType>

storm::bisimulation::Initialization< ValueType >::Initialization	(	storm::models::sparse::Model< ValueType > const &	model,
		Options const &	options,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas )

Definition at line 88 of file Initialization.cpp.

Member Function Documentation

getChoiceClasses()

template<typename ValueType>

std::optional< std::vector< uint64_t > > storm::bisimulation::Initialization< ValueType >::getChoiceClasses

(

)

const

Definition at line 286 of file Initialization.cpp.

getInitialStatePartition()

template<typename ValueType>

Partition storm::bisimulation::Initialization< ValueType >::getInitialStatePartition

(

std::optional< std::vector< uint64_t > > const &

choiceClasses = {}

)

const

Definition at line 326 of file Initialization.cpp.

getPreservationInformation()

template<typename ValueType>

PreservationInformation storm::bisimulation::Initialization< ValueType >::getPreservationInformation

(

)

const

Definition at line 36 of file Initialization.cpp.

getWeakBisimulationData()

template<typename ValueType>

WeakBisimulationData storm::bisimulation::Initialization< ValueType >::getWeakBisimulationData	(	Partition &	partition,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		PreservationInformation const &	preservationInformation ) const

Computes the state-level information that weak bisimulation requires on top of the partition, and refines the given (initial) partition so that it becomes homogeneous with respect to that information.

Parameters

partition	the initial partition, which already has to respect the preserved annotations. Is split so that no block contains both divergent and non-divergent states.
backwardTransitions	the transposed transition matrix of the model.
preservationInformation	what the minimization has to preserve, cf. getPreservationInformation.

Note

only applicable to deterministic models and if weak bisimulation was requested.

Definition at line 413 of file Initialization.cpp.

---

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

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