storm::MultiObjectiveModelCheckerEnvironment Class Reference

#include <MultiObjectiveModelCheckerEnvironment.h>

Public Types
enum class	PrecisionType { Absolute , RelativeToDiff }
enum class	EncodingType { Auto , Classic , Flow }

Public Member Functions
	MultiObjectiveModelCheckerEnvironment ()
	~MultiObjectiveModelCheckerEnvironment ()
storm::modelchecker::multiobjective::MultiObjectiveMethod const &	getMethod () const
void	setMethod (storm::modelchecker::multiobjective::MultiObjectiveMethod value)
bool	isExportPlotSet () const
boost::optional< std::string >	getPlotPathUnderApproximation () const
void	setPlotPathUnderApproximation (std::string const &path)
void	unsetPlotPathUnderApproximation ()
boost::optional< std::string >	getPlotPathOverApproximation () const
void	setPlotPathOverApproximation (std::string const &path)
void	unsetPlotPathOverApproximation ()
boost::optional< std::string >	getPlotPathParetoPoints () const
void	setPlotPathParetoPoints (std::string const &path)
void	unsetPlotPathParetoPoints ()
storm::RationalNumber const &	getPrecision () const
void	setPrecision (storm::RationalNumber const &value)
PrecisionType const &	getPrecisionType () const
void	setPrecisionType (PrecisionType const &value)
EncodingType const &	getEncodingType () const
void	setEncodingType (EncodingType const &value)
bool	getUseIndicatorConstraints () const
void	setUseIndicatorConstraints (bool value)
bool	getUseBsccOrderEncoding () const
void	setUseBsccOrderEncoding (bool value)
bool	getUseRedundantBsccConstraints () const
void	setUseRedundantBsccConstraints (bool value)
bool	isApproximationTradeoffSet () const
	Configure approximation tradeoff between accuracy of weighted sum optimization vs.
storm::RationalNumber const &	getApproximationTradeoff () const
void	setApproximationTradeoff (storm::RationalNumber const &value)
void	unsetApproximationTradeoff ()
bool	isMaxStepsSet () const
uint64_t const &	getMaxSteps () const
void	setMaxSteps (uint64_t const &value)
void	unsetMaxSteps ()
bool	isSchedulerRestrictionSet () const
storm::storage::SchedulerClass const &	getSchedulerRestriction () const
void	setSchedulerRestriction (storm::storage::SchedulerClass const &value)
void	unsetSchedulerRestriction ()
bool	isPrintResultsSet () const
void	setPrintResults (bool value)

Detailed Description

Definition at line 12 of file MultiObjectiveModelCheckerEnvironment.h.

Member Enumeration Documentation

EncodingType

enum class storm::MultiObjectiveModelCheckerEnvironment::EncodingType

strong

Enumerator
Auto
Classic	Pick automatically.
Flow	The classic backwards encoding. The encoding as a flow network

Definition at line 19 of file MultiObjectiveModelCheckerEnvironment.h.

PrecisionType

enum class storm::MultiObjectiveModelCheckerEnvironment::PrecisionType

strong

Enumerator
Absolute
RelativeToDiff	Absolute precision. Relative to the difference between largest and smallest objective value(s)

Definition at line 14 of file MultiObjectiveModelCheckerEnvironment.h.

Constructor & Destructor Documentation

MultiObjectiveModelCheckerEnvironment()

storm::MultiObjectiveModelCheckerEnvironment::MultiObjectiveModelCheckerEnvironment

(

)

Definition at line 11 of file MultiObjectiveModelCheckerEnvironment.cpp.

~MultiObjectiveModelCheckerEnvironment()

storm::MultiObjectiveModelCheckerEnvironment::~MultiObjectiveModelCheckerEnvironment

(

)

Definition at line 56 of file MultiObjectiveModelCheckerEnvironment.cpp.

Member Function Documentation

getApproximationTradeoff()

storm::RationalNumber const & storm::MultiObjectiveModelCheckerEnvironment::getApproximationTradeoff

(

)

const

Definition at line 158 of file MultiObjectiveModelCheckerEnvironment.cpp.

getEncodingType()

MultiObjectiveModelCheckerEnvironment::EncodingType const & storm::MultiObjectiveModelCheckerEnvironment::getEncodingType

(

)

