Storm: storm::dd::bisimulation::Partition< DdType, ValueType > Class Template Reference

Storm

A Modern Probabilistic Model Checker

Loading...

Searching...

No Matches

#include <Partition.h>

Public Member Functions
	Partition ()

bool	operator== (Partition< DdType, ValueType > const &other) const

Partition< DdType, ValueType >	replacePartition (storm::dd::Add< DdType, ValueType > const &newPartitionAdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional< storm::dd::Add< DdType, ValueType > > const &changedStates=boost::none) const

Partition< DdType, ValueType >	replacePartition (storm::dd::Bdd< DdType > const &newPartitionBdd, uint64_t numberOfBlocks, uint64_t nextFreeBlockIndex, boost::optional< storm::dd::Bdd< DdType > > const &changedStates=boost::none) const

uint64_t	getNumberOfStates () const

uint64_t	getNumberOfBlocks () const

bool	storedAsAdd () const

bool	storedAsBdd () const

storm::dd::Add< DdType, ValueType > const &	asAdd () const

storm::dd::Bdd< DdType > const &	asBdd () const

std::pair< storm::expressions::Variable, storm::expressions::Variable > const &	getBlockVariables () const

storm::expressions::Variable const &	getBlockVariable () const

storm::expressions::Variable const &	getPrimedBlockVariable () const

uint64_t	getNextFreeBlockIndex () const

uint64_t	getNodeCount () const

storm::dd::Bdd< DdType >	getStates () const

bool	hasChangedStates () const
	Retrieves whether this partition has information about the states whose partition block assignment changed.

storm::dd::Add< DdType, ValueType > const &	changedStatesAsAdd () const
	Retrieves the DD representing the states whose partition block assignment changed.

storm::dd::Bdd< DdType > const &	changedStatesAsBdd () const

Static Public Member Functions
static Partition	create (storm::models::symbolic::Model< DdType, ValueType > const &model, storm::storage::BisimulationType const &bisimulationType, PreservationInformation< DdType, ValueType > const &preservationInformation)

static Partition	create (storm::models::symbolic::Model< DdType, ValueType > const &model, storm::storage::BisimulationType const &bisimulationType, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas)

static Partition	createTrivialChoicePartition (storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &model, std::pair< storm::expressions::Variable, storm::expressions::Variable > const &blockVariables)

Detailed Description

template<storm::dd::DdType DdType, typename ValueType>
class storm::dd::bisimulation::Partition< DdType, ValueType >

Definition at line 28 of file Partition.h.

Constructor & Destructor Documentation

◆ Partition()

template<storm::dd::DdType DdType, typename ValueType >

storm::dd::bisimulation::Partition< DdType, ValueType >::Partition ( )

Definition at line 32 of file Partition.cpp.

Member Function Documentation

◆ asAdd()

template<storm::dd::DdType DdType, typename ValueType >

storm::dd::Add< DdType, ValueType > const & storm::dd::bisimulation::Partition< DdType, ValueType >::asAdd ( ) const

Definition at line 307 of file Partition.cpp.

◆ asBdd()

template<storm::dd::DdType DdType, typename ValueType >

storm::dd::Bdd< DdType > const & storm::dd::bisimulation::Partition< DdType, ValueType >::asBdd ( ) const

Definition at line 312 of file Partition.cpp.

◆ changedStatesAsAdd()

template<storm::dd::DdType DdType, typename ValueType >

storm::dd::Add< DdType, ValueType > const & storm::dd::bisimulation::Partition< DdType, ValueType >::changedStatesAsAdd ( ) const

Retrieves the DD representing the states whose partition block assignment changed.

Definition at line 282 of file Partition.cpp.

◆ changedStatesAsBdd()

template<storm::dd::DdType DdType, typename ValueType >

storm::dd::Bdd< DdType > const & storm::dd::bisimulation::Partition< DdType, ValueType >::changedStatesAsBdd ( ) const

Definition at line 287 of file Partition.cpp.

◆ create() [1/2]

template<storm::dd::DdType DdType, typename ValueType >

Partition< DdType, ValueType > storm::dd::bisimulation::Partition< DdType, ValueType >::create	(	storm::models::symbolic::Model< DdType, ValueType > const &	model,
		storm::storage::BisimulationType const &	bisimulationType,
		PreservationInformation< DdType, ValueType > const &	preservationInformation
	)

static

Definition at line 127 of file Partition.cpp.

◆ create() [2/2]

template<storm::dd::DdType DdType, typename ValueType >

Partition< DdType, ValueType > storm::dd::bisimulation::Partition< DdType, ValueType >::create	(	storm::models::symbolic::Model< DdType, ValueType > const &	model,
		storm::storage::BisimulationType const &	bisimulationType,
		std::vector< std::shared_ptr< storm::logic::Formula const > > const &	formulas
	)

static

Definition at line 109 of file Partition.cpp.

◆ createTrivialChoicePartition()

