This class represents the bisimulation settings. More...

#include <BisimulationSettings.h>

Inheritance diagram for storm::settings::modules::BisimulationSettings:

Collaboration diagram for storm::settings::modules::BisimulationSettings:

Public Types
enum class	BisimulationType { Strong , Weak }

enum class	ReuseMode { None , BlockNumbers }

enum class	InitialPartitionMode { Regular , Finer }

enum class	RefinementMode { Full , ChangedStates }

Public Member Functions
	BisimulationSettings ()
	Creates a new set of bisimulation settings.

bool	isStrongBisimulationSet () const
	Retrieves whether strong bisimulation is to be used.

bool	isWeakBisimulationSet () const
	Retrieves whether weak bisimulation is to be used.

bool	isQuotientFormatSetFromDefaultValue () const
	Retrieves whether the format in which the quotient is to be extracted has been set from its default value.

storm::dd::bisimulation::QuotientFormat	getQuotientFormat () const
	Retrieves the format in which the quotient is to be extracted.

bool	isUseRepresentativesSet () const
	Retrieves whether representatives for blocks are to be used instead of the block numbers.

bool	isUseOriginalVariablesSet () const
	Retrieves whether the extracted quotient model is supposed to use the same variables as the original model.

bool	useExactArithmeticInDdBisimulation () const
	Retrieves whether exact arithmetic is to be used in symbolic bisimulation minimization.

storm::dd::bisimulation::SignatureMode	getSignatureMode () const
	Retrieves the mode to compute signatures.

ReuseMode	getReuseMode () const
	Retrieves the selected reuse mode.

InitialPartitionMode	getInitialPartitionMode () const
	Retrieves the initial partition mode.

RefinementMode	getRefinementMode () const
	Retrieves the refinement mode to use.

virtual bool	check () const override
	Checks whether the settings are consistent.

Public Member Functions inherited from storm::settings::modules::ModuleSettings
	ModuleSettings (std::string const &moduleName)
	Constructs a new settings object.

virtual	~ModuleSettings ()

virtual void	finalize ()
	Prepares the modules for further usage, should be called at the end of the initialization, before checks are executed.

std::unique_ptr< storm::settings::SettingMemento >	overrideOption (std::string const &name, bool requiredStatus)
	Sets the option with the given name to the required status.

std::string const &	getModuleName () const
	Retrieves the name of the module to which these settings belong.

std::vector< std::shared_ptr< Option > > const &	getOptions () const
	Retrieves the options of this module.

uint_fast64_t	getPrintLengthOfLongestOption (bool includeAdvanced) const
	Retrieves the (print) length of the longest option.

void	restoreDefaults ()
	Restores the default values for all arguments of all options.

Static Public Attributes
static const std::string	moduleName = "bisimulation"

Additional Inherited Members
Protected Member Functions inherited from storm::settings::modules::ModuleSettings
Option &	getOption (std::string const &longName)
	Retrieves the option with the given long name.

Option const &	getOption (std::string const &longName) const
	Retrieves the option with the given long name.

bool	isSet (std::string const &optionName) const
	Retrieves whether the option with the given name was set.

void	set (std::string const &name)
	Sets the option with the specified name.

void	unset (std::string const &name)
	Unsets the option with the specified name.

void	addOption (std::shared_ptr< Option > const &option)
	Adds and registers the given option.

Detailed Description

This class represents the bisimulation settings.

Definition at line 16 of file BisimulationSettings.h.

Member Enumeration Documentation

◆ BisimulationType

enum class storm::settings::modules::BisimulationSettings::BisimulationType

strong

Enumerator
Strong
Weak

Definition at line 19 of file BisimulationSettings.h.

◆ InitialPartitionMode

enum class storm::settings::modules::BisimulationSettings::InitialPartitionMode

strong

Enumerator
Regular
Finer

Definition at line 23 of file BisimulationSettings.h.

◆ RefinementMode

enum class storm::settings::modules::BisimulationSettings::RefinementMode

strong

Enumerator
Full
ChangedStates

Definition at line 25 of file BisimulationSettings.h.

◆ ReuseMode

enum class storm::settings::modules::BisimulationSettings::ReuseMode

strong

Enumerator
None
BlockNumbers

Definition at line 21 of file BisimulationSettings.h.

Constructor & Destructor Documentation

◆ BisimulationSettings()

storm::settings::modules::BisimulationSettings::BisimulationSettings ( )

Creates a new set of bisimulation settings.

Definition at line 26 of file BisimulationSettings.cpp.

Member Function Documentation

◆ check()

bool storm::settings::modules::BisimulationSettings::check ( ) const

overridevirtual

