Namespaces
namespace	preprocessing

Classes
class	DeterministicSchedsAchievabilityChecker

class	DeterministicSchedsLpChecker
	Represents the LP Encoding for achievability under simple strategies. More...

class	DeterministicSchedsObjectiveHelper

class	DeterministicSchedsParetoExplorer
	Implements the exploration of the Pareto front. More...

struct	Objective

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

class	RewardBoundedMdpPcaaWeightVectorChecker
	Helper Class that takes preprocessed Pcaa data and a weight vector and ... More...

class	SparseCbAchievabilityQuery

class	SparseCbQuery

class	SparsePcaaAchievabilityQuery

class	SparsePcaaParetoQuery

class	SparsePcaaQuantitativeQuery

class	SparsePcaaQuery

class	StandardMaPcaaWeightVectorChecker
	Helper Class that takes preprocessed Pcaa data and a weight vector and ... More...

class	StandardMdpPcaaWeightVectorChecker
	Helper Class that takes preprocessed Pcaa data and a weight vector and ... More...

class	StandardPcaaWeightVectorChecker
	Helper Class that takes preprocessed Pcaa data and a weight vector and ... More...

class	VisitingTimesHelper
	Provides helper functions for computing bounds on the expected visiting times. More...

class	WeightVectorCheckerFactory

Functions
template<typename ValueType >
auto	createChoiceVariables (storm::solver::LpSolver< ValueType > &lpModel, storm::storage::SparseMatrix< ValueType > const &matrix)

template<typename ValueType , typename HelperType >
std::vector< storm::expressions::Expression >	classicConstraints (storm::solver::LpSolver< ValueType > &lpModel, bool const &indicatorConstraints, storm::storage::SparseMatrix< ValueType > const &matrix, uint64_t initialState, uint64_t objIndex, HelperType const &objectiveHelper, std::vector< storm::expressions::Expression > const &choiceVariables)

template<typename ValueType , typename ObjHelperType >
auto	computeProblematicMecs (storm::storage::SparseMatrix< ValueType > const &matrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, std::vector< ObjHelperType > const &objectiveHelper)
	Computes the set of problematic MECS with the objective indices that induced them An EC is problematic if its contained in the "maybestates" of an objective and only considers zero-reward choices.

template<typename ValueType , typename UpperBoundsGetterType >
auto	problematicMecConstraintsExpVisits (storm::solver::LpSolver< ValueType > &lpModel, bool const &indicatorConstraints, bool const &redundantConstraints, storm::storage::SparseMatrix< ValueType > const &matrix, storm::storage::SparseMatrix< ValueType > const &backwardChoices, uint64_t mecIndex, storm::storage::MaximalEndComponent const &problematicMec, std::vector< uint64_t > const &relevantObjectiveIndices, std::vector< std::vector< storm::expressions::Expression > > const &objectiveValueVariables, std::vector< storm::expressions::Expression > const &choiceVariables, UpperBoundsGetterType const &objectiveStateUpperBoundGetter)

template<typename ValueType , typename UpperBoundsGetterType >
auto	problematicMecConstraintsOrder (storm::solver::LpSolver< ValueType > &lpModel, bool const &indicatorConstraints, bool const &redundantConstraints, storm::storage::SparseMatrix< ValueType > const &matrix, uint64_t mecIndex, storm::storage::MaximalEndComponent const &problematicMec, std::vector< uint64_t > const &relevantObjectiveIndices, std::vector< storm::expressions::Expression > const &choiceVariables, std::vector< std::vector< storm::expressions::Expression > > const &objectiveValueVariables, UpperBoundsGetterType const &objectiveStateUpperBoundGetter)

template<typename ValueType , typename HelperType >
std::vector< storm::expressions::Expression >	expVisitsConstraints (storm::solver::LpSolver< ValueType > &lpModel, bool const &indicatorConstraints, storm::storage::SparseMatrix< ValueType > const &matrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::SparseMatrix< ValueType > const &backwardChoices, uint64_t initialState, std::vector< HelperType > const &objectiveHelper, std::vector< storm::expressions::Expression > const &choiceVariables)

template<typename HelperType >
bool	useFlowEncoding (storm::Environment const &env, std::vector< HelperType > const &objectiveHelper)

