In January 2021 we will introduce a 10 GB quota for project repositories. Higher limits for individual projects will be available on request. Please see for more information.

Commit 06c86e06 authored by Salomon Sickert-Zehnter's avatar Salomon Sickert-Zehnter

Merge branch 'quotient-automaton' into 'master'

Add QuotientAutomaton.

See merge request i7/owl!357
parents b7490ae7 f0b7a67d
...@@ -23,10 +23,12 @@ import static; ...@@ -23,10 +23,12 @@ import static;
import static owl.automaton.Automaton.PreferredEdgeAccess.EDGE_TREE; import static owl.automaton.Automaton.PreferredEdgeAccess.EDGE_TREE;
import; import;
import; import;
import; import;
import java.util.BitSet; import java.util.BitSet;
import java.util.HashMap; import java.util.HashMap;
import java.util.HashSet;
import java.util.List; import java.util.List;
import java.util.Map; import java.util.Map;
import java.util.NoSuchElementException; import java.util.NoSuchElementException;
...@@ -44,6 +46,7 @@ import owl.automaton.edge.Edge; ...@@ -44,6 +46,7 @@ import owl.automaton.edge.Edge;
import owl.automaton.edge.Edges; import owl.automaton.edge.Edges;
import owl.collections.ValuationSet; import owl.collections.ValuationSet;
import owl.collections.ValuationTree; import owl.collections.ValuationTree;
import owl.collections.ValuationTrees;
import owl.factories.ValuationSetFactory; import owl.factories.ValuationSetFactory;
import; import;
import; import;
...@@ -413,4 +416,79 @@ public final class Views { ...@@ -413,4 +416,79 @@ public final class Views {
return mapper == null ? edges :; return mapper == null ? edges :;
} }
} }
* This is essentially {@code fmap :: (S -> T) -> Automaton<S,A> -> Automaton<T,A>}.
* When the function is injective, the effect is just replacing states of type S with states of
* type T. If it is not, the result will be a quotient wrt. the equivalence classes induced by
* the preimages.
* @param <S> input state type
* @param <T> output state type
* @param <A> acceptance condition
* @param automaton input automaton
* @param mappingFunction function from S to T
* @return Output automaton where states are mapped from S to T (and possibly quotiented)
public static <S, T, A extends OmegaAcceptance> Automaton<T,A>
quotientAutomaton(Automaton<S,A> automaton, Function<S,T> mappingFunction) {
Map<S, T> mapping = new HashMap<>();
ImmutableListMultimap.Builder<T, S> reverseMappingBuilder = ImmutableListMultimap.builder();
for (var state : automaton.states()) {
var mappedState = mappingFunction.apply(state);
mapping.put(state, mappedState);
reverseMappingBuilder.put(mappedState, state);
return new QuotientAutomaton<>(automaton, Map.copyOf(mapping),;
private static class QuotientAutomaton<S, T, A extends OmegaAcceptance>
extends AbstractImmutableAutomaton.NonDeterministicEdgeTreeAutomaton<T, A> {
private final Automaton<S, A> automaton;
private final Map<S, T> mapping;
private final ImmutableListMultimap<T, S> reverseMapping;
private QuotientAutomaton(Automaton<S, A> automaton, Map<S, T> mapping,
ImmutableListMultimap<T, S> reverseMapping) {
this.automaton = automaton;
this.mapping = Map.copyOf(mapping);
this.reverseMapping = reverseMapping;
public Set<Edge<T>> edges(T state, BitSet valuation) {
return reverseMapping.get(state).stream()
.flatMap((S sState) -> automaton.edges(sState, valuation).stream())
.map((Edge<S> sEdge) -> sEdge.withSuccessor(mapping.get(sEdge.successor())))
public ValuationTree<Edge<T>> edgeTree(T state) {
return ValuationTrees.cartesianProduct(
).map(x -> {
Set<Edge<T>> set = new HashSet<>();
for (List<Edge<S>> edges : x) {
for (Edge<S> edge : edges) {
return set;
public List<PreferredEdgeAccess> preferredEdgeAccess() {
return automaton.preferredEdgeAccess();
} }
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment