#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
#include <boost/container/flat_map.hpp>
#include "storm/modelchecker/prctl/helper/SemanticSolutionType.h"
#include "storm/modelchecker/hints/ExplicitModelCheckerHint.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/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/utility/graph.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Variable.h"
#include "storm/solver/LpSolver.h"
#include "storm/solver/MinMaxLinearEquationSolver.h"
#include "storm/solver/multiplier/Multiplier.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/IOSettings.h"
#include "storm/settings/modules/ModelCheckerSettings.h"
#include "storm/io/export.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/ProgressMeasurement.h"
#include "storm/utility/SignalHandler.h"
#include "storm/utility/Stopwatch.h"
#include "storm/transformer/EndComponentEliminator.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/exceptions/IllegalArgumentException.h"
#include "storm/exceptions/IllegalFunctionCallException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/InvalidSettingsException.h"
#include "storm/exceptions/InvalidStateException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/exceptions/UncheckedRequirementException.h"

Include dependency graph for SparseMdpPrctlHelper.cpp:

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

struct	storm::modelchecker::helper::MaybeStateResult< ValueType >

struct	storm::modelchecker::helper::QualitativeStateSetsUntilProbabilities

struct	storm::modelchecker::helper::QualitativeStateSetsReachabilityRewards

Namespaces
namespace	storm
	LabParser.cpp.

namespace	storm::modelchecker

namespace	storm::modelchecker::helper

Functions
template<typename ValueType , typename SolutionType = ValueType>
std::vector< uint_fast64_t >	storm::modelchecker::helper::computeValidSchedulerHint (Environment const &env, SemanticSolutionType const &type, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &filterStates, storm::storage::BitVector const &targetStates, boost::optional< storm::storage::BitVector > const &selectedChoices)

template<typename ValueType , typename SolutionType >
void	storm::modelchecker::helper::extractValueAndSchedulerHint (SparseMdpHintType< SolutionType > &hintStorage, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, boost::optional< storm::storage::BitVector > const &selectedChoices, ModelCheckerHint const &hint, bool skipECWithinMaybeStatesCheck)

template<typename ValueType , typename SolutionType >
SparseMdpHintType< SolutionType >	storm::modelchecker::helper::computeHints (Environment const &env, SemanticSolutionType const &type, ModelCheckerHint const &hint, storm::OptimizationDirection const &dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &targetStates, bool produceScheduler, boost::optional< storm::storage::BitVector > const &selectedChoices=boost::none)

template<typename ValueType , typename SolutionType >
MaybeStateResult< SolutionType >	storm::modelchecker::helper::computeValuesForMaybeStates (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, storm::storage::SparseMatrix< ValueType > &&submatrix, std::vector< ValueType > const &b, bool produceScheduler, SparseMdpHintType< SolutionType > &hint)

template<typename ValueType >
QualitativeStateSetsUntilProbabilities	storm::modelchecker::helper::getQualitativeStateSetsUntilProbabilitiesFromHint (ModelCheckerHint const &hint)

template<typename ValueType , typename SolutionType >
QualitativeStateSetsUntilProbabilities	storm::modelchecker::helper::computeQualitativeStateSetsUntilProbabilities (storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)

template<typename ValueType , typename SolutionType >
QualitativeStateSetsUntilProbabilities	storm::modelchecker::helper::getQualitativeStateSetsUntilProbabilities (storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, ModelCheckerHint const &hint)

template<typename SolutionType , bool subChoicesCoverOnlyMaybeStates = true>
void	storm::modelchecker::helper::extractSchedulerChoices (storm::storage::Scheduler< SolutionType > &scheduler, std::vector< uint64_t > const &subChoices, storm::storage::BitVector const &maybeStates)

template<typename ValueType , typename SolutionType >
void	storm::modelchecker::helper::extendScheduler (storm::storage::Scheduler< SolutionType > &scheduler, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)

template<typename ValueType , typename SolutionType >
void	storm::modelchecker::helper::computeFixedPointSystemUntilProbabilities (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b)

template<typename ValueType , typename SolutionType >
boost::optional< SparseMdpEndComponentInformation< ValueType > >	storm::modelchecker::helper::computeFixedPointSystemUntilProbabilitiesEliminateEndComponents (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsUntilProbabilities const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, bool produceScheduler)

template<typename ValueType >
QualitativeStateSetsReachabilityRewards	storm::modelchecker::helper::getQualitativeStateSetsReachabilityRewardsFromHint (ModelCheckerHint const &hint, storm::storage::BitVector const &targetStates)

template<typename ValueType , typename SolutionType >
QualitativeStateSetsReachabilityRewards	storm::modelchecker::helper::computeQualitativeStateSetsReachabilityRewards (storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)

template<typename ValueType , typename SolutionType >
QualitativeStateSetsReachabilityRewards	storm::modelchecker::helper::getQualitativeStateSetsReachabilityRewards (storm::solver::SolveGoal< ValueType, SolutionType > const &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, ModelCheckerHint const &hint, std::function< storm::storage::BitVector()> const &zeroRewardStatesGetter, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)

template<typename ValueType , typename SolutionType >
void	storm::modelchecker::helper::extendScheduler (storm::storage::Scheduler< SolutionType > &scheduler, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, std::function< storm::storage::BitVector()> const &zeroRewardChoicesGetter)

template<typename ValueType , typename SolutionType >
void	storm::modelchecker::helper::extractSchedulerChoices (storm::storage::Scheduler< SolutionType > &scheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint_fast64_t > const &subChoices, storm::storage::BitVector const &maybeStates, boost::optional< storm::storage::BitVector > const &selectedChoices)

template<typename ValueType , typename SolutionType >
void	storm::modelchecker::helper::computeFixedPointSystemReachabilityRewards (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, std::vector< ValueType > *oneStepTargetProbabilities=nullptr)

template<typename ValueType , typename SolutionType >
boost::optional< SparseMdpEndComponentInformation< ValueType > >	storm::modelchecker::helper::computeFixedPointSystemReachabilityRewardsEliminateEndComponents (storm::solver::SolveGoal< ValueType, SolutionType > &goal, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, QualitativeStateSetsReachabilityRewards const &qualitativeStateSets, boost::optional< storm::storage::BitVector > const &selectedChoices, std::function< std::vector< ValueType >(uint_fast64_t, storm::storage::SparseMatrix< ValueType > const &, storm::storage::BitVector const &)> const &totalStateRewardVectorGetter, storm::storage::SparseMatrix< ValueType > &submatrix, std::vector< ValueType > &b, boost::optional< std::vector< ValueType > > &oneStepTargetProbabilities, bool produceScheduler)

template<typename ValueType , typename SolutionType >
void	storm::modelchecker::helper::computeUpperRewardBounds (SparseMdpHintType< SolutionType > &hintInformation, storm::OptimizationDirection const &direction, storm::storage::SparseMatrix< ValueType > const &submatrix, std::vector< ValueType > const &choiceRewards, std::vector< ValueType > const &oneStepTargetProbabilities)

Classes

Namespaces

Functions