template<typename ModelType >
storm::storage::BitVector	evaluatePropositionalFormula (ModelType const &model, storm::logic::Formula const &formula)

template<typename ValueType >
std::vector< ValueType >	getTotalRewardVector (storm::models::sparse::MarkovAutomaton< ValueType > const &model, storm::logic::Formula const &formula)

template<typename ValueType >
std::vector< ValueType >	getTotalRewardVector (storm::models::sparse::Mdp< ValueType > const &model, storm::logic::Formula const &formula)

template<typename ValueType >
void	setLowerUpperTotalRewardBoundsToSolver (storm::solver::AbstractEquationSolver< ValueType > &solver, storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< ValueType > const &rewards, std::vector< ValueType > const &exitProbabilities, std::optional< storm::OptimizationDirection > dir, bool reqLower, bool reqUpper)

template<typename ValueType >
std::vector< ValueType >	computeValuesOfReducedSystem (Environment const &env, storm::storage::SparseMatrix< ValueType > const &submatrix, std::vector< ValueType > const &exitProbs, std::vector< ValueType > const &rewards, storm::OptimizationDirection const &dir)

template<typename ValueType >
void	plusMinMaxSolverPrecision (Environment const &env, ValueType &value)

template<typename ValueType >
void	minusMinMaxSolverPrecision (Environment const &env, ValueType &value)

template<storm::OptimizationDirection Dir, typename ValueType >
ValueType	sumOfMecRewards (storm::storage::MaximalEndComponent const &mec, std::vector< ValueType > const &rewards)

template<typename ValueType >
ValueType	getLowerBoundForNonZeroReachProb (storm::storage::SparseMatrix< ValueType > const &transitions, uint64_t init, uint64_t target)

template<typename GeometryValueType >
bool	closePoints (std::vector< GeometryValueType > const &first, std::vector< GeometryValueType > const &second, GeometryValueType const &maxDistance)

template<typename SparseModelType >
std::unique_ptr< CheckResult >	performMultiObjectiveModelChecking (Environment const &env, SparseModelType const &model, storm::logic::MultiObjectiveFormula const &formula)

template std::unique_ptr< CheckResult >	performMultiObjectiveModelChecking< storm::models::sparse::Mdp< double > > (Environment const &env, storm::models::sparse::Mdp< double > const &model, storm::logic::MultiObjectiveFormula const &formula)

template std::unique_ptr< CheckResult >	performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< double > > (Environment const &env, storm::models::sparse::MarkovAutomaton< double > const &model, storm::logic::MultiObjectiveFormula const &formula)

template std::unique_ptr< CheckResult >	performMultiObjectiveModelChecking< storm::models::sparse::Mdp< storm::RationalNumber > > (Environment const &env, storm::models::sparse::Mdp< storm::RationalNumber > const &model, storm::logic::MultiObjectiveFormula const &formula)

template std::unique_ptr< CheckResult >	performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< storm::RationalNumber > > (Environment const &env, storm::models::sparse::MarkovAutomaton< storm::RationalNumber > const &model, storm::logic::MultiObjectiveFormula const &formula)

std::string	toString (MultiObjectiveMethod m)

template<typename ValueType , typename GeometryValueType >
std::vector< GeometryValueType >	transformObjectiveValuesToOriginal (std::vector< Objective< ValueType > > objectives, std::vector< GeometryValueType > const &point)

template<typename ValueType , typename GeometryValueType >
std::shared_ptr< storm::storage::geometry::Polytope< GeometryValueType > >	transformObjectivePolytopeToOriginal (std::vector< Objective< ValueType > > objectives, std::shared_ptr< storm::storage::geometry::Polytope< GeometryValueType > > const &polytope)

template std::vector< storm::RationalNumber >	transformObjectiveValuesToOriginal (std::vector< Objective< double > > objectives, std::vector< storm::RationalNumber > const &point)

template std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > >	transformObjectivePolytopeToOriginal (std::vector< Objective< double > > objectives, std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > > const &polytope)

template std::vector< storm::RationalNumber >	transformObjectiveValuesToOriginal (std::vector< Objective< storm::RationalNumber > > objectives, std::vector< storm::RationalNumber > const &point)

