package de.renew.faformalism.util;

import java.util.AbstractMap;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import javax.swing.JFrame;
import javax.swing.JLabel;
import javax.swing.JOptionPane;

import de.renew.unify.Tuple;

/**
 * This static class is used for the simulation of automaton.
 * The FASingleNetCompiler translates the FAFigures into a Petri net, and adds inscriptions to the arcs and transitions.
 * These transitions will call the methods canFire() and fire().
 */
public class FAAutomatonSimulationHelper {

    private static final char EPSILON = 'ε';
    // [(current word, current stack), (current rule) -> [new word, new stack]]
    private static final String DISPLAY_FORMAT = "[(%s, %s), (%s) ] → [%s, %s]";
    private static final String PDA_RULE_FORMAT = "%c, %c->%c";

    private FAAutomatonSimulationHelper() {}

    /**
     * Checks if the transition can fire according to the rules of the automaton model.
     *
     * @param currentTuple the tuple currently being simulated in this step consisting of the word of type {@code String} and,
     * if the automaton is a PDA, an {@link AutomatonDataStructure}, otherwise {@code null}
     * @param arcInscription the inscription of the arc
     * @return {@code true} if the transition can fire, {@code false} otherwise.
     */
    public static boolean canFire(Tuple currentTuple, String arcInscription) {
        String currentWord = (String) currentTuple.getComponent(0);
        switch (SimulationSettingsManager.getAutomatonModel()) {
            case NFA, DFA -> {
                return canFireNFA(currentWord, arcInscription);
            }
            case BUECHI -> {
                return canFireBUECHI(currentWord, arcInscription);
            }
            case PDA -> {
                return canFirePDA(currentTuple, arcInscription);
            }
        }
        return false;
    }

    private static boolean canFireNFA(String currentWord, String arcInscription) {
        if (!SimulationSettingsManager.getSimulateWordMode()) {
            return true;
        }
        List<String> allowedByArc = splitNFAArcInscription(arcInscription);
        if (allowedByArc.contains("")) {
            return true;
        }
        List<String> preparedWords = prepareTokenForConsumption(currentWord);
        for (String word : preparedWords) {
            for (String arcInscr : allowedByArc) {
                if (!word.isEmpty() && word.charAt(0) == arcInscr.charAt(0)) {
                    return true;
                }
            }
        }
        return false;
    }

    private static boolean canFireBUECHI(String currentWord, String arcInscription) {
        //this method is also called by FASyntaxChecker, which wants to know if all possible words end on '°'.
        //therefore, we first check the prepared words and then take the arcInscription into account0
        if (SimulationSettingsManager.getSimulateWordMode()) {
            List<String> preparedWords = prepareTokenForConsumption(currentWord);
            for (String word : preparedWords) {
                if (!word.endsWith("°")) {
                    return false;
                }
            }
            return canFireNFA(currentWord, arcInscription);
        } else {
            return true;
        }
    }

    private static boolean canFirePDA(Tuple currentTuple, String arcInscription) {
        String currentWord = (String) currentTuple.getComponent(0);
        StackDataStructure currentStack = (StackDataStructure) currentTuple.getComponent(1);
        String[] allRules = arcInscription.split("\n");
        List<String> preparedWords = prepareTokenForConsumption(currentWord);
        for (String preparedWord : preparedWords) {
            for (String rule : allRules) {
                if (preparedWord.isEmpty()) {
                    continue;
                }
                PDARule letters = generatePDARuleFromArcInscription(rule);
                if (SimulationSettingsManager.getSimulateWordMode()) {
                    if (isValidWordForPDASimulateWord(letters, currentStack, preparedWord)) {
                        return true;
                    }
                } else {
                    if (isValidWordForPDABuildWord(letters, currentStack)) {
                        return true;
                    }
                }
            }
        }

        return false;
    }

    private static boolean isValidWordForPDASimulateWord(
        PDARule rule, StackDataStructure currentStack, String preparedWord)
    {
        if (rule.letter == EPSILON && (rule.requiredStackSymbol == EPSILON
            || currentStack.peek() == rule.requiredStackSymbol)) {
            return true;
        }
        if (rule.letter != EPSILON && rule.letter == preparedWord.charAt(0)) {
            if (rule.requiredStackSymbol == EPSILON) {
                return true;
            }
            return currentStack.peek() == rule.requiredStackSymbol;
        }
        return false;
    }

