DeterministicSchedsObjectiveHelper.cpp File Reference

#include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsObjectiveHelper.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/multiobjective/deterministicScheds/VisitingTimesHelper.h"
#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/solver/LinearEquationSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/transformer/EndComponentEliminator.h"
#include "storm/utility/Extremum.h"
#include "storm/utility/FilteredRewardModel.h"
#include "storm/utility/graph.h"
#include "storm/utility/vector.h"
#include "storm/exceptions/UncheckedRequirementException.h"
#include "storm/exceptions/UnexpectedException.h"

Include dependency graph for DeterministicSchedsObjectiveHelper.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::modelchecker
namespace	storm::modelchecker::multiobjective

Functions
template<typename ModelType >
storm::storage::BitVector	storm::modelchecker::multiobjective::evaluatePropositionalFormula (ModelType const &model, storm::logic::Formula const &formula)
template<typename ValueType >
std::vector< ValueType >	storm::modelchecker::multiobjective::getTotalRewardVector (storm::models::sparse::MarkovAutomaton< ValueType > const &model, storm::logic::Formula const &formula)
template<typename ValueType >
std::vector< ValueType >	storm::modelchecker::multiobjective::getTotalRewardVector (storm::models::sparse::Mdp< ValueType > const &model, storm::logic::Formula const &formula)
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)
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)
template<typename ValueType >
void	storm::modelchecker::multiobjective::plusMinMaxSolverPrecision (Environment const &env, ValueType &value)
template<typename ValueType >
void	storm::modelchecker::multiobjective::minusMinMaxSolverPrecision (Environment const &env, ValueType &value)
template<storm::OptimizationDirection Dir, typename ValueType >
ValueType	storm::modelchecker::multiobjective::sumOfMecRewards (storm::storage::MaximalEndComponent const &mec, std::vector< ValueType > const &rewards)
template<typename ValueType >
ValueType	storm::modelchecker::multiobjective::getLowerBoundForNonZeroReachProb (storm::storage::SparseMatrix< ValueType > const &transitions, uint64_t init, uint64_t target)