template std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > >	transformObjectivePolytopeToOriginal (std::vector< Objective< storm::RationalNumber > > objectives, std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > > const &polytope)

template<typename ValueType >
void	computeSchedulerProb1 (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &consideredStates, storm::storage::BitVector const &statesToReach, std::vector< uint64_t > &choices, storm::storage::BitVector const *allowedChoices=nullptr)

template<typename ValueType >
void	computeSchedulerProb0 (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &consideredStates, storm::storage::BitVector const &statesToAvoid, storm::storage::BitVector const &allowedChoices, std::vector< uint64_t > &choices)

template<typename ValueType >
std::vector< uint64_t >	computeValidInitialScheduler (storm::storage::SparseMatrix< ValueType > const &matrix, storm::storage::BitVector const &rowsWithSumLessOne)

template<typename ValueType >
void	computeSchedulerFinitelyOften (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &finitelyOftenChoices, storm::storage::BitVector safeStates, std::vector< uint64_t > &choices)
	Computes a scheduler taking the choices from the given set only finitely often.

Function Documentation

◆ classicConstraints()

template<typename ValueType , typename HelperType >

std::vector< storm::expressions::Expression > storm::modelchecker::multiobjective::classicConstraints	(	storm::solver::LpSolver< ValueType > &	lpModel,
		bool const &	indicatorConstraints,
		storm::storage::SparseMatrix< ValueType > const &	matrix,
		uint64_t	initialState,
		uint64_t	objIndex,
		HelperType const &	objectiveHelper,
		std::vector< storm::expressions::Expression > const &	choiceVariables
	)

Definition at line 166 of file DeterministicSchedsLpChecker.cpp.

◆ closePoints()

template<typename GeometryValueType >

bool storm::modelchecker::multiobjective::closePoints	(	std::vector< GeometryValueType > const &	first,
		std::vector< GeometryValueType > const &	second,
		GeometryValueType const &	maxDistance
	)

Definition at line 550 of file DeterministicSchedsParetoExplorer.cpp.

◆ computeProblematicMecs()

template<typename ValueType , typename ObjHelperType >

auto storm::modelchecker::multiobjective::computeProblematicMecs	(	storm::storage::SparseMatrix< ValueType > const &	matrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		std::vector< ObjHelperType > const &	objectiveHelper
	)

Computes the set of problematic MECS with the objective indices that induced them An EC is problematic if its contained in the "maybestates" of an objective and only considers zero-reward choices.

Definition at line 239 of file DeterministicSchedsLpChecker.cpp.

◆ computeSchedulerFinitelyOften()

template<typename ValueType >

void storm::modelchecker::multiobjective::computeSchedulerFinitelyOften	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	finitelyOftenChoices,
		storm::storage::BitVector	safeStates,
		std::vector< uint64_t > &	choices
	)

Computes a scheduler taking the choices from the given set only finitely often.

Parameters

safeStates it is assumed that reaching such a state is unproblematic. The choice for these states is not set.

Precondition: such a scheduler exists

Definition at line 328 of file StandardPcaaWeightVectorChecker.cpp.

◆ computeSchedulerProb0()

template<typename ValueType >

void storm::modelchecker::multiobjective::computeSchedulerProb0	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	consideredStates,
		storm::storage::BitVector const &	statesToAvoid,
		storm::storage::BitVector const &	allowedChoices,
		std::vector< uint64_t > &	choices
	)

Definition at line 281 of file StandardPcaaWeightVectorChecker.cpp.

◆ computeSchedulerProb1()

template<typename ValueType >

void storm::modelchecker::multiobjective::computeSchedulerProb1	(	storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::BitVector const &	consideredStates,
		storm::storage::BitVector const &	statesToReach,
		std::vector< uint64_t > &	choices,
		storm::storage::BitVector const *	allowedChoices = `nullptr`
	)

Definition at line 238 of file StandardPcaaWeightVectorChecker.cpp.

◆ computeValidInitialScheduler()

template<typename ValueType >

std::vector< uint64_t > storm::modelchecker::multiobjective::computeValidInitialScheduler	(	storm::storage::SparseMatrix< ValueType > const &	matrix,
		storm::storage::BitVector const &	rowsWithSumLessOne
	)

Definition at line 306 of file StandardPcaaWeightVectorChecker.cpp.

