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, bisimulation::BisimulationOptions const &bisimulationOptions=bisimulation::BisimulationOptions())
	BisimulationDecomposition (storm::models::symbolic::Model< DdType, ValueType > const &model, storm::storage::BisimulationType const &bisimulationType, bisimulation::PreservationInformation< DdType, ValueType > const &preservationInformation, bisimulation::BisimulationOptions const &bisimulationOptions=bisimulation::BisimulationOptions())
	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, bisimulation::BisimulationOptions const &bisimulationOptions=bisimulation::BisimulationOptions())
	BisimulationDecomposition (storm::models::symbolic::Model< DdType, ValueType > const &model, bisimulation::Partition< DdType, ValueType > const &initialPartition, bisimulation::PreservationInformation< DdType, ValueType > const &preservationInformation, bisimulation::BisimulationOptions const &bisimulationOptions=bisimulation::BisimulationOptions())
	~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 38 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,
		bisimulation::BisimulationOptions const &	bisimulationOptions = bisimulation::BisimulationOptions() )

Definition at line 35 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,
		bisimulation::BisimulationOptions const &	bisimulationOptions = bisimulation::BisimulationOptions() )

Definition at line 46 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,
		bisimulation::BisimulationOptions const &	bisimulationOptions = bisimulation::BisimulationOptions() )

Definition at line 57 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,
		bisimulation::BisimulationOptions const &	bisimulationOptions = bisimulation::BisimulationOptions() )

Definition at line 68 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 97 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 128 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 161 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 156 of file BisimulationDecomposition.cpp.

---

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

• src/storm-gamebased-ar/modelchecker/abstraction/BisimulationAbstractionRefinementModelChecker.h
• src/storm/storage/dd/bisimulation/BisimulationDecomposition.h
• src/storm/storage/dd/bisimulation/BisimulationDecomposition.cpp