Select Git revision
AutomataEq.java
Code owners
Assign users and groups as approvers for specific file changes. Learn more.
AutomataEq.java 2.32 KiB
import net.automatalib.automata.fsa.FiniteStateAcceptor;
import net.automatalib.automata.fsa.impl.compact.CompactNFA;
import net.automatalib.words.Word;
import java.util.*;
/**
* equivalence of automata, currenctly very simple, to be extended to Hopcroft and Karp
* https://hal.archives-ouvertes.fr/file/index/docid/648587/filename/hkc.pdf
*/
public class AutomataEq {
public static <I> Word<I> eqCounterex(CompactNFA<I> a, FiniteStateAcceptor<?, I> b) {
Set<PairwW<Set, I>> R = new HashSet<>();
Set<PairwW<Set, I>> todo = new HashSet<>();
todo.add(new PairwW<>(a.getInitialStates(), b.getInitialStates(), Word.epsilon()));
while (!todo.isEmpty()) {
PairwW<Set, I> currentPair = todo.iterator().next();
todo.remove(currentPair);
if (R.contains(currentPair)) //FIXME transitivity
continue;
if (a.isAccepting(currentPair.a) != b.isAccepting(currentPair.b)) {
System.out.println(currentPair.w);
return currentPair.w;
}
for (I i:a.getInputAlphabet()) {
todo.add(new PairwW<Set, I>(a.getSuccessors(currentPair.a, Collections.singletonList(i)),
b.getSuccessors(currentPair.b, Collections.singletonList(i)),
currentPair.w.append(i)));
}
R.add(currentPair);
}
return null;
}
public static <I> boolean eq(CompactNFA<I> a, FiniteStateAcceptor<?, I> b) {
return eqCounterex(a, b) == null;
}
public static class PairwW<S, I> {
public final S a;
public final S b;
public final Word<I> w;
public PairwW(S a, S b, Word<I> w) {
this.a = a;
this.b = b;
this.w = w;
}
/**
* don't care about the word w for equality
*/
@Override
public boolean equals(Object o) {
if (this == o) return true;
if (o == null || getClass() != o.getClass()) return false;
PairwW<?, ?> pair = (PairwW<?, ?>) o;
return Objects.equals(a, pair.a) &&
Objects.equals(b, pair.b);
}
@Override
public int hashCode() {
return Objects.hash(a, b);