◆ computeValuesOfReducedSystem()

template<typename ValueType >

std::vector< ValueType > storm::modelchecker::multiobjective::computeValuesOfReducedSystem	(	Environment const &	env,
		storm::storage::SparseMatrix< ValueType > const &	submatrix,
		std::vector< ValueType > const &	exitProbs,
		std::vector< ValueType > const &	rewards,
		storm::OptimizationDirection const &	dir
	)

Definition at line 361 of file DeterministicSchedsObjectiveHelper.cpp.

◆ createChoiceVariables()

template<typename ValueType >

auto storm::modelchecker::multiobjective::createChoiceVariables	(	storm::solver::LpSolver< ValueType > &	lpModel,
		storm::storage::SparseMatrix< ValueType > const &	matrix
	)

Definition at line 145 of file DeterministicSchedsLpChecker.cpp.

◆ evaluatePropositionalFormula()

template<typename ModelType >

storm::storage::BitVector storm::modelchecker::multiobjective::evaluatePropositionalFormula	(	ModelType const &	model,
		storm::logic::Formula const &	formula
	)

Definition at line 37 of file DeterministicSchedsObjectiveHelper.cpp.

◆ expVisitsConstraints()

template<typename ValueType , typename HelperType >

std::vector< storm::expressions::Expression > storm::modelchecker::multiobjective::expVisitsConstraints	(	storm::solver::LpSolver< ValueType > &	lpModel,
		bool const &	indicatorConstraints,
		storm::storage::SparseMatrix< ValueType > const &	matrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardTransitions,
		storm::storage::SparseMatrix< ValueType > const &	backwardChoices,
		uint64_t	initialState,
		std::vector< HelperType > const &	objectiveHelper,
		std::vector< storm::expressions::Expression > const &	choiceVariables
	)

Definition at line 433 of file DeterministicSchedsLpChecker.cpp.

◆ getLowerBoundForNonZeroReachProb()

template<typename ValueType >

ValueType storm::modelchecker::multiobjective::getLowerBoundForNonZeroReachProb	(	storm::storage::SparseMatrix< ValueType > const &	transitions,
		uint64_t	init,
		uint64_t	target
	)

Definition at line 468 of file DeterministicSchedsObjectiveHelper.cpp.

◆ getTotalRewardVector() [1/2]

template<typename ValueType >

std::vector< ValueType > storm::modelchecker::multiobjective::getTotalRewardVector	(	storm::models::sparse::MarkovAutomaton< ValueType > const &	model,
		storm::logic::Formula const &	formula
	)

Definition at line 46 of file DeterministicSchedsObjectiveHelper.cpp.

◆ getTotalRewardVector() [2/2]

template<typename ValueType >

std::vector< ValueType > storm::modelchecker::multiobjective::getTotalRewardVector	(	storm::models::sparse::Mdp< ValueType > const &	model,
		storm::logic::Formula const &	formula
	)

Definition at line 71 of file DeterministicSchedsObjectiveHelper.cpp.

◆ minusMinMaxSolverPrecision()

template<typename ValueType >

void storm::modelchecker::multiobjective::minusMinMaxSolverPrecision	(	Environment const &	env,
		ValueType &	value
	)

Definition at line 443 of file DeterministicSchedsObjectiveHelper.cpp.

◆ performMultiObjectiveModelChecking()

template<typename SparseModelType >

std::unique_ptr< CheckResult > storm::modelchecker::multiobjective::performMultiObjectiveModelChecking	(	Environment const &	env,
		SparseModelType const &	model,
		storm::logic::MultiObjectiveFormula const &	formula
	)

Definition at line 27 of file multiObjectiveModelChecking.cpp.

◆ performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< double > >()

template std::unique_ptr< CheckResult > storm::modelchecker::multiobjective::performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< double > >	(	Environment const &	env,
		storm::models::sparse::MarkovAutomaton< double > const &	model,
		storm::logic::MultiObjectiveFormula const &	formula
	)

◆ performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< storm::RationalNumber > >()

template std::unique_ptr< CheckResult > storm::modelchecker::multiobjective::performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< storm::RationalNumber > >	(	Environment const &	env,
		storm::models::sparse::MarkovAutomaton< storm::RationalNumber > const &	model,
		storm::logic::MultiObjectiveFormula const &	formula
	)