    private static boolean isValidWordForPDABuildWord(PDARule letters, StackDataStructure stack) {
        return letters.requiredStackSymbol == EPSILON
            || stack.peek() == letters.requiredStackSymbol;
    }

    /**
     * Takes in the current word and alters it according to the automaton model as determined by {@link SimulationSettingsManager#getAutomatonModel()}.
     *
     * @param currentTuple the tuple currently being simulated in this step consisting of the word as a String and,
     * if the automaton is a PDA, an {@link AutomatonDataStructure}, otherwise {@code null}
     * @param arcInscription the inscription of the arc
     * @return the word after transitioning to the new FAState.
     */
    public static Tuple fire(Tuple currentTuple, String arcInscription) {
        String currentWord = (String) currentTuple.getComponent(0);
        currentWord = currentWord.replace(" ", "");
        arcInscription = arcInscription.replace(" ", "");
        FAAutomatonModelEnum model = SimulationSettingsManager.getAutomatonModel();
        switch (model) {
            case DFA, NFA, BUECHI -> {
                currentWord = fireNFA(currentWord, arcInscription);
            }
            case PDA -> {
                return firePDA(currentTuple, arcInscription);
            }
        }
        return new Tuple(new Object[] { currentWord, currentTuple.getComponent(1) }, null);
    }

    private static Tuple firePDA(Tuple currentTuple, String arcInscription) {
        String currentWord = (String) currentTuple.getComponent(0);
        StackDataStructure currentStack = (StackDataStructure) currentTuple.getComponent(1);
        String[] allRules = arcInscription.split("\n");
        List<String> preparedWords = prepareTokenForConsumption(currentWord);
        HashMap<String, PDAOperationResult> nextWords = new HashMap<>();

        if (SimulationSettingsManager.getSimulateWordMode()) {
            for (String preparedWord : preparedWords) {
                for (String rule : allRules) {
                    Optional<Map.Entry<String, PDAOperationResult>> validWordForRule =
                        retrieveNextValidWordForRule(rule, currentWord, preparedWord, currentStack);
                    validWordForRule.ifPresent(
                        stringPDAOperationResultEntry -> nextWords.put(
                            stringPDAOperationResultEntry.getKey(),
                            stringPDAOperationResultEntry.getValue()));
                }
            }
        } else {
            for (String rule : allRules) {
                Optional<Map.Entry<String, PDAOperationResult>> nextPossibleWord =
                    buildNextPossibleWordForRule(rule, currentWord, currentStack);
                nextPossibleWord.ifPresent(
                    nextPossibleWordEntry -> nextWords
                        .put(nextPossibleWordEntry.getKey(), nextPossibleWordEntry.getValue()));
            }
        }
        return selectAndFirePDAArc(nextWords);
    }

    /**
     * Builds the next possible word and stack configuration for the given rule. The corresponding arc is traversable, if the stack rule is valid. If no word can be generated,
     * an empty optional is returned.
     *
     * @param currentInscription the current inscription specifying how the stack is to be updated and the new word is to be formed
     * @param currentWord the current word already built
     * @param currentStack the stack corresponding to the current word
     * @return an optional entry containing the display for the new word together with a {@link PDAOperationResult} containing the resulting word and stack
     */
    private static Optional<Map.Entry<String, PDAOperationResult>> buildNextPossibleWordForRule(
        String currentInscription, String currentWord, StackDataStructure currentStack)
    {
        PDARule rule = generatePDARuleFromArcInscription(currentInscription);
        StackDataStructure clonedStack = (StackDataStructure) currentStack.clone();
        if (!updateStack(rule, clonedStack)) {
            return Optional.empty();
        }
        String resultingWord = currentWord;
        char toAdd = rule.letter;
        if (toAdd != EPSILON) {
            resultingWord += toAdd;
        }
        if (resultingWord.isBlank()) {
            resultingWord = String.valueOf(EPSILON);
        }
        String display =
            DISPLAY_FORMAT.formatted(currentWord, currentStack, rule, resultingWord, clonedStack);
        return Optional.of(
            new AbstractMap.SimpleEntry<>(
                display, new PDAOperationResult(resultingWord, clonedStack)));
    }

