package org.workcraft.plugins.wtg.converter;

import org.workcraft.dom.math.MathNode;
import org.workcraft.dom.references.Identifier;
import org.workcraft.exceptions.FormatException;
import org.workcraft.exceptions.InvalidConnectionException;
import org.workcraft.plugins.dtd.Signal;
import org.workcraft.plugins.dtd.*;
import org.workcraft.plugins.stg.*;
import org.workcraft.plugins.wtg.*;
import org.workcraft.types.Triple;

import java.util.*;

import static org.workcraft.plugins.wtg.utils.WtgUtils.getInitialSignalStates;
import static org.workcraft.plugins.wtg.utils.WtgUtils.getUnstableSignalNames;

public class WtgToStgConverter {

    private final Wtg srcModel;
    private final Stg dstModel;

    private final Map<State, StgPlace> stateToPlaceMap;
    private final Map<String, UnstableSignalStg> unstableSignalToStgMap;
    private final Map<Waveform, Triple<NamedTransition, NamedTransition, StgPlace>> waveformToEntryExitInactiveMap;
    private final Map<Event, NamedTransition> eventToTransitionMap;

    public WtgToStgConverter(Wtg srcModel, Stg dstModel) {
        this.srcModel = srcModel;
        this.dstModel = dstModel;
        stateToPlaceMap = convertStates();
        unstableSignalToStgMap = createSignalStatePlaces();
        waveformToEntryExitInactiveMap = convertWaveforms();
        eventToTransitionMap = convertEvents();
        convertConnections();
        convertGuards();
    }

    private Map<State, StgPlace> convertStates() {
        Map<State, StgPlace> result = new HashMap<>();
        for (State state: srcModel.getStates()) {
            String name = srcModel.getName(state);
            StgPlace place = dstModel.createPlace(name, null);
            place.setTokens(state.isInitial() ? 1 : 0);
            result.put(state, place);
        }
        return result;
    }

    private Map<String, UnstableSignalStg> createSignalStatePlaces() {
        Map<String, UnstableSignalStg> result = new HashMap<>();
        Map<String, Signal.State> initialSignalStates = getInitialSignalStates(srcModel);
        for (String signalName: getUnstableSignalNames(srcModel)) {
            // Only input signals can be unstable
            org.workcraft.plugins.stg.Signal.Type signalType = org.workcraft.plugins.stg.Signal.Type.INPUT;

            StgPlace lowPlace = dstModel.createPlace(getLowStateName(signalName), null);
            StgPlace highPlace = dstModel.createPlace(getHighStateName(signalName), null);
            StgPlace unstablePlace = dstModel.createPlace(getUnstableStateName(signalName), null);
            StgPlace stablePlace = dstModel.createPlace(getStableStateName(signalName), null);

            Signal.State initialSignalState = initialSignalStates.get(signalName);
            if (initialSignalState == Signal.State.UNSTABLE) {
                stablePlace.setTokens(0);
                unstablePlace.setTokens(1);
            } else {
                stablePlace.setTokens(1);
                unstablePlace.setTokens(0);
            }
            if (initialSignalState == Signal.State.HIGH) {
                highPlace.setTokens(1);
                lowPlace.setTokens(0);
            } else {
                //If the initial Signal State is unstable or stable, we default to 0. This is an arbitrary decision
                highPlace.setTokens(0);
                lowPlace.setTokens(1);
            }

            SignalTransition riseTransition = dstModel.createSignalTransition(signalName,
                    SignalTransition.Direction.PLUS, null);
            riseTransition.setSignalType(signalType);

            SignalTransition fallTransition = dstModel.createSignalTransition(signalName,
                    SignalTransition.Direction.MINUS, null);
            fallTransition.setSignalType(signalType);

            try {
                dstModel.connect(lowPlace, riseTransition);
                dstModel.connect(riseTransition, highPlace);
                dstModel.connect(highPlace, fallTransition);
                dstModel.connect(fallTransition, lowPlace);
                // Read-arc to fall transition
                dstModel.connect(fallTransition, unstablePlace);
                dstModel.connect(unstablePlace, fallTransition);
                // Read-arc to rise transition
                dstModel.connect(riseTransition, unstablePlace);
                dstModel.connect(unstablePlace, riseTransition);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }

            UnstableSignalStg signalStg = new UnstableSignalStg(lowPlace, highPlace,
                    fallTransition, riseTransition, stablePlace, unstablePlace);
            result.put(signalName, signalStg);
        }
        return result;
    }

