Package owl.automaton.algorithm
Class SccDecomposition<S>
- java.lang.Object
-
- owl.automaton.algorithm.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 anAutomatonor aSuccessorFunction.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 Summary
Constructors Constructor Description SccDecomposition()
-
Method Summary
All Methods Static Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description booleananySccMatches(Predicate<? super Set<S>> predicate)Returns whether any strongly connected components match the provided predicate.Set<Integer>bottomSccs()Return indices of all strongly connected components that are bottom.com.google.common.graph.ImmutableGraph<Integer>condensation()Compute the condensation graph corresponding to the SCC decomposition.intindex(S state)Find the index of the strongly connected component this state belongs to.Map<S,Integer>indexMap()protected abstract Set<S>initialStates()booleanisBottomScc(Set<S> scc)Determine if a given strongly connected component is bottom.booleanisTransientScc(Set<S> scc)Determine if a given strongly connected component is transient.static <S> SccDecomposition<S>of(Set<S> initialStates, SuccessorFunction<S> successorFunction)static <S> SccDecomposition<S>of(Automaton<S,?> automaton)Set<S>scc(S state)Find the the strongly connected component this state belongs to.List<Set<S>>sccs()Compute the list of strongly connected components.List<Set<S>>sccsWithoutTransient()Compute the list of strongly connected components, skipping transient components.protected abstract SuccessorFunction<S>successorFunction()Set<Integer>transientSccs()Return indices of all strongly connected components that are transient.
-
-
-
Method Detail
-
successorFunction
protected abstract SuccessorFunction<S> successorFunction()
-
of
public static <S> SccDecomposition<S> of(Automaton<S,?> automaton)
-
of
public static <S> SccDecomposition<S> of(Set<S> initialStates, SuccessorFunction<S> successorFunction)
-
anySccMatches
public boolean anySccMatches(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 thenfalseis 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:
trueif any strongly connected components of the graph match the provided predicate, otherwisefalse
-
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 transitiona->bin 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
isuch thatsccs().get(i).contains(state)istrueor-1if no suchiexists (only ifstateis 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
sccsuch thatsccs.contains(state)istrue. - Throws:
IllegalArgumentException- ifstateis not part of the automaton
-
condensation
@Memoized public com.google.common.graph.ImmutableGraph<Integer> condensation()
Compute the condensation graph corresponding to the SCC decomposition. TheIntegervertices correspond to the index in the list returned bysccs(). Every path in this graph is labelled by monotonic increasing ids.- Returns:
- the condensation graph.
-
bottomSccs
@Memoized public Set<Integer> 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:
trueifsccis bottom,falseotherwise.
-
transientSccs
@Memoized public Set<Integer> 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.
-
-