template<storm::dd::DdType DdType, typename ValueType >

Partition< DdType, ValueType > storm::dd::bisimulation::Partition< DdType, ValueType >::createTrivialChoicePartition	(	storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &	model,
		std::pair< storm::expressions::Variable, storm::expressions::Variable > const &	blockVariables
	)

static

Definition at line 248 of file Partition.cpp.

◆ getBlockVariable()

template<storm::dd::DdType DdType, typename ValueType >

storm::expressions::Variable const & storm::dd::bisimulation::Partition< DdType, ValueType >::getBlockVariable ( ) const

Definition at line 322 of file Partition.cpp.

◆ getBlockVariables()

template<storm::dd::DdType DdType, typename ValueType >

std::pair< storm::expressions::Variable, storm::expressions::Variable > const & storm::dd::bisimulation::Partition< DdType, ValueType >::getBlockVariables ( ) const

Definition at line 317 of file Partition.cpp.

◆ getNextFreeBlockIndex()

template<storm::dd::DdType DdType, typename ValueType >

uint64_t storm::dd::bisimulation::Partition< DdType, ValueType >::getNextFreeBlockIndex ( ) const

Definition at line 332 of file Partition.cpp.

◆ getNodeCount()

template<storm::dd::DdType DdType, typename ValueType >

uint64_t storm::dd::bisimulation::Partition< DdType, ValueType >::getNodeCount ( ) const

Definition at line 337 of file Partition.cpp.

◆ getNumberOfBlocks()

template<storm::dd::DdType DdType, typename ValueType >

uint64_t storm::dd::bisimulation::Partition< DdType, ValueType >::getNumberOfBlocks ( ) const

Definition at line 292 of file Partition.cpp.

◆ getNumberOfStates()

template<storm::dd::DdType DdType, typename ValueType >

uint64_t storm::dd::bisimulation::Partition< DdType, ValueType >::getNumberOfStates ( ) const

Definition at line 263 of file Partition.cpp.

◆ getPrimedBlockVariable()

template<storm::dd::DdType DdType, typename ValueType >

storm::expressions::Variable const & storm::dd::bisimulation::Partition< DdType, ValueType >::getPrimedBlockVariable ( ) const

Definition at line 327 of file Partition.cpp.

◆ getStates()

template<storm::dd::DdType DdType, typename ValueType >

storm::dd::Bdd< DdType > storm::dd::bisimulation::Partition< DdType, ValueType >::getStates ( ) const

Definition at line 268 of file Partition.cpp.

◆ hasChangedStates()

template<storm::dd::DdType DdType, typename ValueType >

bool storm::dd::bisimulation::Partition< DdType, ValueType >::hasChangedStates ( ) const

Retrieves whether this partition has information about the states whose partition block assignment changed.

Definition at line 277 of file Partition.cpp.

◆ operator==()

template<storm::dd::DdType DdType, typename ValueType >

bool storm::dd::bisimulation::Partition< DdType, ValueType >::operator== ( Partition< DdType, ValueType > const & other ) const

Definition at line 61 of file Partition.cpp.

◆ replacePartition() [1/2]

template<storm::dd::DdType DdType, typename ValueType >

Partition< DdType, ValueType > storm::dd::bisimulation::Partition< DdType, ValueType >::replacePartition	(	storm::dd::Add< DdType, ValueType > const &	newPartitionAdd,
		uint64_t	numberOfBlocks,
		uint64_t	nextFreeBlockIndex,
		boost::optional< storm::dd::Add< DdType, ValueType > > const &	changedStates = `boost::none`
	)		const

Definition at line 67 of file Partition.cpp.

◆ replacePartition() [2/2]

template<storm::dd::DdType DdType, typename ValueType >

Partition< DdType, ValueType > storm::dd::bisimulation::Partition< DdType, ValueType >::replacePartition	(	storm::dd::Bdd< DdType > const &	newPartitionBdd,
		uint64_t	numberOfBlocks,
		uint64_t	nextFreeBlockIndex,
		boost::optional< storm::dd::Bdd< DdType > > const &	changedStates = `boost::none`
	)		const

Definition at line 74 of file Partition.cpp.

◆ storedAsAdd()

template<storm::dd::DdType DdType, typename ValueType >

bool storm::dd::bisimulation::Partition< DdType, ValueType >::storedAsAdd ( ) const

Definition at line 297 of file Partition.cpp.

◆ storedAsBdd()

template<storm::dd::DdType DdType, typename ValueType >

bool storm::dd::bisimulation::Partition< DdType, ValueType >::storedAsBdd ( ) const

Definition at line 302 of file Partition.cpp.

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

src/storm/storage/dd/bisimulation/InternalCuddSignatureRefiner.h
src/storm/storage/dd/bisimulation/Partition.h
src/storm/storage/dd/bisimulation/Partition.cpp

storm
dd
bisimulation
Partition
Generated by 1.9.8