HybridMdpPrctlHelper.cpp File Reference

#include "storm/modelchecker/prctl/helper/HybridMdpPrctlHelper.h"
#include "storm/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/dd/Add.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdManager.h"
#include "storm/storage/dd/Odd.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
#include "storm/modelchecker/prctl/helper/SparseMdpEndComponentInformation.h"
#include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/multiplier/Multiplier.h"
#include "storm/utility/Stopwatch.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/UncheckedRequirementException.h"

Include dependency graph for HybridMdpPrctlHelper.cpp:

Go to the source code of this file.

Classes
struct	storm::modelchecker::helper::SolverRequirementsData< ValueType >

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

Functions
template<typename ValueType >
std::vector< uint64_t >	storm::modelchecker::helper::computeValidInitialSchedulerForUntilProbabilities (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< ValueType > const &b)
template<typename ValueType >
void	storm::modelchecker::helper::eliminateExtendedStatesFromExplicitRepresentation (std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &explicitRepresentation, boost::optional< std::vector< uint64_t > > &scheduler, storm::storage::BitVector const &properMaybeStates)
template<typename ValueType >
void	storm::modelchecker::helper::eliminateEndComponentsAndExtendedStatesUntilProbabilities (std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &explicitRepresentation, SolverRequirementsData< ValueType > &solverRequirementsData, storm::storage::BitVector const &targetStates)
template<typename ValueType >
storm::storage::BitVector	storm::modelchecker::helper::computeTargetStatesForReachabilityRewardsFromExplicitRepresentation (storm::storage::SparseMatrix< ValueType > const &transitionMatrix)
template<typename ValueType >
std::vector< uint64_t >	storm::modelchecker::helper::computeValidInitialSchedulerForReachabilityRewards (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &properMaybeStates, storm::storage::BitVector const &targetStates)
template<typename ValueType >
std::vector< ValueType >	storm::modelchecker::helper::computeOneStepTargetProbabilitiesFromExtendedExplicitRepresentation (storm::storage::SparseMatrix< ValueType > const &extendedMatrix, storm::storage::BitVector const &properMaybeStates, storm::storage::BitVector const &targetStates)
template<typename ValueType >
void	storm::modelchecker::helper::eliminateEndComponentsAndTargetStatesReachabilityRewards (std::pair< storm::storage::SparseMatrix< ValueType >, std::vector< ValueType > > &explicitRepresentation, SolverRequirementsData< ValueType > &solverRequirementsData, storm::storage::BitVector const &targetStates, bool computeOneStepTargetProbabilities)
template<typename ValueType >
void	storm::modelchecker::helper::setUpperRewardBounds (storm::solver::MinMaxLinearEquationSolver< ValueType > &solver, storm::OptimizationDirection const &direction, storm::storage::SparseMatrix< ValueType > const &submatrix, std::vector< ValueType > const &choiceRewards, std::vector< ValueType > const &oneStepTargetProbabilities)