#include <PartitionRefiner.h>

Inheritance diagram for storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >:

Public Member Functions
	PartitionRefiner (storm::models::symbolic::Model< DdType, ValueType > const &model, Partition< DdType, ValueType > const &initialStatePartition)
virtual	~PartitionRefiner ()=default
virtual bool	refine (SignatureMode const &mode=SignatureMode::Eager)
	Refines the partition.
bool	refineWrtRewardModel (storm::models::symbolic::StandardRewardModel< DdType, ValueType > const &rewardModel)
	Refines the partition wrt.
Partition< DdType, ValueType > const &	getStatePartition () const
	Retrieves the current state partition in the refinement process.
Signature< DdType, ValueType >	getFullSignature () const
	Retrieves the full signature of all states wrt.
Status	getStatus () const
	Retrieves the status of the refinement process.
std::chrono::high_resolution_clock::duration	getTotalSignatureTime () const
std::chrono::high_resolution_clock::duration	getTotalRefinementTime () const

Protected Member Functions
Partition< DdType, ValueType >	internalRefine (SignatureComputer< DdType, ValueType > &stateSignatureComputer, SignatureRefiner< DdType, ValueType > &signatureRefiner, Partition< DdType, ValueType > const &oldPartition, Partition< DdType, ValueType > const &targetPartition, SignatureMode const &mode=SignatureMode::Eager)
Partition< DdType, ValueType >	internalRefine (Signature< DdType, ValueType > const &signature, SignatureRefiner< DdType, ValueType > &signatureRefiner, Partition< DdType, ValueType > const &oldPartition)
virtual bool	refineWrtStateRewards (storm::dd::Add< DdType, ValueType > const &stateRewards)
virtual bool	refineWrtStateActionRewards (storm::dd::Add< DdType, ValueType > const &stateActionRewards)

Protected Attributes
Status	status
uint64_t	refinements
Partition< DdType, ValueType >	statePartition
SignatureComputer< DdType, ValueType >	signatureComputer
SignatureRefiner< DdType, ValueType >	signatureRefiner
std::chrono::high_resolution_clock::duration	totalSignatureTime
std::chrono::high_resolution_clock::duration	totalRefinementTime

Detailed Description

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

Definition at line 21 of file PartitionRefiner.h.

Constructor & Destructor Documentation

◆ PartitionRefiner()

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

storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::PartitionRefiner	(	storm::models::symbolic::Model< DdType, ValueType > const &	model,
		Partition< DdType, ValueType > const &	initialStatePartition )

Definition at line 15 of file PartitionRefiner.cpp.

◆ ~PartitionRefiner()

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

virtual storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::~PartitionRefiner ( )

virtualdefault

Member Function Documentation

◆ getFullSignature()

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

Signature< DdType, ValueType > storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::getFullSignature ( ) const

Retrieves the full signature of all states wrt.

the current state partition.

Definition at line 145 of file PartitionRefiner.cpp.

◆ getStatePartition()

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

Partition< DdType, ValueType > const & storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::getStatePartition ( ) const

Retrieves the current state partition in the refinement process.

Definition at line 140 of file PartitionRefiner.cpp.

◆ getStatus()

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

Status storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::getStatus ( ) const

Retrieves the status of the refinement process.

Definition at line 150 of file PartitionRefiner.cpp.

◆ getTotalRefinementTime()

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

std::chrono::high_resolution_clock::duration storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::getTotalRefinementTime ( ) const

Definition at line 160 of file PartitionRefiner.cpp.

◆ getTotalSignatureTime()

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

std::chrono::high_resolution_clock::duration storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::getTotalSignatureTime ( ) const

Definition at line 155 of file PartitionRefiner.cpp.

◆ internalRefine() [1/2]

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

Partition< DdType, ValueType > storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::internalRefine	(	Signature< DdType, ValueType > const &	signature,
		SignatureRefiner< DdType, ValueType > &	signatureRefiner,
		Partition< DdType, ValueType > const &	oldPartition )

protected

Definition at line 92 of file PartitionRefiner.cpp.

◆ internalRefine() [2/2]

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

Partition< DdType, ValueType > storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::internalRefine	(	SignatureComputer< DdType, ValueType > &	stateSignatureComputer,
		SignatureRefiner< DdType, ValueType > &	signatureRefiner,
		Partition< DdType, ValueType > const &	oldPartition,
		Partition< DdType, ValueType > const &	targetPartition,
		SignatureMode const &	mode = SignatureMode::Eager )

protected

Definition at line 41 of file PartitionRefiner.cpp.

◆ refine()

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

bool storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::refine ( SignatureMode const & mode = SignatureMode::Eager )

virtual

Refines the partition.

Parameters

mode	The signature mode to use.

Returns: False iff the partition is stable and no refinement was actually performed.

Reimplemented in storm::dd::bisimulation::NondeterministicModelPartitionRefiner< DdType, ValueType >.

Definition at line 29 of file PartitionRefiner.cpp.

◆ refineWrtRewardModel()

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

bool storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::refineWrtRewardModel ( storm::models::symbolic::StandardRewardModel< DdType, ValueType > const & rewardModel )

Refines the partition wrt.

to the reward model.

Returns: True iff the partition is stable and no refinement was actually performed.

Definition at line 106 of file PartitionRefiner.cpp.

◆ refineWrtStateActionRewards()

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

bool storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::refineWrtStateActionRewards ( storm::dd::Add< DdType, ValueType > const & stateActionRewards )

protectedvirtual

Definition at line 133 of file PartitionRefiner.cpp.

◆ refineWrtStateRewards()

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

bool storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::refineWrtStateRewards ( storm::dd::Add< DdType, ValueType > const & stateRewards )

protectedvirtual

Definition at line 121 of file PartitionRefiner.cpp.

Member Data Documentation

◆ refinements

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

uint64_t storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::refinements

protected

Definition at line 73 of file PartitionRefiner.h.

◆ signatureComputer

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

SignatureComputer<DdType, ValueType> storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::signatureComputer

protected

Definition at line 79 of file PartitionRefiner.h.

◆ signatureRefiner

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

SignatureRefiner<DdType, ValueType> storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::signatureRefiner

protected

Definition at line 82 of file PartitionRefiner.h.

◆ statePartition

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

Partition<DdType, ValueType> storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::statePartition

protected

Definition at line 76 of file PartitionRefiner.h.

◆ status

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

Status storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::status

protected

Definition at line 70 of file PartitionRefiner.h.

◆ totalRefinementTime

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

std::chrono::high_resolution_clock::duration storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::totalRefinementTime

protected

Definition at line 86 of file PartitionRefiner.h.

◆ totalSignatureTime

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

std::chrono::high_resolution_clock::duration storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >::totalSignatureTime

protected

Definition at line 85 of file PartitionRefiner.h.

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

src/storm/storage/dd/bisimulation/BisimulationDecomposition.h
src/storm/storage/dd/bisimulation/PartitionRefiner.h
src/storm/storage/dd/bisimulation/PartitionRefiner.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ PartitionRefiner()

◆ ~PartitionRefiner()

Member Function Documentation

◆ getFullSignature()

◆ getStatePartition()

◆ getStatus()

◆ getTotalRefinementTime()

◆ getTotalSignatureTime()

◆ internalRefine() [1/2]

◆ internalRefine() [2/2]

◆ refine()

◆ refineWrtRewardModel()

◆ refineWrtStateActionRewards()

◆ refineWrtStateRewards()

Member Data Documentation

◆ refinements

◆ signatureComputer

◆ signatureRefiner

◆ statePartition

◆ status

◆ totalRefinementTime

◆ totalSignatureTime