Package owl.automaton.algorithm

Class SccDecomposition<S>

  • public abstract class SccDecomposition<S>
extends Object
    This class provides a decomposition into strongly connected components (SCCs) of a directed graph given by either an Automaton or a SuccessorFunction.

    The SCC decomposition is computed using 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.

    • Constructor Detail

      • SccDecomposition

        public SccDecomposition()

    • Method Detail

      • initialStates

        protected abstract Set<S> initialStates()

      • automaton

        @Nullable
protected abstract Automaton<S,​?> automaton()

      • anyMatch

        public boolean anyMatch​(Predicate<? super Set<S>> predicate)
        Returns whether any strongly connected components match the provided predicate. May not evaluate the predicate on all strongly connected components if not necessary for determining the result. If the initial states are empty then false is returned and the predicate is not evaluated.

        This method evaluates the existential quantification of the predicate over the strongly connected components (for some x P(x)).

        Parameters:
        predicate - a non-interfering, stateless predicate to apply to strongly connected components of the graph
        Returns:
        true if any strongly connected components of the graph match the provided predicate, otherwise false

      • allMatch

        public boolean allMatch​(Predicate<? super Set<S>> predicate)
        Returns whether all strongly connected components match the provided predicate. May not evaluate the predicate on all strongly connected components if not necessary for determining the result. If the initial states are empty then true is returned and the predicate is not evaluated.

        This method evaluates the universal quantification of the predicate over the strongly connected components (for all x P(x)).

        Parameters:
        predicate - a non-interfering, stateless predicate to apply to strongly connected components of the graph
        Returns:
        true if all strongly connected components of the graph match the provided predicate, otherwise false

      • sccs

        @Memoized
public List<Set<S>> sccs()
        Compute the list of strongly connected components. The returned list of SCCs is ordered according to the topological ordering in the condensation graph, i.e., a 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.
        Returns:
        the list of strongly connected components.

      • sccsWithoutTransient

        @Memoized
public List<Set<S>> sccsWithoutTransient()
        Compute the list of strongly connected components, skipping transient components.
        Returns:
        the list of strongly connected components without transient.

      • index

        public int index​(S state)
        Find the index of the strongly connected component this state belongs to.
        Parameters:
        state - the state.
        Returns:
        the index i such that sccs().get(i).contains(state) is true or -1 if no such i exists (only if state is not part of the automaton)

      • scc

        public Set<S> scc​(S state)
        Find the the strongly connected component this state belongs to.
        Parameters:
        state - the state.
        Returns:
        scc scc such that sccs.contains(state) is true.
        Throws:
        IllegalArgumentException - if state is not part of the automaton

      • indexMap

        @Memoized
public Map<S,​Integer> indexMap()

      • condensation

        @Memoized
public com.google.common.graph.ImmutableGraph<Integer> condensation()
        Compute the condensation graph corresponding to the SCC decomposition. The Integer vertices correspond to the index in the list returned by sccs(). Every path in this graph is labelled by monotonic increasing ids.
        Returns:
        the condensation graph.

      • bottomSccs

        @Memoized
public ImmutableBitSet bottomSccs()
        Return indices of all strongly connected components that are bottom. A SCC is considered bottom if it is not transient and there are no transitions leaving it.
        Returns:
        indices of bottom strongly connected components.

      • isBottomScc

        public boolean isBottomScc​(Set<S> scc)
        Determine if a given strongly connected component is bottom. A SCC is considered bottom if there are no transitions leaving it.
        Parameters:
        scc - a strongly connected component.
        Returns:
        true if scc is bottom, false otherwise.

      • transientSccs

        @Memoized
public ImmutableBitSet transientSccs()
        Return indices of all strongly connected components that are transient. An SCC is considered transient if there are no transitions within in it.
        Returns:
        indices of transient strongly connected components.

      • isTransientScc

        public boolean isTransientScc​(Set<? extends S> scc)
        Determine if a given strongly connected component is transient. An SCC is considered transient if there are no transitions within in it.
        Parameters:
        scc - a strongly connected component.
        Returns:
        true if scc is transient, false otherwise.

      • pathExists

        public boolean pathExists​(S source,
                          S target)
        reachability relation on states.

      • deterministicSccs

        @Memoized
public ImmutableBitSet deterministicSccs()
        deterministic SCCs.

      • acceptingSccs

        @Memoized
public ImmutableBitSet acceptingSccs()
        Weak accepting SCCs (non-trivial and only good cycles). Only BüchiAcceptance supported.

      • rejectingSccs

        @Memoized
public ImmutableBitSet rejectingSccs()
        Weak rejecting SCCs (trivial or only rejecting cycles).