    /**
     * Retrieves the next possible new word based off of the given rule, word and prepared word and the current stack. The resulting word is
     * returned as an optional map entry where the key is the display representation and the value is a {@link PDAOperationResult}.
     *
     * @param currentInscription the current rule inscribed to an arc
     * @param currentWord the current word that is to be used when traversing the arc
     * @param preparedWord the word that's first letter has been prepared to be the next letter to consume
     * @param currentStack the current stack
     * @return an optional map entry where the key is the display representation and the value is a {@link PDAOperationResult}.
     */
    private static Optional<Map.Entry<String, PDAOperationResult>> retrieveNextValidWordForRule(
        String currentInscription, String currentWord, String preparedWord,
        StackDataStructure currentStack)
    {
        String resultingWord = null;
        String oldWord = null;
        PDARule rule = generatePDARuleFromArcInscription(currentInscription);
        StackDataStructure clonedStack = (StackDataStructure) currentStack.clone();
        if (rule.letter == EPSILON && (rule.requiredStackSymbol == EPSILON
            || currentStack.peek() == rule.requiredStackSymbol)) {
            //Stack is: [?] Arc is: EPSILON,EPSILON -> ? ||OR|| Stack is: [X] Arc is: EPSILON,X -> ?
            updateStack(rule, clonedStack);
            resultingWord = currentWord;
            oldWord = currentWord;
        }
        if (rule.letter != EPSILON && rule.letter == preparedWord.charAt(0)) {
            // Rule is: x, ? -> ? AND word is: x
            if (!updateStack(rule, clonedStack)) {
                return Optional.empty();
            }
            resultingWord = preparedWord.substring(1);
            oldWord = preparedWord;
            //change empty word to epsilon. user might have multiple options and epsilon is easier to understand.
            if (resultingWord.isEmpty()) {
                resultingWord = String.valueOf(EPSILON);
            }
        }
        if (resultingWord != null) {
            String formattedRule = rule.toString();
            String display = DISPLAY_FORMAT
                .formatted(oldWord, currentStack, formattedRule, resultingWord, clonedStack);
            return Optional.of(
                new AbstractMap.SimpleEntry<>(
                    display, new PDAOperationResult(resultingWord, clonedStack)));
        }
        return Optional.empty();
    }

    private static boolean updateStack(PDARule rule, StackDataStructure stack) {
        if (rule.requiredStackSymbol != EPSILON && stack.peek() == rule.requiredStackSymbol) {
            stack.pop();
        } else if (rule.requiredStackSymbol != EPSILON
            && stack.peek() != rule.requiredStackSymbol) {
            return false;
        }
        if (rule.newStackSymbol != EPSILON) {
            stack.push(rule.newStackSymbol);
        }
        return true;
    }

    private static Tuple selectAndFirePDAArc(HashMap<String, PDAOperationResult> nextWords) {
        if (nextWords.keySet().size() > 1) {
            //multiple possibilities
            PDAOperationResult chosenResult;
            if (SimulationSettingsManager.getManualSimulation()) {
                // let the user choose
                String chosenOperation =
                    (String) showBindingOptionsWindow(nextWords.keySet().toArray());
                chosenResult = nextWords.get(chosenOperation);
            } else {
                // take a random transition
                int r = (int) (Math.random() * nextWords.keySet().size());
                chosenResult = nextWords.get((String) nextWords.keySet().toArray()[r]);
            }
            String resultingWord = chosenResult.resultingWord;
            if (resultingWord.equals(String.valueOf(EPSILON))) {
                resultingWord = "";
            }
            return new Tuple(new Object[] { resultingWord, chosenResult.resultingStack }, null);
        } else {
            //only one option
            String chosenWord = (String) nextWords.keySet().toArray()[0];
            PDAOperationResult result = nextWords.get(chosenWord);
            return new Tuple(new Object[] { result.resultingWord, result.resultingStack }, null);
        }
    }