const

Definition at line 124 of file MultiObjectiveModelCheckerEnvironment.cpp.

getMaxSteps()

uint64_t const & storm::MultiObjectiveModelCheckerEnvironment::getMaxSteps

(

)

const

Definition at line 174 of file MultiObjectiveModelCheckerEnvironment.cpp.

getMethod()

storm::modelchecker::multiobjective::MultiObjectiveMethod const & storm::MultiObjectiveModelCheckerEnvironment::getMethod

(

)

const

Definition at line 60 of file MultiObjectiveModelCheckerEnvironment.cpp.

getPlotPathOverApproximation()

boost::optional< std::string > storm::MultiObjectiveModelCheckerEnvironment::getPlotPathOverApproximation

(

)

const

Definition at line 84 of file MultiObjectiveModelCheckerEnvironment.cpp.

getPlotPathParetoPoints()

boost::optional< std::string > storm::MultiObjectiveModelCheckerEnvironment::getPlotPathParetoPoints

(

)

const

Definition at line 96 of file MultiObjectiveModelCheckerEnvironment.cpp.

getPlotPathUnderApproximation()

boost::optional< std::string > storm::MultiObjectiveModelCheckerEnvironment::getPlotPathUnderApproximation

(

)

const

Definition at line 72 of file MultiObjectiveModelCheckerEnvironment.cpp.

getPrecision()

storm::RationalNumber const & storm::MultiObjectiveModelCheckerEnvironment::getPrecision

(

)

const

Definition at line 108 of file MultiObjectiveModelCheckerEnvironment.cpp.

getPrecisionType()

MultiObjectiveModelCheckerEnvironment::PrecisionType const & storm::MultiObjectiveModelCheckerEnvironment::getPrecisionType

(

)

const

Definition at line 116 of file MultiObjectiveModelCheckerEnvironment.cpp.

getSchedulerRestriction()

storm::storage::SchedulerClass const & storm::MultiObjectiveModelCheckerEnvironment::getSchedulerRestriction

(

)

const

Definition at line 190 of file MultiObjectiveModelCheckerEnvironment.cpp.

getUseBsccOrderEncoding()

bool storm::MultiObjectiveModelCheckerEnvironment::getUseBsccOrderEncoding

(

)

const

Definition at line 139 of file MultiObjectiveModelCheckerEnvironment.cpp.

getUseIndicatorConstraints()

bool storm::MultiObjectiveModelCheckerEnvironment::getUseIndicatorConstraints

(

)

const

Definition at line 132 of file MultiObjectiveModelCheckerEnvironment.cpp.

getUseRedundantBsccConstraints()

bool storm::MultiObjectiveModelCheckerEnvironment::getUseRedundantBsccConstraints

(

)

const

Definition at line 146 of file MultiObjectiveModelCheckerEnvironment.cpp.

isApproximationTradeoffSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isApproximationTradeoffSet

(

)

const

Configure approximation tradeoff between accuracy of weighted sum optimization vs.

Pareto curve exploration. See gamma in https://doi.org/10.18154/RWTH-2023-09669, Alg. 3.3. We must have 0 < gamma < 1. A small value means that weighted sum optimization is done with higher accuracy, which can lead to convergence of Pareto exploration within fewer steps. If no value is set explicitly, a value is set heuristically based on precision requirements.

Definition at line 154 of file MultiObjectiveModelCheckerEnvironment.cpp.

isExportPlotSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isExportPlotSet

(

)

const

Definition at line 68 of file MultiObjectiveModelCheckerEnvironment.cpp.

isMaxStepsSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isMaxStepsSet

(

)

const

Definition at line 170 of file MultiObjectiveModelCheckerEnvironment.cpp.

isPrintResultsSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isPrintResultsSet

(

)

const

Definition at line 202 of file MultiObjectiveModelCheckerEnvironment.cpp.

isSchedulerRestrictionSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isSchedulerRestrictionSet

(

)

const

Definition at line 186 of file MultiObjectiveModelCheckerEnvironment.cpp.

setApproximationTradeoff()

void storm::MultiObjectiveModelCheckerEnvironment::setApproximationTradeoff

(

storm::RationalNumber const &

value

)

Definition at line 162 of file MultiObjectiveModelCheckerEnvironment.cpp.