Checks whether the settings are consistent.

If they are inconsistent, an exception is thrown.

Returns: True if the settings are consistent.

Reimplemented from storm::settings::modules::ModuleSettings.

Definition at line 176 of file BisimulationSettings.cpp.

◆ getInitialPartitionMode()

BisimulationSettings::InitialPartitionMode storm::settings::modules::BisimulationSettings::getInitialPartitionMode ( ) const

Retrieves the initial partition mode.

Definition at line 156 of file BisimulationSettings.cpp.

◆ getQuotientFormat()

storm::dd::bisimulation::QuotientFormat storm::settings::modules::BisimulationSettings::getQuotientFormat ( ) const

Retrieves the format in which the quotient is to be extracted.

NOTE: only applies to DD-based bisimulation.

Definition at line 115 of file BisimulationSettings.cpp.

◆ getRefinementMode()

BisimulationSettings::RefinementMode storm::settings::modules::BisimulationSettings::getRefinementMode ( ) const

Retrieves the refinement mode to use.

Definition at line 166 of file BisimulationSettings.cpp.

◆ getReuseMode()

BisimulationSettings::ReuseMode storm::settings::modules::BisimulationSettings::getReuseMode ( ) const

Retrieves the selected reuse mode.

Definition at line 146 of file BisimulationSettings.cpp.

◆ getSignatureMode()

storm::dd::bisimulation::SignatureMode storm::settings::modules::BisimulationSettings::getSignatureMode ( ) const

Retrieves the mode to compute signatures.

Definition at line 136 of file BisimulationSettings.cpp.

◆ isQuotientFormatSetFromDefaultValue()

bool storm::settings::modules::BisimulationSettings::isQuotientFormatSetFromDefaultValue ( ) const

Retrieves whether the format in which the quotient is to be extracted has been set from its default value.

Returns: True iff it has been set from its default value.

Definition at line 110 of file BisimulationSettings.cpp.

◆ isStrongBisimulationSet()

bool storm::settings::modules::BisimulationSettings::isStrongBisimulationSet ( ) const

Retrieves whether strong bisimulation is to be used.

Returns: True iff strong bisimulation is to be used.

Definition at line 96 of file BisimulationSettings.cpp.

◆ isUseOriginalVariablesSet()

bool storm::settings::modules::BisimulationSettings::isUseOriginalVariablesSet ( ) const

Retrieves whether the extracted quotient model is supposed to use the same variables as the original model.

NOTE: only applies to DD-based bisimulation.

Definition at line 128 of file BisimulationSettings.cpp.

◆ isUseRepresentativesSet()

bool storm::settings::modules::BisimulationSettings::isUseRepresentativesSet ( ) const

Retrieves whether representatives for blocks are to be used instead of the block numbers.

NOTE: only applies to DD-based bisimulation.

Definition at line 124 of file BisimulationSettings.cpp.

◆ isWeakBisimulationSet()

bool storm::settings::modules::BisimulationSettings::isWeakBisimulationSet ( ) const

Retrieves whether weak bisimulation is to be used.

Returns: True iff weak bisimulation is to be used.

Definition at line 103 of file BisimulationSettings.cpp.

◆ useExactArithmeticInDdBisimulation()

bool storm::settings::modules::BisimulationSettings::useExactArithmeticInDdBisimulation ( ) const

Retrieves whether exact arithmetic is to be used in symbolic bisimulation minimization.

Returns: True iff exact arithmetic is to be used in symbolic bisimulation minimization.

Definition at line 132 of file BisimulationSettings.cpp.

Member Data Documentation

◆ moduleName

const std::string storm::settings::modules::BisimulationSettings::moduleName = "bisimulation"

static

Definition at line 102 of file BisimulationSettings.h.

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

src/storm/settings/modules/BisimulationSettings.h
src/storm/settings/modules/BisimulationSettings.cpp

Public Types

Public Member Functions

Static Public Attributes

Additional Inherited Members

Detailed Description

Member Enumeration Documentation

◆ BisimulationType

◆ InitialPartitionMode

◆ RefinementMode

◆ ReuseMode

Constructor & Destructor Documentation

◆ BisimulationSettings()

Member Function Documentation

◆ check()

◆ getInitialPartitionMode()

◆ getQuotientFormat()

◆ getRefinementMode()

◆ getReuseMode()

◆ getSignatureMode()

◆ isQuotientFormatSetFromDefaultValue()

◆ isStrongBisimulationSet()

◆ isUseOriginalVariablesSet()

◆ isUseRepresentativesSet()

◆ isWeakBisimulationSet()

◆ useExactArithmeticInDdBisimulation()

Member Data Documentation

◆ moduleName