    private static String fireNFA(String currentWord, String arcInscription) {
        //1. prepare all possible tokens for consumption (^*, *, ^+, ^°, °, union)
        //2. match extracted words' first character against possibilities allowed by arc
        //3. if manual simulation is selected and multiple options exist: ask user for binding. otherwise, choose at random

        List<String> allowedByArc = splitNFAArcInscription(arcInscription);
        List<String> preparedWords = prepareTokenForConsumption(currentWord);

        if (SimulationSettingsManager.getSimulateWordMode()) {
            preparedWords.removeIf(s -> {
                if (allowedByArc.contains("")) {
                    return false;
                } else if (!s.isEmpty()) {
                    for (String arcInscr : allowedByArc) {
                        if (s.charAt(0) == arcInscr.charAt(0)) {
                            return false;
                        }
                    }
                }
                return true;
            });

            HashMap<String, String> nextWords = new HashMap<>();
            HashSet<String> options = new HashSet<>();
            for (String preparedWord : preparedWords) {
                for (String arcInscr : allowedByArc) {
                    if (arcInscr.isEmpty()) {
                        //epsilon arc, we add the currentWord
                        String display = "[" + currentWord + ", ε] → " + currentWord;
                        if (options.add(display)) {
                            nextWords.putIfAbsent(display, currentWord);
                        }
                    } else if (!preparedWord.isBlank()
                        && preparedWord.charAt(0) == arcInscr.charAt(0)) {
                        String resultingWord = preparedWord.substring(1);
                        if (resultingWord.isEmpty()) {
                            resultingWord = "ε";
                        }
                        String display =
                            "[" + preparedWord + ", " + arcInscr.charAt(0) + "] → " + resultingWord;
                        if (options.add(display)) {
                            nextWords.putIfAbsent(display, preparedWord.substring(1));
                        }
                    }
                }
            }
            if (options.size() > 1) {
                //multiple possibilities
                if (SimulationSettingsManager.getManualSimulation()) {
                    return nextWords.get((String) showBindingOptionsWindow(options.toArray()));
                } else {
                    int r = (int) (Math.random() * options.size());
                    return nextWords.get((String) options.toArray()[r]);
                }
            } else {
                //only one option
                if (allowedByArc.contains("")) {
                    return currentWord;
                } else {
                    return preparedWords.get(0).substring(1);
                }
            }
        } else {
            if (preparedWords.size() > 1) {
                boolean topLevelUnion = false;
                int insideBracket = 0;
                for (int i = 0; i < currentWord.length(); i++) {
                    switch (currentWord.charAt(i)) {
                        case '(' -> insideBracket++;
                        case ')' -> insideBracket--;
                        case '+', '|' -> {
                            if (insideBracket == 0) {
                                topLevelUnion = true;
                            }
                        }
                    }
                }
                if (topLevelUnion && !currentWord.startsWith("(")) {
                    currentWord = "(" + currentWord + ")";
                }
            }
            if (allowedByArc.size() > 1) {
                //multiple next letters
                if (SimulationSettingsManager.getManualSimulation()) {
                    //let the user choose
                    String[] options = new String[allowedByArc.size()];
                    HashMap<String, String> nextWords = new HashMap<>();
                    for (int i = 0; i < allowedByArc.size(); i++) {
                        String word = currentWord + allowedByArc.get(i);
                        if (word.isBlank()) {
                            word = "ε";
                        }
                        String letter = allowedByArc.get(i);
                        if (letter.isEmpty()) {
                            letter = "ε";
                        }
                        options[i] = "[" + currentWord + ", " + letter + "] → " + word;
                        nextWords.put(options[i], word);
                    }
                    return nextWords.get((String) showBindingOptionsWindow(options));
                } else {
                    int r = (int) (Math.random() * allowedByArc.size());
                    return currentWord + allowedByArc.get(r);
                }
            } else {
                //only one possible letter, add it
                return currentWord + allowedByArc.get(0);
            }
        }
    }

