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 }

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.
storm::dd::bisimulation::ReuseMode	getReuseMode () const
	Retrieves the selected reuse mode.
storm::dd::bisimulation::InitialPartitionMode	getInitialPartitionMode () const
	Retrieves the initial partition mode.
storm::dd::bisimulation::RefinementMode	getRefinementMode () const
	Retrieves the refinement mode to use.
bool	isToleranceSet () const
	Retrieves whether the tolerance to use for (approximate) bisimulation minimization has been set explicitly (as opposed to using its default value).
double	getTolerance () const
	Retrieves the tolerance to use for bisimulation minimization.
bool	isActionSensitiveSet () const
	Retrieves whether action-sensitive bisimulation is to be used, i.e., choices are only lumped together if they belong to the same action.
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::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 and marks all options as not set.

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	addOption (std::shared_ptr< Option > const &option)
	Adds and registers the given option.

Detailed Description

This class represents the bisimulation settings.

Definition at line 18 of file BisimulationSettings.h.

Member Enumeration Documentation

◆ BisimulationType

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

strong

Enumerator
Strong
Weak

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 28 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 206 of file BisimulationSettings.cpp.

◆ getInitialPartitionMode()

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

Retrieves the initial partition mode.

Definition at line 174 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 133 of file BisimulationSettings.cpp.

◆ getRefinementMode()

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

Retrieves the refinement mode to use.

Definition at line 184 of file BisimulationSettings.cpp.

◆ getReuseMode()

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

Retrieves the selected reuse mode.

Definition at line 164 of file BisimulationSettings.cpp.

◆ getSignatureMode()

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

Retrieves the mode to compute signatures.

Definition at line 154 of file BisimulationSettings.cpp.

◆ getTolerance()

double storm::settings::modules::BisimulationSettings::getTolerance ( ) const

Retrieves the tolerance to use for bisimulation minimization.

Note: : only applies to sparse bisimulation.

Definition at line 198 of file BisimulationSettings.cpp.

◆ isActionSensitiveSet()

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

Retrieves whether action-sensitive bisimulation is to be used, i.e., choices are only lumped together if they belong to the same action.

NOTE: only applies to sparse bisimulation.

Definition at line 202 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 128 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 114 of file BisimulationSettings.cpp.

◆ isToleranceSet()

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

Retrieves whether the tolerance to use for (approximate) bisimulation minimization has been set explicitly (as opposed to using its default value).

Definition at line 194 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 146 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 142 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 121 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 150 of file BisimulationSettings.cpp.

Member Data Documentation

◆ moduleName

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

static

Definition at line 115 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

Constructor & Destructor Documentation

◆ BisimulationSettings()

Member Function Documentation

◆ check()

◆ getInitialPartitionMode()

◆ getQuotientFormat()

◆ getRefinementMode()

◆ getReuseMode()

◆ getSignatureMode()

◆ getTolerance()

◆ isActionSensitiveSet()

◆ isQuotientFormatSetFromDefaultValue()

◆ isStrongBisimulationSet()

◆ isToleranceSet()

◆ isUseOriginalVariablesSet()

◆ isUseRepresentativesSet()

◆ isWeakBisimulationSet()

◆ useExactArithmeticInDdBisimulation()

Member Data Documentation

◆ moduleName