◆ performMultiObjectiveModelChecking< storm::models::sparse::Mdp< double > >()

template std::unique_ptr< CheckResult > storm::modelchecker::multiobjective::performMultiObjectiveModelChecking< storm::models::sparse::Mdp< double > >	(	Environment const &	env,
		storm::models::sparse::Mdp< double > const &	model,
		storm::logic::MultiObjectiveFormula const &	formula
	)

◆ performMultiObjectiveModelChecking< storm::models::sparse::Mdp< storm::RationalNumber > >()

template std::unique_ptr< CheckResult > storm::modelchecker::multiobjective::performMultiObjectiveModelChecking< storm::models::sparse::Mdp< storm::RationalNumber > >	(	Environment const &	env,
		storm::models::sparse::Mdp< storm::RationalNumber > const &	model,
		storm::logic::MultiObjectiveFormula const &	formula
	)

◆ plusMinMaxSolverPrecision()

template<typename ValueType >

void storm::modelchecker::multiobjective::plusMinMaxSolverPrecision	(	Environment const &	env,
		ValueType &	value
	)

Definition at line 431 of file DeterministicSchedsObjectiveHelper.cpp.

◆ problematicMecConstraintsExpVisits()

template<typename ValueType , typename UpperBoundsGetterType >

auto storm::modelchecker::multiobjective::problematicMecConstraintsExpVisits	(	storm::solver::LpSolver< ValueType > &	lpModel,
		bool const &	indicatorConstraints,
		bool const &	redundantConstraints,
		storm::storage::SparseMatrix< ValueType > const &	matrix,
		storm::storage::SparseMatrix< ValueType > const &	backwardChoices,
		uint64_t	mecIndex,
		storm::storage::MaximalEndComponent const &	problematicMec,
		std::vector< uint64_t > const &	relevantObjectiveIndices,
		std::vector< std::vector< storm::expressions::Expression > > const &	objectiveValueVariables,
		std::vector< storm::expressions::Expression > const &	choiceVariables,
		UpperBoundsGetterType const &	objectiveStateUpperBoundGetter
	)

Definition at line 265 of file DeterministicSchedsLpChecker.cpp.

◆ problematicMecConstraintsOrder()

template<typename ValueType , typename UpperBoundsGetterType >

auto storm::modelchecker::multiobjective::problematicMecConstraintsOrder	(	storm::solver::LpSolver< ValueType > &	lpModel,
		bool const &	indicatorConstraints,
		bool const &	redundantConstraints,
		storm::storage::SparseMatrix< ValueType > const &	matrix,
		uint64_t	mecIndex,
		storm::storage::MaximalEndComponent const &	problematicMec,
		std::vector< uint64_t > const &	relevantObjectiveIndices,
		std::vector< storm::expressions::Expression > const &	choiceVariables,
		std::vector< std::vector< storm::expressions::Expression > > const &	objectiveValueVariables,
		UpperBoundsGetterType const &	objectiveStateUpperBoundGetter
	)

Definition at line 366 of file DeterministicSchedsLpChecker.cpp.

◆ setLowerUpperTotalRewardBoundsToSolver()

template<typename ValueType >

void storm::modelchecker::multiobjective::setLowerUpperTotalRewardBoundsToSolver	(	storm::solver::AbstractEquationSolver< ValueType > &	solver,
		storm::storage::SparseMatrix< ValueType > const &	matrix,
		std::vector< ValueType > const &	rewards,
		std::vector< ValueType > const &	exitProbabilities,
		std::optional< storm::OptimizationDirection >	dir,
		bool	reqLower,
		bool	reqUpper
	)

Definition at line 303 of file DeterministicSchedsObjectiveHelper.cpp.

◆ sumOfMecRewards()

template<storm::OptimizationDirection Dir, typename ValueType >

ValueType storm::modelchecker::multiobjective::sumOfMecRewards	(	storm::storage::MaximalEndComponent const &	mec,
		std::vector< ValueType > const &	rewards
	)

Definition at line 455 of file DeterministicSchedsObjectiveHelper.cpp.

◆ toString()

std::string storm::modelchecker::multiobjective::toString ( MultiObjectiveMethod m )

