package ta;

import java.io.IOException;
import java.util.AbstractMap;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.stream.Collectors;

import org.antlr.v4.runtime.ANTLRFileStream;
import org.antlr.v4.runtime.ANTLRInputStream;
import org.antlr.v4.runtime.CommonTokenStream;

import com.google.common.base.Preconditions;

import ta.declarations.BoundedVariableDecl;
import ta.declarations.ClockDecl;
import ta.declarations.VariableDecl;
import ta.expressions.Value;
import ta.parser.TALexer;
import ta.parser.TAParser;
import ta.state.State;
import ta.transition.Transition;
import ta.visitors.TAVisitor;

public class TA {

	public static int IDCOUNTER = 0;
	private final int id;
	private final Set<VariableDecl> variableDeclaration;

	private final Set<ClockDecl> clockDeclarations;

	private List<String> actions;
	private List<String> sendActions;
	private List<String> receiveActions;

	/**
	 * The name of the timed automaton
	 */
	private final String identifier;

	/**
	 * The initial state of the timed automaton
	 */
	private final State initialState;

	/**
	 * The atomic propositions of the timed automaton
	 */
	private final Set<AP> atomicPropositions;

	/**
	 * The states of the timed automaton
	 */
	private final Set<State> states;

	private final Set<Clock> clocks;
	private final Set<Clock> allclocks;

	private final Set<Variable> variables;
	private final Set<Variable> allVariables;
	/**
	 * The transitions of the timed automaton
	 */
	private final Set<Transition> transitions;

	/**
	 * keeps the outgoing transitions for each state
	 */
	private final Map<State, Set<Transition>> outTransitions;

	private final Map<Entry<State, State>, Set<Transition>> mapSourceDestinationTransitions;

	private final Map<State, Set<State>> successors;
	
	public boolean containsVariable(String variableId) {
		return this.variableDeclaration.stream().map(d -> d.getId())
				.collect(Collectors.toSet()).contains(variableId);
	}
	
	
	public boolean isBounded(String variableId) {
		return this.variableDeclaration.stream().filter(d -> d instanceof BoundedVariableDecl).map(d -> d.getId())
				.collect(Collectors.toSet()).contains(variableId);
	}

	public Set<Integer> getBound(String variableId) {
		Set<Integer> retSet = new HashSet<>();
		this.variableDeclaration.stream().filter(d -> d instanceof BoundedVariableDecl)
				.map(d -> ((BoundedVariableDecl) d).getValues()).forEach(c -> retSet.addAll(c));
		return retSet;
	}

	public int getNumberStates() {
		return this.states.size();
	}

	public TA(String identifier, Set<AP> atomicPropositions, Set<State> states, Set<Transition> transitions,
			State initialState, Set<Clock> clocks, Set<Variable> variables, Set<VariableDecl> variableDeclaration,
			Set<ClockDecl> clockDeclarations) {
		Preconditions.checkNotNull(states, "The set of the states cannot be null");
		Preconditions.checkNotNull(clocks, "The set of the clocks cannot be null");
		Preconditions.checkNotNull(variables, "The set of the variables cannot be null");
		this.id = IDCOUNTER;
		IDCOUNTER++;
		this.identifier = identifier;
		if (atomicPropositions != null) {
			this.atomicPropositions = new HashSet<>(atomicPropositions);
		} else {
			this.atomicPropositions = new HashSet<>();
		}
		this.states = new HashSet<>(states);
		this.transitions = new HashSet<>(transitions);
		this.initialState = initialState;
		this.clocks = clocks;
		this.outTransitions = new HashMap<>();
		this.variables = variables;
		this.allclocks = new HashSet<>(clocks);
		this.allVariables = new HashSet<>(variables);

		this.actions = new ArrayList<>();
		this.sendActions = new ArrayList<>();
		this.receiveActions = new ArrayList<>();
		this.states.forEach(s -> this.outTransitions.put(s, new HashSet<>()));
		this.transitions.forEach(t -> {
			Preconditions.checkArgument(this.outTransitions.containsKey(t.getSource()),
					"The state " + t.getSource() + "is not contained in the states of the TA");

			this.outTransitions.get(t.getSource()).add(t);
			t.getGuard().getClockConstraints().forEach(c -> allclocks.addAll(c.getClocks()));
			t.getAssignement().getClockassigments().forEach(c -> allclocks.add(c.getClock()));
			t.getGuard().getConditions().forEach(g -> allVariables.addAll(g.getVariables()));
			t.getAssignement().getVariableassigments().forEach(v -> allVariables.add(v.getVariable()));
			if (t.getSync() != null && t.getSync().getEvent() != null) {
				if (t.getSync().getOperator() != "TAU" && t.getSync().getOperator() != "tau") {
					if (!this.actions.contains(t.getSync().getEvent())) {
						this.actions.add(t.getSync().getEvent());
					}
					if (!this.sendActions.contains(t.getSync().getEvent()) && t.getSync().getOperator().equals("!")) {
						this.sendActions.add(t.getSync().getEvent());
					}
					if (!this.receiveActions.contains(t.getSync().getEvent())
							&& t.getSync().getOperator().equals("?")) {
						this.receiveActions.add(t.getSync().getEvent());
					}
				}
			}
		});

		this.variableDeclaration = variableDeclaration;
		this.clockDeclarations = clockDeclarations;

		this.mapSourceDestinationTransitions = new HashMap<>();

		for (Transition t : this.transitions) {
			if (!this.mapSourceDestinationTransitions
					.containsKey(new AbstractMap.SimpleEntry<>(t.getSource(), t.getDestination()))) {
				Set<Transition> associatedtransitions = new HashSet<>();
				associatedtransitions.add(t);
				this.mapSourceDestinationTransitions
						.put(new AbstractMap.SimpleEntry<>(t.getSource(), t.getDestination()), associatedtransitions);
			} else {
				this.mapSourceDestinationTransitions
						.get(new AbstractMap.SimpleEntry<>(t.getSource(), t.getDestination())).add(t);
			}
		}
		
		
		this.successors=new HashMap<>();
		
		for(State s: this.states){
			this.successors.put(s, new HashSet<>());
		}
		for (Transition t : this.transitions) {
			this.successors.get(t.getSource()).add(t.getDestination());
		}
	}

