Checks for a given DFA if a sampleset S=(S_+,S_-) is RPNI-complete (uses https://github.com/LearnLib/automatalib)

RPNICompleteProof.java

import net.automatalib.automata.fsa.impl.compact.CompactDFA;
import net.automatalib.util.automata.Automata;
import net.automatalib.util.automata.builders.AutomatonBuilders;
import net.automatalib.visualization.Visualization;
import net.automatalib.words.Alphabet;
import net.automatalib.words.Word;
import net.automatalib.words.impl.Alphabets;
import java.util.*;

public final class RPNICompleteProof {

	private static final Alphabet<Character> ALPHABET = Alphabets.characters('a', 'b');

	public static void main(String[] args) {
		CompactDFA<Character> originalLanguage = AutomatonBuilders.newDFA(ALPHABET).
				from("q0").on('a').to("q0").
				from("q0").on('b').to("q1").
				from("q1").on('a').to("q0").
				from("q1").on('b').to("q2").
				from("q2").on('a').to("q2").
				from("q2").on('b').to("q3").
				from("q3").on('a').to("q2").
				from("q3").on('b').to("q3").
				withAccepting("q0").
				withAccepting("q2").
				withInitial("q0").create();
		//System.out.println(Arrays.toString(generateMTR(originalLanguage)));
		String[] splus = new String[]{"", "a","bb","ba","bba","bbba","bbbba","babb","abb"};
		String[] sminus = new String[]{"b","bbb","bbbb","bbabb","bbbabb","bbbbb"};
		System.out.println(isRPNIcomplete(originalLanguage,splus,sminus));
		//Visualization.visualize(originalLanguage);
	}

	public static boolean isRPNIcomplete(CompactDFA<Character> dfa, String[] splus, String[] sminus) {
		String[] mr = generateMR(dfa);
		String[] mtr = generateMTR(dfa);


		//(covering the final states)
		boolean[] marked = new boolean[dfa.getStates().size()];
		for (String u : splus) { //mark all words in splus
			if (dfa.accepts(Word.fromString(u))) {
				marked[dfa.getState(Word.fromString(u))] = true;
			}
		} //check if all final states have representative / are covered
		for (int i = 0; i< marked.length; i++) {
			if (dfa.isAccepting(i) && !marked[i]) {
				return false;
			}
		}

		//(covering the transitions)
		for (String w : mtr) {
			boolean success = false;
			for (String wv : splus) {
				if (wv.startsWith(w)) {
					success = true;
					break;
				}
			}
			if (!success) {
				return false;
			}
		}

		//(seperating the equivalence classes)
		for (String u : mr) {
			for (String v : mtr) {
				if ((int)dfa.getState(Word.fromString(u)) != (int)dfa.getState(Word.fromString(v))) {

					boolean success = false;
					LinkedList<String> uwcandidates = new LinkedList<>();
					LinkedList<String> vwcandidates = new LinkedList<>();
					LinkedList<String> allsamples = new LinkedList<>();
					allsamples.addAll(Arrays.asList(splus));
					allsamples.addAll(Arrays.asList(sminus));
					for (String uvw : allsamples) {
						if (uvw.startsWith(u)) {
							uwcandidates.push(uvw);
						}
						if (uvw.startsWith(v)) {
							vwcandidates.push(uvw);
						}
					}

					dloop: for (String uw : uwcandidates) {
						for (String vw : vwcandidates) {
							if (uw.substring(u.length(),uw.length()).equals(vw.substring(v.length(),vw.length()))) {
								if ((Arrays.asList(splus).contains(uw) && Arrays.asList(sminus).contains(vw)) || 
									(Arrays.asList(splus).contains(vw) && Arrays.asList(sminus).contains(uw))) {
									success = true;
									break dloop;
								}
							}
						}
					}

					if (!success) {
						return false;
					}
				}
			}	
		}

		return true;
	}

	public static String[] generateMR(CompactDFA<Character> dfa) { //BFS
		String[] mrset = new String[dfa.getStates().size()];
		boolean[] marked = new boolean[dfa.getStates().size()];
		
		LinkedList<String> queue = new LinkedList<>();
		marked[0] = true;
		mrset[0] = "";
		for (Character c : ALPHABET) {
			queue.push(c.toString());
		}
		while (!queue.isEmpty()) {
			String node = queue.pop();
			if (!marked[dfa.getState(Word.fromString(node))]) {
				marked[dfa.getState(Word.fromString(node))] = true;
				mrset[dfa.getState(Word.fromString(node))] = node;
				for (Character c : ALPHABET) {
					queue.push(node+c.toString());
				}	
			}
		}
		return mrset;
	}

	public static String[] generateMTR(CompactDFA<Character> dfa) {
		String[] mr = generateMR(dfa);
		LinkedList<String> mtr = new LinkedList<>();
		for (int i = 0; i < mr.length ; i++) {
			for (Character c : ALPHABET) {
				if (dfa.getState(Word.fromString(mr[i]+c.toString())) != null) { //Check for partial DFA's
					mtr.push(mr[i]+c.toString());	
				}
			}
		}
		return mtr.toArray(new String[mtr.size()]);
	}

}