Class SccDecomposition<S>


  • public final class SccDecomposition<S>
    extends Object
    Finds the SCCs of a given graph / transition system using Tarjan's algorithm.
    • Method Detail

      • computeSccs

        public static <S> List<Set<S>> computeSccs​(Automaton<S,​?> automaton)
        This method computes the SCCs of the state-/transition-graph of the automaton. It is based on Tarjan's strongly connected component algorithm. It runs in linear time, assuming the Map-operation get, put and containsKey (and the onStack set-operations) take constant time.

        The returned list of SCCs is ordered according to the topological ordering in the "condensation graph", aka the graph where the SCCs are vertices, ordered such that for each transition a->b in the condensation graph, a is in the list before b

        Parameters:
        automaton - Automaton, for which the class is analysed
        Returns:
        A list of set of states, where each set corresponds to an SCC, in topological order
      • computeSccs

        public static <S> List<Set<S>> computeSccs​(Automaton<S,​?> automaton,
                                                   boolean includeTransient)
      • computeSccs

        public static <S> List<Set<S>> computeSccs​(SuccessorFunction<S> function,
                                                   S initialState,
                                                   boolean includeTransient)
      • computeSccs

        public static <S> List<Set<S>> computeSccs​(SuccessorFunction<S> function,
                                                   Set<S> initialStates,
                                                   boolean includeTransient)
      • isTransient

        public static <S> boolean isTransient​(SuccessorFunction<S> successorFunction,
                                              Set<S> scc)
      • isTrap

        public static <S> boolean isTrap​(Automaton<S,​?> automaton,
                                         Set<S> trap)
        Determines whether the given set of states is a BSCC in the given automaton.