graph.h File Reference

#include <limits>
#include <set>
#include <storm/storage/StronglyConnectedComponent.h>
#include "storm/utility/OsDetection.h"
#include "storm/models/sparse/DeterministicModel.h"
#include "storm/models/sparse/NondeterministicModel.h"
#include "storm/storage/Scheduler.h"
#include "storm/storage/sparse/StateType.h"
#include "storm/storage/dd/Bdd.h"
#include "storm/storage/dd/DdType.h"
#include "storm/solver/OptimizationDirection.h"

Include dependency graph for graph.h:

Go to the source code of this file.

Classes
struct	storm::utility::graph::SymbolicGameProb01Result< Type >
struct	storm::utility::graph::ExplicitGameProb01Result

Namespaces
namespace	storm
	LabParser.cpp.
namespace	storm::storage
namespace	storm::models
namespace	storm::models::symbolic
namespace	storm::dd
namespace	storm::utility
namespace	storm::utility::graph

Functions
template<typename T >
storm::storage::BitVector	storm::utility::graph::getReachableOneStep (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates)
	Computes the states reachable in one step from the states indicated by the bitvector.
template<typename T >
storm::storage::BitVector	storm::utility::graph::getReachableStates (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, bool useStepBound=false, uint_fast64_t maximalSteps=0, boost::optional< storm::storage::BitVector > const &choiceFilter=boost::none)
	Performs a forward depth-first search through the underlying graph structure to identify the states that are reachable from the given set only passing through a constrained set of states until some target have been reached.
template<typename T >
storm::storage::BitVector	storm::utility::graph::getBsccCover (storm::storage::SparseMatrix< T > const &transitionMatrix)
	Retrieves a set of states that covers als BSCCs of the system in the sense that for every BSCC exactly one state is included in the cover.
template<typename T >
bool	storm::utility::graph::hasCycle (storm::storage::SparseMatrix< T > const &transitionMatrix, boost::optional< storm::storage::BitVector > const &subsystem=boost::none)
	Returns true if the graph represented by the given matrix has a cycle.
template<typename T >
bool	storm::utility::graph::checkIfECWithChoiceExists (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &subsystem, storm::storage::BitVector const &choices)
	Checks whether there is an End Component that.
