diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index d17d95edc..fa23afe7f 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -116,6 +116,43 @@ namespace storm { return result; } + template + bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, boost::optional const& subsystem) { + storm::storage::BitVector unexploredStates; // States that have not been visited yet + storm::storage::BitVector acyclicStates; // States that are known to not lie on a cycle consisting of subsystem states + if (subsystem) { + unexploredStates = subsystem.get(); + acyclicStates = ~subsystem.get(); + } else { + unexploredStates.resize(transitionMatrix.getRowGroupCount(), true); + acyclicStates.resize(transitionMatrix.getRowGroupCount(), false); + } + std::vector dfsStack; + for (uint64_t start = unexploredStates.getNextSetIndex(0); start < unexploredStates.size(); start = unexploredStates.getNextSetIndex(start + 1)) { + dfsStack.push_back(start); + while (!dfsStack.empty()) { + uint64_t state = dfsStack.back(); + if (unexploredStates.get(state)) { + unexploredStates.set(state, false); + for (auto const& entry : transitionMatrix.getRowGroup(start)) { + if (unexploredStates.get(entry.getColumn())) { + dfsStack.push_back(entry.getColumn()); + } else { + if (!acyclicStates.get(entry.getColumn())) { + // The state has been visited before but is not known to be acyclic. + return true; + } + } + } + } else { + acyclicStates.set(state, true); + dfsStack.pop_back(); + } + } + } + return false; + } + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices) { @@ -1650,6 +1687,8 @@ namespace storm { template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + template bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, boost::optional const& subsystem); + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1727,8 +1766,10 @@ namespace storm { 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, bool useStepBound, uint_fast64_t maximalSteps, boost::optional const& choiceFilter); template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); - - template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); + + template bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, boost::optional const& subsystem); + + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); @@ -1785,6 +1826,8 @@ namespace storm { template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + template bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, boost::optional const& subsystem); + template bool checkIfECWithChoiceExists(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& choices); template std::vector getDistances(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional const& subsystem); diff --git a/src/storm/utility/graph.h b/src/storm/utility/graph.h index 152cf10b9..6f65bbcfa 100644 --- a/src/storm/utility/graph.h +++ b/src/storm/utility/graph.h @@ -81,6 +81,15 @@ namespace storm { template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix const& transitionMatrix); + + /*! + * Returns true if the graph represented by the given matrix has a cycle + * @param transitionMatrix + * @param subsystem if given, only states in the subsystem are considered for the check. + */ + template + bool hasCycle(storm::storage::SparseMatrix const& transitionMatrix, boost::optional const& subsystem = boost::none); + /*! * Checks whether there is an End Component that * 1. contains at least one of the specified choices and