    private Map<Waveform, Triple<NamedTransition, NamedTransition, StgPlace>> convertWaveforms() {
        Map<Waveform, Triple<NamedTransition, NamedTransition, StgPlace>> result = new HashMap<>();
        for (Waveform waveform : srcModel.getWaveforms()) {
            result.put(waveform, convertWaveform(waveform));
        }
        return result;
    }

    private Triple<NamedTransition, NamedTransition, StgPlace> convertWaveform(Waveform waveform) {
        Set<MathNode> preset = srcModel.getPreset(waveform);
        Set<MathNode> postset = srcModel.getPostset(waveform);
        if ((preset.size() != 1) || (postset.size() != 1)) {
            String waveformName = srcModel.getName(waveform);
            throw new FormatException("Incorrect preset and/or postset of waveform '" + waveformName + "'");
        }
        String waveformName = Identifier.truncateNamespaceSeparator(srcModel.getName(waveform));
        // Waveform entry
        DummyTransition entryTransition = null;
        MathNode entryNode = preset.iterator().next();
        if (entryNode instanceof State) {
            State entryState = (State) entryNode;
            StgPlace entryPlace = stateToPlaceMap.get(entryState);
            entryTransition = dstModel.createDummyTransition(getEntryEventName(waveformName), null);
            try {
                dstModel.connect(entryPlace, entryTransition);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }
        }
        // Waveform exit
        DummyTransition exitTransition = null;
        MathNode exitNode = postset.iterator().next();
        if (exitNode instanceof State) {
            State exitState = (State) exitNode;
            StgPlace exitPlace = stateToPlaceMap.get(exitState);
            exitTransition = dstModel.createDummyTransition(getExitEventName(waveformName), null);
            try {
                dstModel.connect(exitTransition, exitPlace);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }
        }
        // Waveform inactive place
        StgPlace inactivePlace = dstModel.createPlace(getInactivePlaceName(waveformName), null);
        inactivePlace.setTokens(1);
        try {
            dstModel.connect(inactivePlace, entryTransition);
            dstModel.connect(exitTransition, inactivePlace);
        } catch (InvalidConnectionException e) {
            throw new RuntimeException(e);
        }
        return Triple.of(entryTransition, exitTransition, inactivePlace);
    }

    private Map<Event, NamedTransition> convertEvents() {
        Map<Event, NamedTransition> result = new HashMap<>();
        for (Waveform waveform : srcModel.getWaveforms()) {
            result.putAll(convertEvents(waveform));
        }
        return result;
    }

    private Map<Event, NamedTransition> convertEvents(Waveform waveform) {
        Map<Event, NamedTransition> result = new HashMap<>();
        // Entry events
        result.putAll(convertEntryEvents(waveform));
        // Exit events
        result.putAll(convertExitEvents(waveform));
        // Transition events
        result.putAll(convertTransitionEvents(waveform));
        return result;
    }

    private Map<Event, NamedTransition> convertEntryEvents(Waveform waveform) {
        Map<Event, NamedTransition> result = new HashMap<>();
        NamedTransition entryTransition = waveformToEntryExitInactiveMap.get(waveform).getFirst();
        for (EntryEvent entryEvent : srcModel.getEntries(waveform)) {
            result.put(entryEvent, entryTransition);
        }
        return result;
    }