    /**
     * Prepares the given word by ensuring that the next token to be consumed is at index 0.
     * The possible starting characters are given by the kleene star, the union operation, or the ^+-operator.
     * Examples: <ul>
     * <li>a -> {a}</li>
     * <li>a* -> {>empty String<, aa^*}</li>
     * <li>a^+ -> aa^*</li>
     * <li>a+b -> {a, b}</li>
     * <li>a^++b -> {aa^*, b}</li>
     * <li>a+(b+c)^* -> {aa^*, b(b+c)^*, c(b+c)^*}</li>
     * <li>a*b*c*d^+ -> {aa*b*c*d^+, bb*c*d^+, cc*d^+, dd^*}</li>
     * </ul>
     *
     * @param currentWord for which the possible next words are to prepared
     * @return a list of strings, each starting with the next token to be consumed, or the empty String, if no token needs to be consumed to yield the empty string
     */
    public static List<String> prepareTokenForConsumption(String currentWord) {
        List<String> result = new ArrayList<>();
        if (currentWord == null) {
            throw new IllegalStateException("Word can't be null!");
        }
        if (currentWord.isEmpty()) {
            result.add("");
            return result;
        }
        //find all union operators at bracket level 0
        int openBracket = 0;
        List<Integer> unionOperators = new ArrayList<>();
        for (int i = 0; i < currentWord.length(); i++) {
            switch (currentWord.charAt(i)) {
                case '(' -> openBracket++;
                case ')' -> openBracket--;
                case '+' -> {
                    if (openBracket == 0 && (i == 0 || (currentWord.charAt(i - 1) != '^'))) {
                        unionOperators.add(i);
                    }
                }
                case '|' -> {
                    if (openBracket == 0) {
                        unionOperators.add(i);
                    }
                }
            }
        }
        //if union exists:
        //  call this method with substrings, excluding the union
        if (!unionOperators.isEmpty()) {
            int wordIndex = 0;
            for (Integer unionIndex : unionOperators) {
                //  aggregate results
                result.addAll(
                    prepareTokenForConsumption(currentWord.substring(wordIndex, unionIndex)));
                wordIndex = unionIndex + 1;
            }
            result.addAll(prepareTokenForConsumption(currentWord.substring(wordIndex)));
            return result;
        }
        //find the longest consecutive row of Kleene-groups starting from index 0
        int groupIndex = 0;
        boolean insideKleene = true;
        while (insideKleene && groupIndex < currentWord.length()) {
            insideKleene = false;
            if (currentWord.charAt(groupIndex) == '(') {
                openBracket = 1;
                int j = groupIndex + 1;
                while (openBracket > 0) {
                    switch (currentWord.charAt(j)) {
                        case '(' -> openBracket++;
                        case ')' -> openBracket--;
                    }
                    j++;
                }
                //after loop, j is index for first character after closed bracket
                if (j + 1 < currentWord.length()) {
                    // current group can't end on '°'.
                    // After '°', no character except a union operator is allowed.
                    // But it can't be a union, since we already split for those.
                    if (currentWord.charAt(groupIndex + 1) == ')') { //open and closed brackets next to each other, we skip the group
                        insideKleene = true;
                        if (currentWord.charAt(j) == '^') {
                            //()^
                            j++;
                        }
                        if (currentWord.charAt(j) == '*') {
                            //()^* or ()*
                            j++;
                        }
                        if (currentWord.charAt(j) == '+') {
                            //()^+   can't be ()+, since we split for union already
                            j++;
                        }
                        if (currentWord.charAt(j) == '°') { //should be illegal
                            //()^° or ()°
                            j++;
                        }
                        groupIndex = j;
                    } else if (currentWord.charAt(j) == '^') {
                        //(X)^
                        if (currentWord.charAt(j + 1) == '*') {
                            //(X)^* -> X(X)^*
                            insideKleene = true;
                            List<String> temp = prepareTokenForConsumption(
                                currentWord.substring(groupIndex + 1, j - 1));
                            for (String prefix : temp) {
                                result.add(prefix + currentWord.substring(groupIndex));
                            }
                            groupIndex = j + 2; //j pointed at '^', '*' came after, j + 2 looks at the next potential group.
                            if (groupIndex == currentWord.length()) {
                                //(X)^*$ -> ""
                                result.add("");
                            } //else we stay in while-loop
                        } else if (currentWord.charAt(j + 1) == '+') {
                            //(X)^+ -> X(X)^*
                            List<String> temp;
                            if (j + 2 == currentWord.length()) {
                                //(X)^+$ -> X(X)^*$
                                temp = prepareTokenForConsumption(
                                    currentWord.substring(groupIndex + 1, j - 1));
                                for (String prefix : temp) {
                                    result.add(
                                        prefix + currentWord.substring(groupIndex, j + 1) + "*");
                                }
                            } else {
                                //(X)^+b -> X(X)^*b
                                temp = prepareTokenForConsumption(
                                    currentWord.substring(groupIndex + 1, j - 1));
                                for (String prefix : temp) {
                                    result.add(
                                        prefix + currentWord.substring(groupIndex, j + 1) + "*"
                                            + currentWord.substring(j + 2));
                                }
                            }
                            if (temp.contains("")) {
                                //(X*)^+, (X^*)^+, (X^*+Y^*)^+
                                result.add("");
                            }
                        } else {
                            //we have an illegal state. '^' must be followed by either '+' or '*', according to syntax check
                            throw new IllegalStateException("Read '^' without '+' or '*'.");
                        }
                    } else {
                        if (currentWord.charAt(j) == '*') {
                            //(X)* -> X(X)*
                            insideKleene = true;
                            List<String> temp = prepareTokenForConsumption(
                                currentWord.substring(groupIndex + 1, j - 1));
                            for (String prefix : temp) {
                                result.add(prefix + currentWord.substring(groupIndex));
                            }
                            groupIndex = j + 1;
                            if (groupIndex == currentWord.length()) {
                                //a*$ -> ""$
                                result.add("");
                            } //else we stay in while-loop
                        } else {
                            //(X)b -> X'b
                            List<String> temp = prepareTokenForConsumption(
                                currentWord.substring(groupIndex + 1, j - 1));
                            for (String prefix : temp) {
                                result.add(prefix + currentWord.substring(j));
                            }
                        }
                    }
                } else if (j < currentWord.length()) {
                    //(X)j$
                    if (currentWord.charAt(j) == '*') {
                        //(X)*$ -> X(X)*$
                        insideKleene = true;
                        List<String> temp = prepareTokenForConsumption(
                            currentWord.substring(groupIndex + 1, j - 1));
                        for (String prefix : temp) {
                            result.add(prefix + currentWord.substring(groupIndex));
                        }
                        groupIndex = j + 1;
                        result.add("");//according to previous if, groupIndex is now equal to currentWord.length()
                    } else if (currentWord.charAt(j) == '°') {
                        //(X)°$ -> X(X)°$
                        List<String> temp = prepareTokenForConsumption(
                            currentWord.substring(groupIndex + 1, j - 1));
                        for (String prefix : temp) {
                            result.add(prefix + currentWord.substring(groupIndex));
                        }
                        groupIndex = j + 1;//according to previous if, groupIndex is now equal to currentWord.length()
                    } else {
                        //(X)b$ -> Xb$
                        List<String> temp = prepareTokenForConsumption(
                            currentWord.substring(groupIndex + 1, j - 1));
                        for (String prefix : temp) {
                            result.add(prefix + currentWord.substring(j));
                        }
                    }
                } else {
                    //(X)$ -> X
                    result.addAll(
                        prepareTokenForConsumption(currentWord.substring(groupIndex + 1, j - 1)));
                }
                //--------------------- group did not start with an open bracket --------------------------------
            } else if (groupIndex + 2 < currentWord.length()) {
                if (currentWord.charAt(groupIndex + 1) == '^') {
                    //a^
                    if (currentWord.charAt(groupIndex + 2) == '*') {
                        //a^* -> aa^*
                        insideKleene = true;
                        result.add(
                            currentWord.charAt(groupIndex) + currentWord.substring(groupIndex));
                        groupIndex += 3; //+1 for the char we analyzed, +2 for '^*'
                        if (groupIndex == currentWord.length()) {
                            //a^*$ -> ""
                            result.add("");
                        } //else we stay in while-loop
                    } else if (currentWord.charAt(groupIndex + 2) == '+') {
                        //a^+
                        if (groupIndex + 3 == currentWord.length()) {
                            //a^+$ -> aa^*$
                            result.add(
                                "" + currentWord.charAt(groupIndex) + currentWord.charAt(groupIndex)
                                    + "^*");
                        } else {
                            //a^+b -> aa^*b
                            result.add(
                                "" + currentWord.charAt(groupIndex) + currentWord.charAt(groupIndex)
                                    + "^*" + currentWord.substring(groupIndex + 3));
                        }
                    } else if (currentWord.charAt(groupIndex + 2) == '°') {
                        //a^° -> aa^°
                        //we don't care if any chars come after '°'. this is checked by FASyntaxChecker
                        result.add(
                            currentWord.charAt(groupIndex) + currentWord.substring(groupIndex));
                    } else {
                        //we have an illegal state. '^' must be followed by either '°', '+' or '*', according to syntax check
                        throw new IllegalStateException("Read '^' without '+' or '*'.");
                    }
                } else {
                    //a*, a°, or ab. a+ can't be, since + is a union operator, and we already split for those.
                    if (currentWord.charAt(groupIndex + 1) == '*') {
                        //a* -> a*
                        insideKleene = true;
                        result.add(
                            currentWord.charAt(groupIndex) + currentWord.substring(groupIndex));
                        groupIndex += 2;
                        if (groupIndex == currentWord.length()) {
                            //a*$ -> ""$
                            result.add("");
                        } //else we stay in while-loop
                    } else if (currentWord.charAt(groupIndex + 1) == '°') {
                        //a° -> aa°
                        result.add(
                            currentWord.charAt(groupIndex) + currentWord.substring(groupIndex));
                    } else {
                        //ab -> ab
                        result.add(currentWord.substring(groupIndex));
                    }
                }
            } else if (groupIndex + 1 < currentWord.length()) {
                //a*$ or a°$ or ab$
                if (currentWord.charAt(groupIndex + 1) == '*') {
                    //a*$ -> aa*$
                    insideKleene = true;
                    result.add(currentWord.charAt(groupIndex) + currentWord.substring(groupIndex));
                    groupIndex += 2;
                    result.add("");//according to previous if, groupIndex is now equal to currentWord.length()
                } else if (currentWord.charAt(groupIndex + 1) == '°') {
                    //a°$ -> aa°$
                    result.add(currentWord.charAt(groupIndex) + currentWord.substring(groupIndex));
                } else {
                    //ab$ -> ab$
                    result.add(currentWord.substring(groupIndex));
                }
            } else {
                //a$ -> //a$
                result.add(currentWord.charAt(groupIndex) + "");
            }
        }

        return result;
    }

    private static Object showBindingOptionsWindow(Object[] options) {
        JFrame jFrame = new JFrame("Multiple possible bindings:");
        JLabel text = new JLabel("Multiple possible bindings found. Chose one:");
        Object result = JOptionPane.showInputDialog(
            jFrame, text, "Possible Bindings", JOptionPane.INFORMATION_MESSAGE, null, options,
            options[0]);
        if (result == null) {
            return options[0];
        } else {
            return result;
        }
    }

    /**
     * Convenience method to extract all possible letters that the arc accepts.
     * Commas are treated as separators. E.g.: <ul>
     * <li>'a,b' -> {'a','b'}</li>
     * <li>'a,' -> {'a',''}</li>
     * <li>'a,b,a' -> {'a','b'}</li>
     * </ul>
     *
     * @param arcInscription the inscription from which the letters are to be extracted
     * @return a List of Strings of length 1
     */
    public static List<String> splitNFAArcInscription(String arcInscription) {
        if (arcInscription == null) {
            throw new IllegalStateException("Arc inscription may not be null!");
        }
        arcInscription = arcInscription.replaceAll("\\s", "");
        arcInscription = arcInscription.replaceAll("\n", "");
        String[] parts = arcInscription.split(",");
        HashSet<String> allowed = new HashSet<>(Arrays.asList(parts));
        if (parts.length * 2 - 1 != arcInscription.length()) {
            allowed.add("");
        }
        return allowed.stream().toList();
    }

