Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType > Class Template Referenceabstract

Helper Class that takes a weight vector and ... More...

#include <PcaaWeightVectorChecker.h>

Public Types

typedef ModelType::ValueType ValueType

Public Member Functions

 PcaaWeightVectorChecker (std::vector< Objective< ValueType > > const &objectives)
virtual ~PcaaWeightVectorChecker ()=default
virtual void check (Environment const &env, std::vector< ValueType > weightVector)=0
 Solves the Weighted Sum Optimization Problem for the given weight vector.
virtual std::vector< ValueType > getAchievablePoint () const =0
 Retrieves the result of the individual objectives at the initial state of the given model.
virtual ValueType getOptimalWeightedSum () const =0
 Retrieves the optimal weighted sum of the objective values (or an upper bound thereof).
virtual storm::storage::Scheduler< ValueType > computeScheduler () const
 Retrieves a scheduler that induces the current values (if such a scheduler was generated).
void setWeightedPrecision (ValueType const &value)
 Sets the precision of this weight vector checker.
ValueType const & getWeightedPrecision () const
 Returns the current precision of this weight vector checker as specified by setWeightedPrecision().
virtual bool smallPrecisionsAreChallenging () const
 Returns whether achieving precise values (i.e.

Protected Member Functions

boost::optional< ValueType > computeWeightedResultBound (bool lower, std::vector< ValueType > const &weightVector, storm::storage::BitVector const &objectiveFilter) const
 Computes the weighted lower or upper bounds for the provided set of objectives.

Protected Attributes

std::vector< Objective< ValueType > > objectives

Detailed Description

template<typename ModelType>
class storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >

Helper Class that takes a weight vector and ...

  • computes the optimal value w.r.t. the weighted sum of the individual objectives
  • extracts the scheduler that induces this optimum
  • computes for each objective the value induced by this scheduler

Definition at line 25 of file PcaaWeightVectorChecker.h.

Member Typedef Documentation

◆ ValueType

template<typename ModelType>
typedef ModelType::ValueType storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::ValueType

Definition at line 27 of file PcaaWeightVectorChecker.h.

Constructor & Destructor Documentation

◆ PcaaWeightVectorChecker()

template<typename ModelType>
storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::PcaaWeightVectorChecker ( std::vector< Objective< ValueType > > const & objectives)

Definition at line 15 of file PcaaWeightVectorChecker.cpp.

◆ ~PcaaWeightVectorChecker()

template<typename ModelType>
virtual storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::~PcaaWeightVectorChecker ( )
virtualdefault

Member Function Documentation

◆ check()

template<typename ModelType>
virtual void storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::check ( Environment const & env,
std::vector< ValueType > weightVector )
pure virtual

Solves the Weighted Sum Optimization Problem for the given weight vector.

setWeightedPrecision(..) can be used to control the accuracy of the results. After calling this, getAchievablePoint(), getOptimalWeightedSum(), and computeScheduler() can be invoked to retrieve the result of this call.

Note
before calling this for the first time, a weighted precision needs to be set. Otherwise, an exception is thrown.
Minimizing objectives (Pmin=? [...], Rmin=? [...]) are implicitly negated, i.e., we optimize sum_i p_i * (isMinimizing[i] ? -weightVector[i] : weightVector[i]), where p_i is the value of objective i For instance, a uniform weight vector like weightVector = (1, 1, ..., 1) will give equal weight to all (minimizing and maximizing) objectives.
Parameters
env
weightVectorthe weight vector of the current check. There must be at least one non-zero entry.

Implemented in storm::modelchecker::multiobjective::RewardBoundedMdpPcaaWeightVectorChecker< SparseMdpModelType >, storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseModelType >, and storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMaModelType >.

◆ computeScheduler()

template<typename ModelType>
storm::storage::Scheduler< typename PcaaWeightVectorChecker< ModelType >::ValueType > storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::computeScheduler ( ) const
virtual

Retrieves a scheduler that induces the current values (if such a scheduler was generated).

Note that check(..) has to be called before retrieving the scheduler. Otherwise, an exception is thrown.

Reimplemented in storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseModelType >, storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMaModelType >, and storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMdpModelType >.

Definition at line 36 of file PcaaWeightVectorChecker.cpp.

◆ computeWeightedResultBound()

template<class SparseModelType>
boost::optional< typename SparseModelType::ValueType > storm::modelchecker::multiobjective::PcaaWeightVectorChecker< SparseModelType >::computeWeightedResultBound ( bool lower,
std::vector< ValueType > const & weightVector,
storm::storage::BitVector const & objectiveFilter ) const
protected

Computes the weighted lower or upper bounds for the provided set of objectives.

Parameters
lowerif true, lower result bounds are computed. otherwise upper result bounds
weightVectorthe weight vector of the current check

Definition at line 41 of file PcaaWeightVectorChecker.cpp.

◆ getAchievablePoint()

template<typename ModelType>
virtual std::vector< ValueType > storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::getAchievablePoint ( ) const
pure virtual

Retrieves the result of the individual objectives at the initial state of the given model.

Note
check(..) has to be called before retrieving results. Otherwise, an exception is thrown.
there is no guarantee that the point is achievable if the underlying solution method (e.g. standard value iteration) is unsound.
minimizing objectives are only negated implicitly, i.e. this function yields the actual (non-negated) objective values. Specifically, we have (using v_i for the exact value of objective i induced by the found scheduler): (*) for maximizing objective i, getAchievablePoint()[i] <= v_i (*) for minimizing objective i, getAchievablePoint()[i] >= v_i Here, equality holds if the underlying solution method (and value type) is exact and the weighted precision is set to 0.

Implemented in storm::modelchecker::multiobjective::RewardBoundedMdpPcaaWeightVectorChecker< SparseMdpModelType >, storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseModelType >, storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMaModelType >, and storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMdpModelType >.

◆ getOptimalWeightedSum()

template<typename ModelType>
virtual ValueType storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::getOptimalWeightedSum ( ) const
pure virtual

Retrieves the optimal weighted sum of the objective values (or an upper bound thereof).

Note
check(..) has to be called before retrieving results. Otherwise, an exception is thrown.
there is no guarantee that the upper bound is sound if the underlying solution method (e.g. standard value iteration) is unsound.
minimizing objectives are handled by implicitly negating them, i.e. we optimize sum_i p_i * (isMinimizing[i] ? -weightVector[i] : weightVector[i]), where p_i is the value of objective i

Implemented in storm::modelchecker::multiobjective::RewardBoundedMdpPcaaWeightVectorChecker< SparseMdpModelType >, storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseModelType >, storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMaModelType >, and storm::modelchecker::multiobjective::StandardPcaaWeightVectorChecker< SparseMdpModelType >.

◆ getWeightedPrecision()

template<typename ModelType>
PcaaWeightVectorChecker< ModelType >::ValueType const & storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::getWeightedPrecision ( ) const

Returns the current precision of this weight vector checker as specified by setWeightedPrecision().

Definition at line 25 of file PcaaWeightVectorChecker.cpp.

◆ setWeightedPrecision()

template<typename ModelType>
void storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::setWeightedPrecision ( ValueType const & value)

Sets the precision of this weight vector checker.

After calling check() (with env.solver() set to sound or exact mode) the Euclidean distance between (*) the found achievable point (with values for minimizing objectives negated) and (*) the hyperplane with the given weightVector as normal vector and the found optimal weighted sum as offset is at most the given weightedPrecision.

Definition at line 20 of file PcaaWeightVectorChecker.cpp.

◆ smallPrecisionsAreChallenging()

template<typename ModelType>
bool storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::smallPrecisionsAreChallenging ( ) const
virtual

Returns whether achieving precise values (i.e.

low weighted precisions) might be challenging due to the type of objectives. Currently, only time-bounded Markov automaton objectives are considered challenging. This information is used to guide approximation heuristics, e.g. the choice of the approximation tradeoff in Pareto curve exploration.

Reimplemented in storm::modelchecker::multiobjective::StandardMaPcaaWeightVectorChecker< SparseMaModelType >.

Definition at line 31 of file PcaaWeightVectorChecker.cpp.

Member Data Documentation

◆ objectives

template<typename ModelType>
std::vector<Objective<ValueType> > storm::modelchecker::multiobjective::PcaaWeightVectorChecker< ModelType >::objectives
protected

Definition at line 110 of file PcaaWeightVectorChecker.h.

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