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 Mapoperation get, put and containsKey (and the onStack setoperations) 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 ImmutableBitSet
acceptingSccs()
Weak accepting SCCs (nontrivial and only good cycles).boolean
allMatch(Predicate<? super Set<S>> predicate)
Returns whether all strongly connected components match the provided predicate.boolean
anyMatch(Predicate<? super Set<S>> predicate)
Returns whether any strongly connected components match the provided predicate.protected abstract Automaton<S,?>
automaton()
ImmutableBitSet
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.ImmutableBitSet
deterministicSccs()
deterministic SCCs.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<? 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)
boolean
pathExists(S source, S target)
reachability relation on states.ImmutableBitSet
rejectingSccs()
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()
String
toString()
ImmutableBitSet
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<? 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 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 noninterfering, 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

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 thentrue
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 noninterfering, 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, 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
or1
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 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
ifscc
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
ifscc
is transient,false
otherwise.

deterministicSccs
@Memoized public ImmutableBitSet deterministicSccs()
deterministic SCCs.

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

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

