StandardPcaaWeightVectorChecker.cpp File Reference

#include "storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h"
#include <map>
#include <set>
#include "storm/logic/Formulas.h"
#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectiveRewardAnalysis.h"
#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/transformer/GoalStateMerger.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/exceptions/IllegalFunctionCallException.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UncheckedRequirementException.h"
#include "storm/exceptions/UnexpectedException.h"

Include dependency graph for StandardPcaaWeightVectorChecker.cpp:

Go to the source code of this file.

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

Functions
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)
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)
template<typename ValueType >
std::vector< uint64_t >	storm::modelchecker::multiobjective::computeValidInitialScheduler (storm::storage::SparseMatrix< ValueType > const &matrix, storm::storage::BitVector const &rowsWithSumLessOne)
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.