QuantileHelper.cpp File Reference

#include "storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h"
#include <boost/optional.hpp>
#include <memory>
#include <set>
#include <vector>
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/Expressions.h"
#include "storm/utility/vector.h"
#include "storm/logic/BoundedUntilFormula.h"
#include "storm/logic/ProbabilityOperatorFormula.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UnexpectedException.h"

Include dependency graph for QuantileHelper.cpp:

Go to the source code of this file.

Namespaces
namespace	storm
namespace	storm::modelchecker
namespace	storm::modelchecker::helper
namespace	storm::modelchecker::helper::rewardbounded

Enumerations
enum class	storm::modelchecker::helper::rewardbounded::BoundTransformation { storm::modelchecker::helper::rewardbounded::None , storm::modelchecker::helper::rewardbounded::GreaterZero , storm::modelchecker::helper::rewardbounded::GreaterEqualZero , storm::modelchecker::helper::rewardbounded::LessEqualZero }

Functions
std::shared_ptr< storm::logic::ProbabilityOperatorFormula >	storm::modelchecker::helper::rewardbounded::transformBoundedUntilOperator (storm::logic::ProbabilityOperatorFormula const &boundedUntilOperator, std::vector< BoundTransformation > const &transformations, bool complementQuery=false)
void	storm::modelchecker::helper::rewardbounded::increasePrecision (storm::Environment &env)
	Increases the precision of solver results.
template<typename ValueType>
std::pair< ValueType, ValueType >	storm::modelchecker::helper::rewardbounded::getLowerUpperBound (storm::Environment const &env, ValueType const &factor, ValueType const &value, bool minMax=true)
	Computes a lower / upper bound on the actual result of a sound minmax or linear equation solver.
bool	storm::modelchecker::helper::rewardbounded::getNextCandidateCostLimit (CostLimit const &candidateCostLimitSum, CostLimits &current)
bool	storm::modelchecker::helper::rewardbounded::translateEpochToCostLimits (EpochManager::Epoch const &epoch, EpochManager::Epoch const &startEpoch, storm::storage::BitVector const &consideredDimensions, storm::storage::BitVector const &lowerBoundedDimensions, EpochManager const &epochManager, CostLimits &epochAsCostLimits)