	public Set<State> successors(State s){
		return this.successors.get(s);
	}
	public Set<Transition> getTransitions(State source, State destination) {
		if (this.mapSourceDestinationTransitions.containsKey(new AbstractMap.SimpleEntry<>(source, destination))) {
			return this.mapSourceDestinationTransitions.get(new AbstractMap.SimpleEntry<>(source, destination));
		} else {
			return new HashSet<>();
		}
	}

	public Set<Variable> getAllVariables() {
		return allVariables;
	}

	public Set<Clock> getAllclocks() {
		return allclocks;
	}

	public Set<Variable> getVariables() {
		return variables;
	}

	public Value getInitialValue(Variable v) {

		for (VariableDecl i : this.variableDeclaration) {
			if (i.getId().equals(v.getName())) {
				return new Value(Integer.toString(i.getExp().evaluate()));
			}
		}
		return new Value(Integer.toString(0));
	}

	public Set<Transition> getOutgoingTransitions(State state) {
		Preconditions.checkNotNull(state, "The state cannot be null");
		return this.outTransitions.get(state);
	}

	public <T> T accept(TAVisitor<T> visitor) {
		return visitor.visit(this);
	}

	public Set<AP> getAtomicPropositions() {
		return Collections.unmodifiableSet(atomicPropositions);
	}

	public Set<State> getStates() {
		return Collections.unmodifiableSet(states);
	}

	public Set<Transition> getTransitions() {
		return Collections.unmodifiableSet(transitions);
	}

	public State getInitialState() {
		return initialState;
	}

	public String getIdentifier() {
		return identifier;
	}

	/**
	 * returns the set of the clocks of the TA
	 * 
	 * @return the set of the clocks of the TA
	 */
	public Set<Clock> getClocks() {

		return Collections.unmodifiableSet(clocks);
	}

	public Set<VariableDecl> getDeclarations() {
		return this.variableDeclaration;
	}

	/**
	 * {@inheritDoc}
	 */
	@Override
	public String toString() {

		StringBuilder builder = new StringBuilder();
		builder.append("-----------------------------TIMED AUTOMATON----------------------------- \n");

		builder.append("TA \n");
		builder.append("id: " + this.id + "\n");
		builder.append("\t" + this.identifier + "\n");
		builder.append("clocks: \n");
		builder.append("\t");
		this.clocks.forEach(c -> builder.append(c + ",\t"));
		builder.append("\n");
		builder.append("variables: \n");
		builder.append("\t");
		this.variables.forEach(c -> builder.append(c + ",\t"));
		builder.append("\n");
		builder.append("initialstate \n");
		builder.append("\t" + this.getInitialState() + "\n");
		builder.append("states \n");
		this.states.forEach(s -> builder.append("\t" + s + ",\n"));
		builder.append("transitions \n");
		this.transitions.forEach(t -> builder.append("\t" + t + ",\n"));
		builder.append("--------------------------\n");
		builder.append("DECLARATION \n");
		builder.append("variables \n");
		this.variableDeclaration.forEach(v -> builder.append("\t" + v + ",\n"));
		builder.append("clocks \n");

		this.clockDeclarations.forEach(v -> builder.append("\t" + v + ",\n"));

		builder.append("-------------------------------------------------------------------------------- \n");
		return builder.toString();
	}

	public static TA parse(String filePath) throws IOException {
		ANTLRInputStream input = new ANTLRFileStream(ClassLoader.getSystemResource(filePath).getPath());
		TALexer lexer = new TALexer(input);
		CommonTokenStream tokens = new CommonTokenStream(lexer);
		TAParser parser = new TAParser(tokens);
		parser.setBuildParseTree(true);
		SystemDecl system = parser.ta().systemret;

		TA ta = system.getTimedAutomata().iterator().next();
		return ta;
	}

	public Set<Variable> getLocalVariables() {
		return this.variableDeclaration.stream().map(v -> new Variable(v.getId())).collect(Collectors.toSet());
	}

	public Set<Clock> getLocalClocks() {
		return this.clockDeclarations.stream().map(cdc -> new Clock(cdc.getId())).collect(Collectors.toSet());
	}

	public List<String> getActions() {
		return Collections.unmodifiableList(actions);
	}

	public List<String> sendActions() {
		return Collections.unmodifiableList(this.sendActions);
	}

	public List<String> reveiveActions() {
		return Collections.unmodifiableList(this.receiveActions);
	}

	public int getId() {
		return id;
	}
}
