Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
storm::dd::bisimulation::PartitionRefiner< DdType, ValueType > Class Template Reference

#include <PartitionRefiner.h>

Inheritance diagram for storm::dd::bisimulation::PartitionRefiner< DdType, ValueType >:
Inheritance graph
[legend]

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
modeThe 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: