Storm 1.13.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType > Class Template Reference

#include <BisimulationDecomposition.h>

Public Member Functions

 BisimulationDecomposition (storm::models::symbolic::Model< DdType, ValueType > const &model, storm::storage::BisimulationType const &bisimulationType)
 BisimulationDecomposition (storm::models::symbolic::Model< DdType, ValueType > const &model, storm::storage::BisimulationType const &bisimulationType, bisimulation::PreservationInformation< DdType, ValueType > const &preservationInformation)
 BisimulationDecomposition (storm::models::symbolic::Model< DdType, ValueType > const &model, std::vector< std::shared_ptr< storm::logic::Formula const > > const &formulas, storm::storage::BisimulationType const &bisimulationType)
 BisimulationDecomposition (storm::models::symbolic::Model< DdType, ValueType > const &model, bisimulation::Partition< DdType, ValueType > const &initialPartition, bisimulation::PreservationInformation< DdType, ValueType > const &preservationInformation)
 ~BisimulationDecomposition ()
void compute (bisimulation::SignatureMode const &mode=bisimulation::SignatureMode::Eager)
 Performs partition refinement until a fixpoint has been reached.
bool compute (uint64_t steps, bisimulation::SignatureMode const &mode=bisimulation::SignatureMode::Eager)
 Performs the given number of refinement steps.
bool getReachedFixedPoint () const
 Retrieves whether a fixed point has been reached.
std::shared_ptr< storm::models::Model< ExportValueType > > getQuotient (storm::dd::bisimulation::QuotientFormat const &quotientFormat) const
 Retrieves the quotient model after the bisimulation decomposition was computed.

Detailed Description

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType = ValueType>
class storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >

Definition at line 37 of file BisimulationDecomposition.h.

Constructor & Destructor Documentation

◆ BisimulationDecomposition() [1/4]

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::BisimulationDecomposition ( storm::models::symbolic::Model< DdType, ValueType > const & model,
storm::storage::BisimulationType const & bisimulationType )

Definition at line 34 of file BisimulationDecomposition.cpp.

◆ BisimulationDecomposition() [2/4]

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::BisimulationDecomposition ( storm::models::symbolic::Model< DdType, ValueType > const & model,
storm::storage::BisimulationType const & bisimulationType,
bisimulation::PreservationInformation< DdType, ValueType > const & preservationInformation )

Definition at line 43 of file BisimulationDecomposition.cpp.

◆ BisimulationDecomposition() [3/4]

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::BisimulationDecomposition ( storm::models::symbolic::Model< DdType, ValueType > const & model,
std::vector< std::shared_ptr< storm::logic::Formula const > > const & formulas,
storm::storage::BisimulationType const & bisimulationType )

Definition at line 53 of file BisimulationDecomposition.cpp.

◆ BisimulationDecomposition() [4/4]

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::BisimulationDecomposition ( storm::models::symbolic::Model< DdType, ValueType > const & model,
bisimulation::Partition< DdType, ValueType > const & initialPartition,
bisimulation::PreservationInformation< DdType, ValueType > const & preservationInformation )

Definition at line 63 of file BisimulationDecomposition.cpp.

◆ ~BisimulationDecomposition()

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::~BisimulationDecomposition ( )
default

Member Function Documentation

◆ compute() [1/2]

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
void storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::compute ( bisimulation::SignatureMode const & mode = bisimulation::SignatureMode::Eager)

Performs partition refinement until a fixpoint has been reached.

Definition at line 89 of file BisimulationDecomposition.cpp.

◆ compute() [2/2]

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
bool storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::compute ( uint64_t steps,
bisimulation::SignatureMode const & mode = bisimulation::SignatureMode::Eager )

Performs the given number of refinement steps.

Returns
True iff the computation arrived at a fixpoint.

Definition at line 120 of file BisimulationDecomposition.cpp.

◆ getQuotient()

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
std::shared_ptr< storm::models::Model< ExportValueType > > storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::getQuotient ( storm::dd::bisimulation::QuotientFormat const & quotientFormat) const

Retrieves the quotient model after the bisimulation decomposition was computed.

Definition at line 153 of file BisimulationDecomposition.cpp.

◆ getReachedFixedPoint()

template<storm::dd::DdType DdType, typename ValueType, typename ExportValueType>
bool storm::dd::BisimulationDecomposition< DdType, ValueType, ExportValueType >::getReachedFixedPoint ( ) const

Retrieves whether a fixed point has been reached.

Depending on this, extracting a quotient will either give a full quotient or a partial one.

Definition at line 148 of file BisimulationDecomposition.cpp.

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