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 anAutomaton
or 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 boolean
anySccMatches(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.int
index(S state)
Find the index of the strongly connected component this state belongs to.Map<S,Integer>
indexMap()
protected abstract Set<S>
initialStates()
boolean
isBottomScc(Set<S> scc)
Determine if a given strongly connected component is bottom.boolean
isTransientScc(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 thenfalse
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, 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->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 thatsccs().get(i).contains(state)
istrue
or-1
if no suchi
exists (only ifstate
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 thatsccs.contains(state)
istrue
. - Throws:
IllegalArgumentException
- ifstate
is not part of the automaton
-
condensation
@Memoized public com.google.common.graph.ImmutableGraph<Integer> condensation()
Compute the condensation graph corresponding to the SCC decomposition. TheInteger
vertices 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:
true
ifscc
is bottom,false
otherwise.
-
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.
-
-