package de.renew.fa.service;

import java.util.Iterator;

import net.automatalib.automata.fsa.impl.FastNFA;
import net.automatalib.automata.fsa.impl.compact.CompactDFA;
import net.automatalib.util.automata.Automata;
import net.automatalib.util.automata.fsa.NFAs;
import net.automatalib.words.Word;
import net.automatalib.words.impl.GrowingMapAlphabet;

import de.renew.fa.FADrawing;
import de.renew.fa.model.FA;
import de.renew.fa.model.Letter;
import de.renew.fa.util.FAHelper;

/**
 * This static class can be used to compare two automatas, each represented by a {@link de.renew.fa.FADrawing}.
 * For this, the <a href="href=https://github.com/LearnLib/automatalib">AutomataLib</a> is used.
 *
 * @see <a href="https://github.com/LearnLib/automatalib"></a>
 */
public class AutomataComparator {

    private AutomataComparator() {}

    /**
     * This method takes two FADrawings, interprets them as NFAs, and returns a word that separates them
     * (i.e. only one of the automaton accepts the word).
     * @param nfa1 The automaton to compare
     * @param nfa2 The other automaton
     * @return <code>null</code> if the automatons language is equals, or two Strings.
     * The first String is the name of the automata that accepts the word,
     * the second entry is the word that is not accepted by the other automata.
     */
    public static String[] nfaLanguageEquivalence(FADrawing nfa1, FADrawing nfa2) {
        FA fa1 = FAHelper.getModel(nfa1);
        Iterator<Letter> fa1Letters = fa1.getAlphabet();
        FA fa2 = FAHelper.getModel(nfa2);
        Iterator<Letter> fa2Letters = fa2.getAlphabet();
        //we have to create the FastNFAs with the set of ALL alphabet symbols, otherwise Exceptions occur.
        //we also can't add the symbols later on.
        GrowingMapAlphabet<String> alphabet = new GrowingMapAlphabet<>();
        while (fa1Letters.hasNext()) {
            alphabet.add(fa1Letters.next().getName());
        }
        while (fa2Letters.hasNext()) {
            alphabet.add(fa2Letters.next().getName());
        }
        FastNFA<String> fastNfa1 = FAHelper.convertFAModelToAutomaton(fa1, alphabet);
        FastNFA<String> fastNfa2 = FAHelper.convertFAModelToAutomaton(fa2, alphabet);
        CompactDFA<String> dfa1 = NFAs.determinize(fastNfa1);
        CompactDFA<String> dfa2 = NFAs.determinize(fastNfa2);
        Word<String> words = Automata.findSeparatingWord(dfa1, dfa2, alphabet);
        if (words != null) {
            StringBuilder word = new StringBuilder();
            for (String s : words) {
                word.append(s);
            }
            String[] result = new String[2];
            result[1] = word.toString();
            if (dfa1.accepts(words)) {
                if (fa1.getName() == null || fa1.getName().equals("")) {
                    fa1.setName("Template");
                }
                result[0] = fa1.getName();
            } else {
                result[0] = fa2.getName();
            }
            return result;
        } else {
            return null;
        }
    }
}