    private Map<Event, NamedTransition> convertExitEvents(Waveform waveform) {
        Map<Event, NamedTransition> result = new HashMap<>();
        NamedTransition exitTransition = waveformToEntryExitInactiveMap.get(waveform).getSecond();
        for (ExitEvent signalExit : srcModel.getExits(waveform)) {
            result.put(signalExit, exitTransition);
        }
        return result;
    }

    private Map<Event, NamedTransition> convertTransitionEvents(Waveform waveform) {
        Map<Event, NamedTransition> result = new HashMap<>();
        for (TransitionEvent srcTransition : srcModel.getTransitions(waveform)) {
            TransitionEvent.Direction direction = srcTransition.getDirection();
            if (direction == TransitionEvent.Direction.DESTABILISE) {
                result.put(srcTransition, convertDestabiliseTransitionEvent(srcTransition));
            } else if (srcModel.getPreviousState(srcTransition) == Signal.State.UNSTABLE) {
                result.put(srcTransition, convertStabiliseTransitionEvent(srcTransition));
            } else {
                Signal signal = srcTransition.getSignal();
                String signalName = srcModel.getName(signal);
                SignalTransition dstTransition = dstModel.createSignalTransition(signalName,
                        convertWtgToStgDirection(direction), null);
                dstTransition.setSignalType(convertWtgToStgType(signal.getType()));
                result.put(srcTransition, dstTransition);

                if (unstableSignalToStgMap.containsKey(signalName)) {
                    convertUnstableSignalStableTransitionEvent(srcTransition, dstTransition);
                }
            }
        }
        return result;
    }

    private DummyTransition convertDestabiliseTransitionEvent(TransitionEvent srcTransition) {
        Signal signal = srcTransition.getSignal();
        String signalName = srcModel.getName(signal);
        String dummyName = getDestabiliseEventName(signalName);
        DummyTransition dstTransition = dstModel.createDummyTransition(dummyName, null);
        UnstableSignalStg signalStg = unstableSignalToStgMap.get(signalName);
        if (signalStg != null) {
            try {
                dstModel.connect(signalStg.stablePlace, dstTransition);
                dstModel.connect(dstTransition, signalStg.unstablePlace);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }
        }
        return dstTransition;
    }

    private DummyTransition convertStabiliseTransitionEvent(TransitionEvent srcTransition) {
        Signal signal = srcTransition.getSignal();
        String signalName = srcModel.getName(signal);
        String dummyName = getStabiliseEventName(signalName);
        DummyTransition dstTransition = dstModel.createDummyTransition(dummyName, null);
        UnstableSignalStg signalStg = unstableSignalToStgMap.get(signalName);
        if (signalStg != null) {
            try {
                dstModel.connect(signalStg.unstablePlace, dstTransition);
                dstModel.connect(dstTransition, signalStg.stablePlace);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }
            if (srcTransition.getDirection() == TransitionEvent.Direction.RISE) {
                // Signal is stable high
                try {
                    dstModel.connect(signalStg.highPlace, dstTransition);
                    dstModel.connect(dstTransition, signalStg.highPlace);
                } catch (InvalidConnectionException e) {
                    throw new RuntimeException(e);
                }
            } else if (srcTransition.getDirection() == TransitionEvent.Direction.FALL) {
                // Signal is stable low
                try {
                    dstModel.connect(signalStg.lowPlace, dstTransition);
                    dstModel.connect(dstTransition, signalStg.lowPlace);
                } catch (InvalidConnectionException e) {
                    throw new RuntimeException(e);
                }
            }
        }
        return dstTransition;
    }

