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 ImmutableBitSetacceptingSccs()Weak accepting SCCs (non-trivial and only good cycles).booleanallMatch(Predicate<? super Set<S>> predicate)Returns whether all strongly connected components match the provided predicate.booleananyMatch(Predicate<? super Set<S>> predicate)Returns whether any strongly connected components match the provided predicate.protected abstract Automaton<S,?>automaton()ImmutableBitSetbottomSccs()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.ImmutableBitSetdeterministicSccs()deterministic SCCs.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<? extends S> scc)Determine if a given strongly connected component is transient.static <S> SccDecomposition<S>of(Set<? extends S> initialStates, SuccessorFunction<S> successorFunction)static <S> SccDecomposition<S>of(Automaton<S,?> automaton)booleanpathExists(S source, S target)reachability relation on states.ImmutableBitSetrejectingSccs()Weak rejecting SCCs (trivial or only rejecting cycles).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()StringtoString()ImmutableBitSettransientSccs()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<? extends S> initialStates, SuccessorFunction<S> successorFunction)
-
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 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
-
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 thentrueis 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:
trueif all 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 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:
trueifsccis bottom,falseotherwise.
-
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:
trueifsccis transient,falseotherwise.
-
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).
-
-