Definition at line 7 of file MultiObjectiveModelCheckingMethod.cpp.

◆ transformObjectivePolytopeToOriginal() [1/3]

template std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > > storm::modelchecker::multiobjective::transformObjectivePolytopeToOriginal	(	std::vector< Objective< double > >	objectives,
		std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > > const &	polytope
	)

◆ transformObjectivePolytopeToOriginal() [2/3]

template std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > > storm::modelchecker::multiobjective::transformObjectivePolytopeToOriginal	(	std::vector< Objective< storm::RationalNumber > >	objectives,
		std::shared_ptr< storm::storage::geometry::Polytope< storm::RationalNumber > > const &	polytope
	)

◆ transformObjectivePolytopeToOriginal() [3/3]

template<typename ValueType , typename GeometryValueType >

std::shared_ptr< storm::storage::geometry::Polytope< GeometryValueType > > storm::modelchecker::multiobjective::transformObjectivePolytopeToOriginal	(	std::vector< Objective< ValueType > >	objectives,
		std::shared_ptr< storm::storage::geometry::Polytope< GeometryValueType > > const &	polytope
	)

Definition at line 33 of file MultiObjectivePostprocessing.cpp.

◆ transformObjectiveValuesToOriginal() [1/3]

template std::vector< storm::RationalNumber > storm::modelchecker::multiobjective::transformObjectiveValuesToOriginal	(	std::vector< Objective< double > >	objectives,
		std::vector< storm::RationalNumber > const &	point
	)

◆ transformObjectiveValuesToOriginal() [2/3]

template std::vector< storm::RationalNumber > storm::modelchecker::multiobjective::transformObjectiveValuesToOriginal	(	std::vector< Objective< storm::RationalNumber > >	objectives,
		std::vector< storm::RationalNumber > const &	point
	)

◆ transformObjectiveValuesToOriginal() [3/3]

template<typename ValueType , typename GeometryValueType >

std::vector< GeometryValueType > storm::modelchecker::multiobjective::transformObjectiveValuesToOriginal	(	std::vector< Objective< ValueType > >	objectives,
		std::vector< GeometryValueType > const &	point
	)

Definition at line 10 of file MultiObjectivePostprocessing.cpp.

◆ useFlowEncoding()

template<typename HelperType >

bool storm::modelchecker::multiobjective::useFlowEncoding	(	storm::Environment const &	env,
		std::vector< HelperType > const &	objectiveHelper
	)

Definition at line 562 of file DeterministicSchedsLpChecker.cpp.

Namespaces

Classes

Functions

Function Documentation

◆ classicConstraints()

◆ closePoints()

◆ computeProblematicMecs()

◆ computeSchedulerFinitelyOften()

◆ computeSchedulerProb0()

◆ computeSchedulerProb1()

◆ computeValidInitialScheduler()

◆ computeValuesOfReducedSystem()

◆ createChoiceVariables()

◆ evaluatePropositionalFormula()

◆ expVisitsConstraints()

◆ getLowerBoundForNonZeroReachProb()

◆ getTotalRewardVector() [1/2]

◆ getTotalRewardVector() [2/2]

◆ minusMinMaxSolverPrecision()

◆ performMultiObjectiveModelChecking()

◆ performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< double > >()

◆ performMultiObjectiveModelChecking< storm::models::sparse::MarkovAutomaton< storm::RationalNumber > >()

◆ performMultiObjectiveModelChecking< storm::models::sparse::Mdp< double > >()

◆ performMultiObjectiveModelChecking< storm::models::sparse::Mdp< storm::RationalNumber > >()

◆ plusMinMaxSolverPrecision()

◆ problematicMecConstraintsExpVisits()

◆ problematicMecConstraintsOrder()

◆ setLowerUpperTotalRewardBoundsToSolver()

◆ sumOfMecRewards()

◆ toString()

◆ transformObjectivePolytopeToOriginal() [1/3]

◆ transformObjectivePolytopeToOriginal() [2/3]

◆ transformObjectivePolytopeToOriginal() [3/3]

◆ transformObjectiveValuesToOriginal() [1/3]

◆ transformObjectiveValuesToOriginal() [2/3]

◆ transformObjectiveValuesToOriginal() [3/3]

◆ useFlowEncoding()