    private void convertUnstableSignalStableTransitionEvent(TransitionEvent srcTransition, SignalTransition dstTransition) {
        UnstableSignalStg signalStg = unstableSignalToStgMap.get(srcModel.getName(srcTransition.getSignal()));
        if (srcTransition.getDirection() == TransitionEvent.Direction.RISE) {
            // Signal goes from stable zero to stable one
            try {
                dstModel.connect(signalStg.lowPlace, dstTransition);
                dstModel.connect(dstTransition, signalStg.highPlace);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }
        } else if (srcTransition.getDirection() == TransitionEvent.Direction.FALL) {
            // Signal goes from stable one to stable zero
            try {
                dstModel.connect(signalStg.highPlace, dstTransition);
                dstModel.connect(dstTransition, signalStg.lowPlace);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }
        }
    }

    private SignalTransition.Direction convertWtgToStgDirection(TransitionEvent.Direction direction) {
        switch (direction) {
        case RISE: return SignalTransition.Direction.PLUS;
        case FALL: return SignalTransition.Direction.MINUS;
        default: return SignalTransition.Direction.TOGGLE;
        }
    }

    private org.workcraft.plugins.stg.Signal.Type convertWtgToStgType(Signal.Type type) {
        switch (type) {
        case INPUT: return org.workcraft.plugins.stg.Signal.Type.INPUT;
        case OUTPUT: return org.workcraft.plugins.stg.Signal.Type.OUTPUT;
        case INTERNAL: return org.workcraft.plugins.stg.Signal.Type.INTERNAL;
        default: return null;
        }
    }

    private void convertConnections() {
        for (Waveform waveform : srcModel.getWaveforms()) {
            convertConnections(waveform);
        }
    }

    private void convertConnections(Waveform waveform) {
        for (Event event : srcModel.getEvents(waveform)) {
            NamedTransition fromTransition = eventToTransitionMap.get(event);
            for (MathNode node: srcModel.getPostset(event)) {
                NamedTransition toTransition = eventToTransitionMap.get(node);
                if (isRedundantConnection(event, node)) continue;
                try {
                    dstModel.connect(fromTransition, toTransition);
                } catch (InvalidConnectionException e) {
                    throw new RuntimeException(e);
                }
            }
        }
    }

    private boolean isRedundantConnection(MathNode fromNode, MathNode toNode) {
        if (fromNode instanceof EntryEvent) {
            Set<MathNode> preset = srcModel.getPreset(toNode);
            if ((preset.size() > 1) && preset.contains(fromNode)) {
                return true;
            }
        }
        if (toNode instanceof ExitEvent) {
            Set<MathNode> postset = srcModel.getPostset(fromNode);
            if ((postset.size() > 1) && postset.contains(toNode)) {
                return true;
            }
        }
        if ((fromNode instanceof  EntryEvent) && (toNode instanceof ExitEvent)) {
            return true;
        }
        if ((fromNode instanceof TransitionEvent) && (toNode instanceof TransitionEvent)) {
            if (isThereAlternativePath((TransitionEvent) fromNode, (TransitionEvent) toNode)) {
                return true;
            }
        }

        return false;
    }

    private boolean isThereAlternativePath(TransitionEvent fromTransition, TransitionEvent toTransition) {
        if (srcModel.getPostset(fromTransition).size() <= 1) {
            return false;
        }
        Queue<Event> toVisit = new LinkedList<>();
        // There should be no loops, so visitedEvents should not be necessary
        // Yet, using it prevents an infinite loop if something else fails
        Set<Event> visitedEvents = new HashSet<>();
        for (MathNode node : srcModel.getPreset(toTransition)) {
            if (node instanceof TransitionEvent) {
                if (node != fromTransition) {
                    toVisit.add((Event) node);
                    visitedEvents.add((Event) node);
                }
            }
        }

        while (!toVisit.isEmpty()) {
            Event event = toVisit.poll();
            if (event instanceof TransitionEvent) {
                for (MathNode node : srcModel.getPreset(event)) {
                    Event previousEvent = (Event) node;
                    if (previousEvent == fromTransition) {
                        return true;
                    }
                    if ((previousEvent.getSignal() != fromTransition.getSignal()) &&
                            (!visitedEvents.contains(previousEvent))) {
                        toVisit.add(previousEvent);
                        visitedEvents.add(previousEvent);
                    }
                }
            }
        }
        return false;
    }