    private static PDARule generatePDARuleFromArcInscription(String arcInscription) {
        if (arcInscription == null) {
            throw new IllegalStateException("Arc inscription may not be null!");
        }
        String[] extractedLetters = new String[3];
        int colonIndex = arcInscription.indexOf(',');
        extractedLetters[0] = arcInscription.substring(0, colonIndex).strip();
        int arrowIndex = arcInscription.indexOf("->");
        extractedLetters[1] = arcInscription.substring(colonIndex + 1, arrowIndex).strip();
        extractedLetters[2] = arcInscription.substring(arrowIndex + 2).strip();
        for (int i = 0; i < extractedLetters.length; i++) {
            if (extractedLetters[i].isEmpty()) {
                extractedLetters[i] = String.valueOf(EPSILON);
            }
        }
        return new PDARule(
            extractedLetters[0].charAt(0), extractedLetters[1].charAt(0),
            extractedLetters[2].charAt(0));
    }

    private record PDAOperationResult(String resultingWord, StackDataStructure resultingStack) {
    }

    private record PDARule(char letter, char requiredStackSymbol, char newStackSymbol) {
        @Override
        public String toString() {
            return PDA_RULE_FORMAT.formatted(letter, requiredStackSymbol, newStackSymbol);
        }
    }
}
