Storm 1.12.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Types | Public Member Functions | List of all members
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)
 
bool isLexicographicModelCheckingSet () const
 
void setLexicographicModelChecking (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 57 of file MultiObjectiveModelCheckerEnvironment.cpp.

Member Function Documentation

◆ getApproximationTradeoff()

storm::RationalNumber const & storm::MultiObjectiveModelCheckerEnvironment::getApproximationTradeoff ( ) const

Definition at line 159 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getEncodingType()

MultiObjectiveModelCheckerEnvironment::EncodingType const & storm::MultiObjectiveModelCheckerEnvironment::getEncodingType ( ) const

Definition at line 125 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getMaxSteps()

uint64_t const & storm::MultiObjectiveModelCheckerEnvironment::getMaxSteps ( ) const

Definition at line 175 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getMethod()

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

Definition at line 61 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getPlotPathOverApproximation()

boost::optional< std::string > storm::MultiObjectiveModelCheckerEnvironment::getPlotPathOverApproximation ( ) const

Definition at line 85 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getPlotPathParetoPoints()

boost::optional< std::string > storm::MultiObjectiveModelCheckerEnvironment::getPlotPathParetoPoints ( ) const

Definition at line 97 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getPlotPathUnderApproximation()

boost::optional< std::string > storm::MultiObjectiveModelCheckerEnvironment::getPlotPathUnderApproximation ( ) const

Definition at line 73 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getPrecision()

storm::RationalNumber const & storm::MultiObjectiveModelCheckerEnvironment::getPrecision ( ) const

Definition at line 109 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getPrecisionType()

MultiObjectiveModelCheckerEnvironment::PrecisionType const & storm::MultiObjectiveModelCheckerEnvironment::getPrecisionType ( ) const

Definition at line 117 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getSchedulerRestriction()

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

Definition at line 191 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getUseBsccOrderEncoding()

bool storm::MultiObjectiveModelCheckerEnvironment::getUseBsccOrderEncoding ( ) const

Definition at line 140 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getUseIndicatorConstraints()

bool storm::MultiObjectiveModelCheckerEnvironment::getUseIndicatorConstraints ( ) const

Definition at line 133 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ getUseRedundantBsccConstraints()

bool storm::MultiObjectiveModelCheckerEnvironment::getUseRedundantBsccConstraints ( ) const

Definition at line 147 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 155 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ isExportPlotSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isExportPlotSet ( ) const

Definition at line 69 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ isLexicographicModelCheckingSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isLexicographicModelCheckingSet ( ) const

Definition at line 211 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ isMaxStepsSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isMaxStepsSet ( ) const

Definition at line 171 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ isPrintResultsSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isPrintResultsSet ( ) const

Definition at line 203 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ isSchedulerRestrictionSet()

bool storm::MultiObjectiveModelCheckerEnvironment::isSchedulerRestrictionSet ( ) const

Definition at line 187 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setApproximationTradeoff()

void storm::MultiObjectiveModelCheckerEnvironment::setApproximationTradeoff ( storm::RationalNumber const &  value)

Definition at line 163 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setEncodingType()

void storm::MultiObjectiveModelCheckerEnvironment::setEncodingType ( EncodingType const &  value)

Definition at line 129 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setLexicographicModelChecking()

void storm::MultiObjectiveModelCheckerEnvironment::setLexicographicModelChecking ( bool  value)

Definition at line 215 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setMaxSteps()

void storm::MultiObjectiveModelCheckerEnvironment::setMaxSteps ( uint64_t const &  value)

Definition at line 179 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setMethod()

void storm::MultiObjectiveModelCheckerEnvironment::setMethod ( storm::modelchecker::multiobjective::MultiObjectiveMethod  value)

Definition at line 65 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setPlotPathOverApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::setPlotPathOverApproximation ( std::string const &  path)

Definition at line 89 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setPlotPathParetoPoints()

void storm::MultiObjectiveModelCheckerEnvironment::setPlotPathParetoPoints ( std::string const &  path)

Definition at line 101 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setPlotPathUnderApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::setPlotPathUnderApproximation ( std::string const &  path)

Definition at line 77 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setPrecision()

void storm::MultiObjectiveModelCheckerEnvironment::setPrecision ( storm::RationalNumber const &  value)

Definition at line 113 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setPrecisionType()

void storm::MultiObjectiveModelCheckerEnvironment::setPrecisionType ( PrecisionType const &  value)

Definition at line 121 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setPrintResults()

void storm::MultiObjectiveModelCheckerEnvironment::setPrintResults ( bool  value)

Definition at line 207 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setSchedulerRestriction()

void storm::MultiObjectiveModelCheckerEnvironment::setSchedulerRestriction ( storm::storage::SchedulerClass const &  value)

Definition at line 195 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setUseBsccOrderEncoding()

void storm::MultiObjectiveModelCheckerEnvironment::setUseBsccOrderEncoding ( bool  value)

Definition at line 143 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setUseIndicatorConstraints()

void storm::MultiObjectiveModelCheckerEnvironment::setUseIndicatorConstraints ( bool  value)

Definition at line 136 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ setUseRedundantBsccConstraints()

void storm::MultiObjectiveModelCheckerEnvironment::setUseRedundantBsccConstraints ( bool  value)

Definition at line 151 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ unsetApproximationTradeoff()

void storm::MultiObjectiveModelCheckerEnvironment::unsetApproximationTradeoff ( )

Definition at line 167 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ unsetMaxSteps()

void storm::MultiObjectiveModelCheckerEnvironment::unsetMaxSteps ( )

Definition at line 183 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ unsetPlotPathOverApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::unsetPlotPathOverApproximation ( )

Definition at line 93 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ unsetPlotPathParetoPoints()

void storm::MultiObjectiveModelCheckerEnvironment::unsetPlotPathParetoPoints ( )

Definition at line 105 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ unsetPlotPathUnderApproximation()

void storm::MultiObjectiveModelCheckerEnvironment::unsetPlotPathUnderApproximation ( )

Definition at line 81 of file MultiObjectiveModelCheckerEnvironment.cpp.

◆ unsetSchedulerRestriction()

void storm::MultiObjectiveModelCheckerEnvironment::unsetSchedulerRestriction ( )

Definition at line 199 of file MultiObjectiveModelCheckerEnvironment.cpp.

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