    private void convertGuards() {
        for (Waveform waveform : srcModel.getWaveforms()) {
            convertGuard(waveform);
        }
    }

    private void convertGuard(Waveform waveform) {
        NamedTransition entryTransition = waveformToEntryExitInactiveMap.get(waveform).getFirst();
        Guard guard = waveform.getGuard();
        for (String signalName : guard.keySet()) {
            UnstableSignalStg signalStg = unstableSignalToStgMap.get(signalName);
            if (signalStg == null) {
                throw new RuntimeException("Cannot find signal '" + signalName + "' used in the guard.");
            }
            StgPlace place = guard.get(signalName) ? signalStg.highPlace : signalStg.lowPlace;
            try {
                // Read-arc from STABLE place
                dstModel.connect(signalStg.stablePlace, entryTransition);
                dstModel.connect(entryTransition, signalStg.stablePlace);
                // Read-arc from HIGH or LOW place
                dstModel.connect(place, entryTransition);
                dstModel.connect(entryTransition, place);
            } catch (InvalidConnectionException e) {
                throw new RuntimeException(e);
            }
        }
    }

    public static String getLowStateName(String signalName) {
        return signalName + WtgSettings.getLowStateSuffix();
    }

    public static String getHighStateName(String signalName) {
        return signalName + WtgSettings.getHighStateSuffix();
    }

    public static String getStableStateName(String signalName) {
        return signalName + WtgSettings.getStableStateSuffix();
    }

    public static String getUnstableStateName(String signalName) {
        return signalName + WtgSettings.getUnstableStateSuffix();
    }

    public static String getStabiliseEventName(String signalName) {
        return signalName + WtgSettings.getStabiliseEventSuffix();
    }

    public static String getDestabiliseEventName(String signalName) {
        return signalName + WtgSettings.getDestabiliseEventSuffix();
    }

    public static String getInactivePlaceName(String signalName) {
        return signalName + WtgSettings.getInactivePlaceSuffix();
    }

    public static String getEntryEventName(String signalName) {
        return signalName + WtgSettings.getEntryEventSuffix();
    }

    public static String getExitEventName(String signalName) {
        return signalName + WtgSettings.getExitEventSuffix();
    }

    public Wtg getSrcModel() {
        return srcModel;
    }

    public Stg getDstModel() {
        return dstModel;
    }

    public boolean isRelated(MathNode highLevelNode, MathNode node) {
        boolean result = false;
        if (highLevelNode instanceof Event) {
            NamedTransition relatedTransition = getRelatedTransition((Event) highLevelNode);
            result = node == relatedTransition;
        } else if (highLevelNode instanceof State) {
            StgPlace relatedPlace = getRelatedPlace((State) highLevelNode);
            result = node == relatedPlace;
        }
        return result;
    }

    public StgPlace getRelatedPlace(State state) {
        return stateToPlaceMap.get(state);
    }

    public NamedTransition getRelatedTransition(Event event) {
        return eventToTransitionMap.get(event);
    }

    public NamedTransition getEnabledUnstableTransition(Signal signal) {
        String signalName = srcModel.getName(signal);
        UnstableSignalStg unstableSignalStg = unstableSignalToStgMap.get(signalName);
        if (unstableSignalStg != null) {
            if (unstableSignalStg.unstablePlace.getTokens() > 0) {
                if (unstableSignalStg.highPlace.getTokens() > 0) {
                    return unstableSignalStg.fallTransition;
                }
                if (unstableSignalStg.lowPlace.getTokens() > 0) {
                    return unstableSignalStg.riseTransition;
                }
            }
        }
        return null;
    }

    public boolean isActiveWaveform(Waveform waveform) {
        StgPlace inactivePlace = waveformToEntryExitInactiveMap.get(waveform).getThird();
        return inactivePlace.getTokens() == 0;
    }

}
