From 2437601a85769bb476e5753722ca9f6215abb5af Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 26 Oct 2014 16:19:53 +0100 Subject: [PATCH] Added function to compute distances of states to some other set of states. Former-commit-id: 2bf19c1b2dcdc66b671c1d1d034c7144e4831d52 --- src/utility/graph.h | 52 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 42 insertions(+), 10 deletions(-) diff --git a/src/utility/graph.h b/src/utility/graph.h index 3af235fe3..59c180efb 100644 --- a/src/utility/graph.h +++ b/src/utility/graph.h @@ -13,14 +13,10 @@ #include "utility/OsDetection.h" -//GCC 4.7 does not support method emplace yet, therefore use boost map on Linux -#ifdef LINUX -#include -#endif - +#include "src/storage/sparse/StateType.h" #include "src/models/AbstractDeterministicModel.h" #include "src/models/AbstractNondeterministicModel.h" -#include "constants.h" +#include "src/utility/constants.h" #include "src/exceptions/InvalidArgumentException.h" #include "log4cplus/logger.h" @@ -75,6 +71,45 @@ namespace storm { return reachableStates; } + /*! + * 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 getReachableStates(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates) { + std::vector distances(transitionMatrix.getRowGroupCount()); + + std::vector> stateQueue; + stateQueue.reserve(transitionMatrix.getRowGroupCount()); + storm::storage::BitVector statesInQueue(transitionMatrix.getRowGroupCount()); + + storm::storage::sparse::state_type currentPosition = 0; + for (auto const& initialState : initialStates) { + stateQueue.emplace_back(initialState, 0); + statesInQueue.set(initialState); + } + + // Perform a BFS. + while (currentPosition < stateQueue.size()) { + std::pair const& stateDistancePair = stateQueue[currentPosition]; + distances[stateDistancePair.first] = stateDistancePair.second; + + for (auto const& successorEntry : transitionMatrix.getRowGroup(stateDistancePair.first)) { + if (!statesInQueue.get(successorEntry.getColumn())) { + stateQueue.emplace_back(successorEntry.getColumn(), stateDistancePair.second + 1); + statesInQueue.set(successorEntry.getColumn()); + } + } + ++currentPosition; + } + + return distances; + } + /*! * 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 @@ -727,11 +762,8 @@ namespace storm { std::vector predecessors(model.getNumberOfStates(), noPredecessorValue); // Set the probability to 1 for all starting states. -#ifdef LINUX - boost::container::set, DistanceCompare> probabilityStateSet; -#else std::set, DistanceCompare> probabilityStateSet; -#endif + for (auto state : startingStates) { probabilityStateSet.emplace(storm::utility::constantOne(), state); probabilities[state] = storm::utility::constantOne();