#ifndef STORM_UTILITY_GRAPH_H_ #define STORM_UTILITY_GRAPH_H_ #include #include #include "utility/OsDetection.h" #include "src/storage/sparse/StateType.h" #include "src/models/sparse/NondeterministicModel.h" #include "src/models/sparse/DeterministicModel.h" #include "src/storage/dd/DdType.h" #include "src/solver/OptimizationDirection.h" namespace storm { namespace storage { class BitVector; template class SparseMatrix; } namespace models { namespace symbolic { template class Model; template class DeterministicModel; template class NondeterministicModel; template class StochasticTwoPlayerGame; } } namespace dd { template class Bdd; template class Add; } namespace utility { namespace graph { /*! * 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. * * @param transitionMatrix The transition relation of the graph structure to search. * @param initialStates The set of states from which to start the search. * @param constraintStates The set of states that must not be left. * @param targetStates The target states that may not be passed. */ template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates); /*! * Performs a breadth-first search through the underlying graph structure to compute the distance from all * states to the starting states of the search. * * @param transitionMatrix The transition relation of the graph structure to search. * @param initialStates The set of states from which to start the search. * @return The distances of each state to the initial states of the sarch. */ template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates); /*! * 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. The resulting states are written to the given bit vector. * * @param backwardTransitions The reversed transition relation of the graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. * @param maximalSteps The maximal number of steps to reach the psi states. * @return A bit vector with all indices of states that have a probability greater than 0. */ template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0); /*! * 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. In order to do this, it uses the given set of states that * characterizes the states that possess at least one path to a target state. * The results are written to the given bit vector. * * @param backwardTransitions The reversed transition relation of the graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. * @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive * probability mass of satisfying phi until psi. * @return A bit vector with all indices of states that have a probability greater than 1. */ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix 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. In order to do this, it uses the given set of states that * characterizes the states that possess at least one path to a target state. * The results are written to the given bit vector. * * @param backwardTransitions The reversed transition relation of the graph structure to search. * @param phiStates A bit vector of all states satisfying phi. * @param psiStates A bit vector of all states satisfying psi. * @return A bit vector with all indices of states that have a probability greater than 1. */ template storm::storage::BitVector performProb1(storm::storage::SparseMatrix 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. * * @param model The model whose graph structure to search. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A pair of bit vectors such that the first bit vector stores the indices of all states * with probability 0 and the second stores all indices of states with probability 1. */ template std::pair performProb01(storm::models::sparse::DeterministicModel 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. * * @param backwardTransitions The backward transitions of the model whose graph structure to search. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A pair of bit vectors such that the first bit vector stores the indices of all states * with probability 0 and the second stores all indices of states with probability 1. */ template std::pair performProb01(storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); /*! * Computes the set of states that has a positive probability of reaching psi states after only passing * through phi states before. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @param stepBound If given, this number indicates the maximal amount of steps allowed. * @return All states with positive probability. */ template storm::dd::Bdd performProbGreater0(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, boost::optional const& stepBound = boost::optional()); /*! * Computes the set of states that have a probability of one of reaching psi states after only passing * through phi states before. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @param statesWithProbabilityGreater0 The set of states with a positive probability of satisfying phi * until psi as a BDD. * @return All states with probability 1. */ template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0); /*! * Computes the set of states that have a probability of one of reaching psi states after only passing * through phi states before. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @return All states with probability 1. */ template storm::dd::Bdd performProb1(storm::models::symbolic::Model const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; /*! * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a * deterministic model. * * @param model The (symbolic) model for which to compute the set of states. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @return A pair of BDDs that represent all states with probability 0 and 1, respectively. */ template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::DeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a * deterministic model. * * @param model The (symbolic) model for which to compute the set of states. This is used for retrieving the * manager and information about the meta variables. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @return A pair of BDDs that represent all states with probability 0 and 1, respectively. */ template std::pair, storm::dd::Bdd> performProb01(storm::models::symbolic::Model const& model, storm::dd::Add const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * 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. Stated differently, * this means that these states have a probability greater 0 of satisfying phi until psi if the * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. * @param maximalSteps The maximal number of steps to reach the psi states. * @return A bit vector that represents all states with probability 0. */ template storm::storage::BitVector performProbGreater0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0) ; template storm::storage::BitVector performProb0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 all * possible resolutions of non-determinism in a non-deterministic model. Stated differently, * this means that these states have probability 0 of satisfying phi until psi even if the * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. * @param maximalSteps The maximal number of steps to reach the psi states. * @return A bit vector that represents all states with probability 0. */ template storm::storage::BitVector performProb0A(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix 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. Stated differently, * this means that these states have probability 1 of satisfying phi until psi if the * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 1. */ template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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. Stated differently, * this means that these states have probability 1 of satisfying phi until psi if the * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 1. */ template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Max(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 non-deterministic model in which all non-deterministic choices are resolved * such that the probability is maximized. * * @param model The model whose graph structure to search. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. */ template std::pair performProb01Max(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ; /*! * 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. Stated differently, * this means that these states have a probability greater 0 of satisfying phi until psi if the * scheduler tries to maximize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @param useStepBound A flag that indicates whether or not to use the given number of maximal steps for the search. * @param maximalSteps The maximal number of steps to reach the psi states. * @return A bit vector that represents all states with probability 0. */ template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 0 of satisfying phi until psi under at least * one possible resolution of non-determinism in a non-deterministic model. Stated differently, * this means that these states have probability 0 of satisfying phi until psi if the * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel const& model, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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. Stated differently, * this means that these states have probability 1 of satisfying phi until psi even if the * scheduler tries to minimize this probability. * * @param model The model whose graph structure to search. * @param backwardTransitions The reversed transition relation of the model. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A bit vector that represents all states with probability 0. */ template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); template std::pair performProb01Min(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& nondeterministicChoiceIndices, storm::storage::SparseMatrix 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 non-deterministic model in which all non-deterministic choices are resolved * such that the probability is minimized. * * @param model The model whose graph structure to search. * @param phiStates The set of all states satisfying phi. * @param psiStates The set of all states satisfying psi. * @return A pair of bit vectors that represent all states with probability 0 and 1, respectively. */ template std::pair performProb01Min(storm::models::sparse::NondeterministicModel const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector 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. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @return A BDD representing all such states. */ template storm::dd::Bdd performProbGreater0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd 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. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The phi states of the model. * @param psiStates The psi states of the model. * @return A BDD representing all such states. */ template storm::dd::Bdd performProb0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; /*! * Computes the set of states for which all schedulers achieve a probability greater than zero of satisfying * phi until psi. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @return A BDD representing all such states. */ template storm::dd::Bdd performProbGreater0A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates) ; /*! * Computes the set of states for which there exists a scheduler that achieves probability zero of satisfying * phi until psi. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @return A BDD representing all such states. */ template storm::dd::Bdd performProb0E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); /*! * Computes the set of states for which all schedulers achieve probability one of satisfying phi until psi. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @param statesWithProbabilityGreater0A The states of the model that have a probability greater zero under * all schedulers. * @return A BDD representing all such states. */ template storm::dd::Bdd performProb1A(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0A); /*! * Computes the set of states for which there exists a scheduler that achieves probability one of satisfying * phi until psi. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. * @param statesWithProbabilityGreater0E The states of the model that have a scheduler that achieves a value * greater than zero. * @return A BDD representing all such states. */ template storm::dd::Bdd performProb1E(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::dd::Bdd const& statesWithProbabilityGreater0E) ; template std::pair, storm::dd::Bdd> performProb01Max(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template std::pair, storm::dd::Bdd> performProb01Min(storm::models::symbolic::NondeterministicModel const& model, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates); template struct GameProb01Result { GameProb01Result(storm::dd::Bdd const& states, boost::optional> const& player1Strategy = boost::none, boost::optional> const& player2Strategy = boost::none) : states(states), player1Strategy(player1Strategy), player2Strategy(player2Strategy) { // Intentionally left empty. } storm::dd::Bdd states; boost::optional> player1Strategy; boost::optional> player2Strategy; }; /*! * Computes the set of states that have probability 0 given the strategies of the two players. * * @param model The (symbolic) model for which to compute the set of states. * @param transitionMatrix The transition matrix of the model as a BDD. * @param phiStates The BDD containing all phi states of the model. * @param psiStates The BDD containing all psi states of the model. */ template GameProb01Result performProb0(storm::models::symbolic::StochasticTwoPlayerGame const& model, storm::dd::Bdd const& transitionMatrix, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, storm::OptimizationDirection const& player1Strategy, storm::OptimizationDirection const& player2Strategy); /*! * Performs a topological sort of the states of the system according to the given transitions. * * @param matrix A square matrix representing the transition relation of the system. * @return A vector of indices that is a topological sort of the states. */ template std::vector getTopologicalSort(storm::storage::SparseMatrix const& matrix); /*! * A class needed to compare the distances for two states in the Dijkstra search. */ template struct DistanceCompare { bool operator()(std::pair const& lhs, std::pair const& rhs) const { return lhs.first > rhs.first || (lhs.first == rhs.first && lhs.second > rhs.second); } }; /*! * Performs a Dijkstra search from the given starting states to determine the most probable paths to all other states * by only passing through the given state set. * * @param model The model whose state space is to be searched. * @param transitions The transitions wrt to which to compute the most probable paths. * @param startingStates The starting states of the Dijkstra search. * @param filterStates A set of states that must not be left on any path. */ template std::pair, std::vector> performDijkstra(storm::models::sparse::Model const& model, storm::storage::SparseMatrix const& transitions, storm::storage::BitVector const& startingStates, storm::storage::BitVector const* filterStates = nullptr); } // namespace graph } // namespace utility } // namespace storm #endif /* STORM_UTILITY_GRAPH_H_ */