setEncodingType()

void storm::MultiObjectiveModelCheckerEnvironment::setEncodingType

(

EncodingType const &

value

)

Definition at line 128 of file MultiObjectiveModelCheckerEnvironment.cpp.

setMaxSteps()

void storm::MultiObjectiveModelCheckerEnvironment::setMaxSteps

(

uint64_t const &

value

)

Definition at line 178 of file MultiObjectiveModelCheckerEnvironment.cpp.

setMethod()

void storm::MultiObjectiveModelCheckerEnvironment::setMethod

(

storm::modelchecker::multiobjective::MultiObjectiveMethod

value

)

Definition at line 64 of file MultiObjectiveModelCheckerEnvironment.cpp.

setPlotPathOverApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::setPlotPathOverApproximation

(

std::string const &

path

)

Definition at line 88 of file MultiObjectiveModelCheckerEnvironment.cpp.

setPlotPathParetoPoints()

void storm::MultiObjectiveModelCheckerEnvironment::setPlotPathParetoPoints

(

std::string const &

path

)

Definition at line 100 of file MultiObjectiveModelCheckerEnvironment.cpp.

setPlotPathUnderApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::setPlotPathUnderApproximation

(

std::string const &

path

)

Definition at line 76 of file MultiObjectiveModelCheckerEnvironment.cpp.

setPrecision()

void storm::MultiObjectiveModelCheckerEnvironment::setPrecision

(

storm::RationalNumber const &

value

)

Definition at line 112 of file MultiObjectiveModelCheckerEnvironment.cpp.

setPrecisionType()

void storm::MultiObjectiveModelCheckerEnvironment::setPrecisionType

(

PrecisionType const &

value

)

Definition at line 120 of file MultiObjectiveModelCheckerEnvironment.cpp.

setPrintResults()

void storm::MultiObjectiveModelCheckerEnvironment::setPrintResults

(

bool

value

)

Definition at line 206 of file MultiObjectiveModelCheckerEnvironment.cpp.

setSchedulerRestriction()

void storm::MultiObjectiveModelCheckerEnvironment::setSchedulerRestriction

(

storm::storage::SchedulerClass const &

value

)

Definition at line 194 of file MultiObjectiveModelCheckerEnvironment.cpp.

setUseBsccOrderEncoding()

void storm::MultiObjectiveModelCheckerEnvironment::setUseBsccOrderEncoding

(

bool

value

)

Definition at line 142 of file MultiObjectiveModelCheckerEnvironment.cpp.

setUseIndicatorConstraints()

void storm::MultiObjectiveModelCheckerEnvironment::setUseIndicatorConstraints

(

bool

value

)

Definition at line 135 of file MultiObjectiveModelCheckerEnvironment.cpp.

setUseRedundantBsccConstraints()

void storm::MultiObjectiveModelCheckerEnvironment::setUseRedundantBsccConstraints

(

bool

value

)

Definition at line 150 of file MultiObjectiveModelCheckerEnvironment.cpp.

unsetApproximationTradeoff()

void storm::MultiObjectiveModelCheckerEnvironment::unsetApproximationTradeoff

(

)

Definition at line 166 of file MultiObjectiveModelCheckerEnvironment.cpp.

unsetMaxSteps()

void storm::MultiObjectiveModelCheckerEnvironment::unsetMaxSteps

(

)

Definition at line 182 of file MultiObjectiveModelCheckerEnvironment.cpp.

unsetPlotPathOverApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::unsetPlotPathOverApproximation

(

)

Definition at line 92 of file MultiObjectiveModelCheckerEnvironment.cpp.

unsetPlotPathParetoPoints()

void storm::MultiObjectiveModelCheckerEnvironment::unsetPlotPathParetoPoints

(

)

Definition at line 104 of file MultiObjectiveModelCheckerEnvironment.cpp.

unsetPlotPathUnderApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::unsetPlotPathUnderApproximation

(

)

Definition at line 80 of file MultiObjectiveModelCheckerEnvironment.cpp.

unsetSchedulerRestriction()

void storm::MultiObjectiveModelCheckerEnvironment::unsetSchedulerRestriction

(

)

Definition at line 198 of file MultiObjectiveModelCheckerEnvironment.cpp.

---

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

• src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h
• src/storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.cpp