template<typename T >
std::vector< uint_fast64_t >	storm::utility::graph::getDistances (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::BitVector const &initialStates, boost::optional< storm::storage::BitVector > const &subsystem=boost::none)
	Performs a breadth-first search through the underlying graph structure to compute the distance from all states to the starting states of the search.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProbGreater0 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0)
	Performs a backward depth-first search trough the underlying graph structure of the given model to determine which states of the model have a positive probability of satisfying phi until psi.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProb1 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::BitVector const &statesWithProbabilityGreater0)
	Computes the set of states of the given model for which all paths lead to the given set of target states and only visit states from the filter set before.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProb1 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the set of states of the given model for which all paths lead to the given set of target states and only visit states from the filter set before.
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	storm::utility::graph::performProb01 (storm::models::sparse::DeterministicModel< T > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	storm::utility::graph::performProb01 (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProbGreater0 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, boost::optional< uint_fast64_t > const &stepBound=boost::optional< uint_fast64_t >())
	Computes the set of states that has a positive probability of reaching psi states after only passing through phi states before.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProb1 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbabilityGreater0)
	Computes the set of states that have a probability of one of reaching psi states after only passing through phi states before.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProb1 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes the set of states that have a probability of one of reaching psi states after only passing through phi states before.
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > >	storm::utility::graph::performProb01 (storm::models::symbolic::DeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > >	storm::utility::graph::performProb01 (storm::models::symbolic::Model< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a deterministic model.
template<typename T , typename SchedulerValueType >
void	storm::utility::graph::computeSchedulerStayingInStates (storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter=boost::none)
	Computes a scheduler for the given states that chooses an action that stays completely in the very same set.
template<typename T >
void	storm::utility::graph::computeSchedulerWithOneSuccessorInStates (storm::storage::BitVector const &states, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< T > &scheduler)
	Computes a scheduler for the given states that chooses an action that has at least one successor in the given set of states.
template<typename T , typename SchedulerValueType >
void	storm::utility::graph::computeSchedulerProbGreater0E (storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter=boost::none)
	Computes a scheduler for the ProbGreater0E-States such that in the induced system the given psiStates are reachable via phiStates.
template<typename T , typename SchedulerValueType >
void	storm::utility::graph::computeSchedulerRewInf (storm::storage::BitVector const &rewInfStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::Scheduler< SchedulerValueType > &scheduler)
	Computes a scheduler for the given states that have a scheduler that has a reward infinity.
template<typename T , typename SchedulerValueType >
void	storm::utility::graph::computeSchedulerProb0E (storm::storage::BitVector const &prob0EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::Scheduler< SchedulerValueType > &scheduler)
	Computes a scheduler for the given states that have a scheduler that has a probability 0.
template<typename T , typename SchedulerValueType >
void	storm::utility::graph::computeSchedulerProb1E (storm::storage::BitVector const &prob1EStates, storm::storage::SparseMatrix< T > const &transitionMatrix, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::storage::Scheduler< SchedulerValueType > &scheduler, boost::optional< storm::storage::BitVector > const &rowFilter=boost::none)
	Computes a scheduler for the given prob1EStates such that in the induced system the given psiStates are reached with probability 1.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProbGreater0E (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0)
	Computes the sets of states that have probability greater 0 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProb0A (storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProb1E (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, boost::optional< storm::storage::BitVector > const &choiceConstraint=boost::none)
	Computes the sets of states that have probability 1 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
template<typename T , typename RM >
storm::storage::BitVector	storm::utility::graph::performProb1E (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the sets of states that have probability 1 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	storm::utility::graph::performProb01Max (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	storm::utility::graph::performProb01Max (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a non-deterministic model in which all non-deterministic choices are resolved such that the probability is maximized.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProbGreater0A (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, bool useStepBound=false, uint_fast64_t maximalSteps=0, boost::optional< storm::storage::BitVector > const &choiceConstraint=boost::none)
	Computes the sets of states that have probability greater 0 of satisfying phi until psi under any possible resolution of non-determinism in a non-deterministic model.
template<typename T , typename RM >
storm::storage::BitVector	storm::utility::graph::performProb0E (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the sets of states that have probability 0 of satisfying phi until psi under at least one possible resolution of non-determinism in a non-deterministic model.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProb0E (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
template<typename T , typename RM >
storm::storage::BitVector	storm::utility::graph::performProb1A (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the sets of states that have probability 1 of satisfying phi until psi under all possible resolutions of non-determinism in a non-deterministic model.
template<typename T >
storm::storage::BitVector	storm::utility::graph::performProb1A (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
template<typename T >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	storm::utility::graph::performProb01Min (storm::storage::SparseMatrix< T > const &transitionMatrix, std::vector< uint_fast64_t > const &nondeterministicChoiceIndices, storm::storage::SparseMatrix< T > const &backwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
template<typename T , typename RM >
std::pair< storm::storage::BitVector, storm::storage::BitVector >	storm::utility::graph::performProb01Min (storm::models::sparse::NondeterministicModel< T, RM > const &model, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates)
	Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a non-deterministic model in which all non-deterministic choices are resolved such that the probability is minimized.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProbGreater0E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes the set of states for which there exists a scheduler that achieves a probability greater than zero of satisfying phi until psi.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::computeSchedulerProbGreater0E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes a scheduler realizing a probability greater zero of satisfying phi until psi for all such states.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProb0A (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes the set of states for which there does not exist a scheduler that achieves a probability greater than zero of satisfying phi until psi.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProbGreater0A (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying phi until psi.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProb0E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
	Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying phi until psi.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProb1A (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbabilityGreater0A)
	Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::performProb1E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbabilityGreater0E)
	Computes the set of states for which there exists a scheduler that achieves probability one of satisfying phi until psi.
template<storm::dd::DdType Type, typename ValueType >
storm::dd::Bdd< Type >	storm::utility::graph::computeSchedulerProb1E (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::dd::Bdd< Type > const &statesWithProbability1E)
	Computes a scheduler satisfying phi until psi with probability 1.
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > >	storm::utility::graph::performProb01Max (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > >	storm::utility::graph::performProb01Max (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > >	storm::utility::graph::performProb01Min (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
template<storm::dd::DdType Type, typename ValueType >
std::pair< storm::dd::Bdd< Type >, storm::dd::Bdd< Type > >	storm::utility::graph::performProb01Min (storm::models::symbolic::NondeterministicModel< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates)
template<storm::dd::DdType Type, typename ValueType >
SymbolicGameProb01Result< Type >	storm::utility::graph::performProb0 (storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy=false, bool producePlayer2Strategy=false)
	Computes the set of states that have probability 0 given the strategies of the two players.
template<storm::dd::DdType Type, typename ValueType >
SymbolicGameProb01Result< Type >	storm::utility::graph::performProb1 (storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType > const &model, storm::dd::Bdd< Type > const &transitionMatrix, storm::dd::Bdd< Type > const &phiStates, storm::dd::Bdd< Type > const &psiStates, storm::OptimizationDirection const &player1Strategy, storm::OptimizationDirection const &player2Strategy, bool producePlayer1Strategy=false, bool producePlayer2Strategy=false, boost::optional< storm::dd::Bdd< Type > > const &player1Candidates=boost::none)
	Computes the set of states that have probability 1 given the strategies of the two players.
template<typename ValueType >
ExplicitGameProb01Result	storm::utility::graph::performProb0 (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair=nullptr)
	Computes the set of states that have probability 0 given the strategies of the two players.
template<typename ValueType >
ExplicitGameProb01Result	storm::utility::graph::performProb1 (storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, storm::storage::SparseMatrix< ValueType > const &player1BackwardTransitions, std::vector< uint64_t > const &player2BackwardTransitions, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::storage::ExplicitGameStrategyPair *strategyPair=nullptr, boost::optional< storm::storage::BitVector > const &player1Candidates=boost::none)
	Computes the set of states that have probability 1 given the strategies of the two players.
template<typename T >
std::vector< uint_fast64_t >	storm::utility::graph::getTopologicalSort (storm::storage::SparseMatrix< T > const &matrix, std::vector< uint64_t > const &firstStates={})
	Performs a topological sort of the states of the system according to the given transitions.
template<typename T >
std::vector< uint_fast64_t >	storm::utility::graph::getBFSSort (storm::storage::SparseMatrix< T > const &matrix, std::vector< uint_fast64_t > const &firstStates)