#include "storm/modelchecker/helper/conditional/ConditionalHelper.h"
#include <algorithm>
#include <stack>
#include "storm/adapters/RationalNumberAdapter.h"
#include "storm/adapters/RationalNumberForward.h"
#include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h"
#include "storm/environment/modelchecker/ModelCheckerEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/solver/SolveGoal.h"
#include "storm/storage/BitVector.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/StronglyConnectedComponentDecomposition.h"
#include "storm/transformer/EndComponentEliminator.h"
#include "storm/utility/Extremum.h"
#include "storm/utility/NumberTraits.h"
#include "storm/utility/OptionalRef.h"
#include "storm/utility/RationalApproximation.h"
#include "storm/utility/SignalHandler.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/utility/logging.h"
#include "storm/utility/macros.h"

Include dependency graph for ConditionalHelper.cpp:

Classes
struct	storm::modelchecker::internal::NormalFormData< ValueType >
struct	storm::modelchecker::internal::ResultReturnType< ValueType, SolutionType >
class	storm::modelchecker::internal::WeightedReachabilityHelper< ValueType, SolutionType >
	A helper class that computes (weighted) reachability probabilities for a given MDP in normal form. More...

Namespaces
namespace	storm
namespace	storm::modelchecker
namespace	storm::modelchecker::internal

Functions
template<typename ValueType>
std::optional< typename storm::transformer::EndComponentEliminator< ValueType >::EndComponentEliminatorReturnType >	storm::modelchecker::internal::eliminateEndComponents (storm::storage::BitVector const &possibleEcStates, bool addRowAtRepresentativeState, std::optional< uint64_t > const representativeRowEntry, storm::storage::SparseMatrix< ValueType > &matrix, storm::storage::BitVector &rowsWithSum1, std::vector< ValueType > &rowValues1, storm::OptionalRef< std::vector< ValueType > > rowValues2={})
template<typename ValueType, typename SolutionType = ValueType>
SolutionType	storm::modelchecker::internal::solveMinMaxEquationSystem (storm::Environment const &env, storm::storage::SparseMatrix< ValueType > const &matrix, std::vector< ValueType > const &rowValues, storm::storage::BitVector const &rowsWithSum1, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, uint64_t const initialState, std::optional< std::vector< uint64_t > > &schedulerOutput)
template<typename ValueType>
std::unique_ptr< storm::storage::Scheduler< ValueType > >	storm::modelchecker::internal::computeReachabilityProbabilities (Environment const &env, std::map< uint64_t, ValueType > &nonZeroResults, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &allowedStates, storm::storage::BitVector const &targetStates, bool computeScheduler=true)
	Computes the reachability probabilities for the given target states and inserts all non-zero values into the given map.
template<typename ValueType>
NormalFormData< ValueType >	storm::modelchecker::internal::obtainNormalForm (Environment const &env, storm::solver::OptimizationDirection const dir, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &relevantStates, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
template<typename ValueType, typename SolutionType = ValueType>
void	storm::modelchecker::internal::finalizeSchedulerForMaybeStates (storm::storage::Scheduler< SolutionType > &scheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &maybeStates, storm::storage::BitVector const &maybeStatesWithoutChoice, storm::storage::BitVector const &maybeStatesWithChoice, std::vector< uint64_t > const &stateToFinalEc, NormalFormData< ValueType > const &normalForm, uint64_t initialComponentIndex, storm::storage::BitVector const &initialComponentExitStates, storm::storage::BitVector const &initialComponentExitRows, uint64_t chosenInitialComponentExitState, uint64_t chosenInitialComponentExit)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	storm::modelchecker::internal::computeViaRestartMethod (Environment const &env, uint64_t const initialState, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
	Uses the restart method by Baier et al.
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	storm::modelchecker::internal::computeViaBisection (Environment const &env, bool const useAdvancedBounds, bool const usePolicyTracking, uint64_t const initialState, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	storm::modelchecker::internal::computeViaBisection (Environment const &env, ConditionalAlgorithmSetting const alg, uint64_t const initialState, storm::solver::SolveGoal< ValueType, SolutionType > const &goal, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< ValueType >	storm::modelchecker::internal::decideThreshold (Environment const &env, uint64_t const initialState, storm::OptimizationDirection const &direction, SolutionType const &threshold, bool computeScheduler, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType = ValueType>
internal::ResultReturnType< SolutionType >	storm::modelchecker::internal::computeViaPolicyIteration (Environment const &env, uint64_t const initialState, storm::solver::OptimizationDirection const dir, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType = ValueType>
std::optional< SolutionType >	storm::modelchecker::internal::handleTrivialCases (uint64_t const initialState, NormalFormData< ValueType > const &normalForm)
template<typename ValueType, typename SolutionType>
std::unique_ptr< CheckResult >	storm::modelchecker::computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< ValueType, SolutionType > &&goal, bool produceSchedulers, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::SparseMatrix< ValueType > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
template std::unique_ptr< CheckResult >	storm::modelchecker::computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< double > &&goal, bool produceSchedulers, storm::storage::SparseMatrix< double > const &transitionMatrix, storm::storage::SparseMatrix< double > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)
template std::unique_ptr< CheckResult >	storm::modelchecker::computeConditionalProbabilities (Environment const &env, storm::solver::SolveGoal< storm::RationalNumber > &&goal, bool produceSchedulers, storm::storage::SparseMatrix< storm::RationalNumber > const &transitionMatrix, storm::storage::SparseMatrix< storm::RationalNumber > const &backwardTransitions, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &conditionStates)

Classes

Namespaces

Functions