/*
 * This file is part of a Java port of the program ltl2dstar
 * (http://www.ltl2dstar.de/) for PRISM (http://www.prismmodelchecker.org/)
 * Copyright (C) 2005-2007 Joachim Klein <j.klein@ltl2dstar.de>
 * Copyright (c) 2007 Carlos Bederian
 * Copyright (c) 2011- Hongyang Qu
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License version 2 as 
 *  published by the Free Software Foundation.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package jltl2dstar;

import java.io.PrintStream;
import java.util.*;

import jltl2ba.APElement;
import jltl2ba.APSet;
import prism.PrismException;
import prism.PrismNotSupportedException;

public class DA {

	/**
	 * A class representing a deterministic omega automaton.
	 * <p>
	 * The template parameters:<br>
	 * Label: the type of the labeling on the edges<br>
	 * EdgeContainer: a template (taking the DA_State class as parameter)
	 *                providing an EdgeContainer for holding the edges in 
	 *                the states.<br>
	 * </p>
	 * <p>
	 *  Each state is identified by an index.<br>
	 *  There exists one start state.<br>
	 *  There exists an acceptance condition <br>
	 *  The DA is <i>compact</i>, if there are no holes in the indexes of the
	 *  states and the acceptance condition is compact as well.
	 * </p>
	 */

	/** The storage index for the states. */
	private Vector<DA_State> _index;

	/** The underlying APset. */
	private APSet _ap_set;

	/** The start state. */
	private DA_State _start_state;

	/** Flag to mark that the automaton is compact. */
	private boolean _is_compact;

	/** A comment */
	private String _comment;

	/** The acceptance condition for this automaton. */
	private RabinAcceptance _acceptance;

	/**
	 * Constructor.
	 * @param ap_set the underlying APSet.
	 */
	public DA(APSet ap_set)
	{
		_ap_set = ap_set; 
		_start_state = null; 
		_is_compact = true;
		_comment = "";
		_index = new Vector<DA_State>();
		_acceptance = new RabinAcceptance();
	}
	
	public static DA newInstance(APSet ap_set) {
		return new DA(ap_set);
	}

	/**
	 * Create a new state.
	 * @return a pointer to the new state.
	 */
	public DA_State newState()
	{
		DA_State state = new DA_State(this);
		int name = _index.size();
		state.setName(name);
		_index.add(state);
		_acceptance.addState(name);
		return state;
	}

	/** Make this automaton into an never accepting automaton */
	public void constructEmpty() {
		DA_State n = newState();
		setStartState(n);

		for (Iterator<APElement> it = getAPSet().elementIterator(); it.hasNext(); ){
			n.edges().put(it.next(), n);
		}
	}

	/** The number of states in the automaton.*/
	public int size()
	{
		return _index.size();
	}

	/** The type of an iterator over the states */
	public Iterator<DA_State> iterator()
	{
		return _index.iterator();
	}

	/**
	 * Array index operator, get the state with index i.
	 */
	public DA_State get(int i)
	{
		return _index.get(i);
	}

	/**
	 * Get the size of the underlying APSet.
	 */
	public int getAPSize()
	{
		return _ap_set.size();
	}

	/**
	 * Get a const reference to the underlying APSet.
	 */
	public APSet getAPSet()
	{
		return _ap_set;
	}

	/**
	 * Switch the APSet to another with the same number of APs.
	 */
	public void switchAPSet(APSet new_apset) throws PrismException
	{
		if (new_apset.size() != _ap_set.size()) {
			throw new PrismException("New APSet has to have the same size as the old APSet!");
		}
		_ap_set=new_apset;
	}

	/**
	 * Get the index for a state.
	 */
	public int getIndexForState(DA_State state)
	{
		return _index.indexOf(state);
	}

	/** Set the start state. */
	public void setStartState(DA_State state)
	{
		_start_state=state;
	}

	/**
	 * Get the start state.
	 * @return the start state, or NULL if it wasn't set.
	 */
	public DA_State getStartState()
	{
		return _start_state;
	}

	/** Checks if the automaton is compact. */
	public boolean isCompact()
	{
		return _is_compact && acceptance().isCompact();
	}

	/** Set a comment for the automaton. */
	public void setComment(String comment)
	{
		_comment=comment;
	}

	/** Get the comment for the automaton. */
	public String getComment()
	{
		return _comment;
	}

	/** Return reference to the acceptance condition for this automaton.
	 * @return reference to the acceptance condition
	 */
	public RabinAcceptance acceptance()
	{
		return _acceptance;
	}

	/**
	 * Reorder states and acceptance conditions so that
	 * the automaton becomes compact.
	 */
	public void makeCompact() throws PrismException {
		acceptance().makeCompact();

		if (!_is_compact) {
			int i, j;
			boolean moved = false;

			Vector<Integer> mapping = new Vector<Integer>(_index.size());
			for (i = 0, j = 0; i < _index.size(); i++) {
				if (_index.get(i) != null) {
					mapping.set(i, new Integer(j));
					if (j != i) {
						_index.set(j, _index.get(i));
						_index.set(i, null);
						moved = true;
					}
					j++;
				}
				else {
					while (_index.get(i) == null && i < _index.size()) {
						i++;
					}
					if (i < _index.size())
						break;
				}
			}

			if (moved) {
				_index.setSize(j);
				acceptance().moveStates(mapping);
			}
			_is_compact=true;
		}
	}


	/**
	 * Print the DA in v2 format to the output stream.
	 * This functions expects that the DA is compact.
	 * @param da_type a string specifying the type of automaton ("DRA", "DSA").
	 * @param out the output stream 
	 */
	public void	print(String da_type, PrintStream out) throws PrismException {
		// Ensure that this DA is compact...
		if (!this.isCompact()) {
			throw new PrismException("DA is not compact!");
		}

		if (this.getStartState() == null) {
			// No start state! 
			throw new PrismException("No start state in DA!");
		}

		out.println(da_type+" v2 explicit");
		
		if (_comment != "") {
			out.println("Comment: \"" + _comment + "\"");
		}
		out.println("States: " + _index.size());
		_acceptance.outputAcceptanceHeader(out);

		int start_state = this.getStartState().getName();
		out.println("Start: " + start_state);

		// Enumerate APSet
		out.print("AP: " + getAPSize());
		for (int ap_i = 0; ap_i < getAPSize(); ap_i++) {
			out.print(" \"" + getAPSet().getAP(ap_i) + "\"");
		}
		out.println();

		out.println("---");

		for (int i_state = 0; i_state < _index.size(); i_state++) {
			DA_State cur_state = _index.get(i_state);
			out.print("State: " + i_state);
			if (cur_state.hasDescription()) {
				out.print(" \"" + cur_state.getDescription() + "\"");
			}
			out.println();

			_acceptance.outputAcceptanceForState(out, i_state);
			
			Iterator<APElement> it = _ap_set.elementIterator();
			while (it.hasNext()) {
				APElement e = it.next();
				DA_State to = cur_state.edges().get(e);
				out.println(to.getName());
			}
		}
	}

	/**
	 * Print the DA in HOA format to the output stream.
	 * This functions expects that the DA is compact.
	 * @param da_type a string specifying the type of automaton ("DRA", "DSA").
	 * @param out the output stream
	 */
	public void printHOA(String da_type, PrintStream out) throws PrismException {
		if (!da_type.equals("DRA")) throw new PrismNotSupportedException("HOA printing for "+da_type+" currently not supported");

		out.println("HOA: v1");
		out.println("States: "+size());
		_ap_set.print_hoa(out);
		out.println("Start: "+getStartState().getName());
		_acceptance.outputAcceptanceHeaderHOA(out);
		out.println("properties: trans-labels explicit-labels state-acc no-univ-branch deterministic");
		out.println("--BODY--");
		for (DA_State state : _index) {
			out.print("State: "+state.getName()+ " ");  // id
			_acceptance.outputAcceptanceForStateHOA(out, state.getName());

			for (Map.Entry<APElement, DA_State> edge : state.edges().entrySet()) {
				APElement label = edge.getKey();
				String labelString = "["+label.toStringHOA(_ap_set.size())+"]";
				DA_State to = edge.getValue();
				out.print(labelString);
				out.print(" ");
				out.println(to);
			}
		}
		out.println("--END--");
	}

	/**
	 * Print the DA in dot format to the output stream.
	 * This functions expects that the DA is compact.
	 * @param da_type a string specifying the type of automaton ("DRA", "DSA").
	 * @param out the output stream 
	 */
	public void	printDot(String da_type, PrintStream out) throws PrismException {
		// Ensure that this DA is compact...
		if (!this.isCompact()) {
			throw new PrismException("DA is not compact!");
		}

		if (this.getStartState() == null) {
			// No start state! 
			throw new PrismException("No start state in DA!");
		}

		int start_state = this.getStartState().getName();

		out.println("digraph model {");
		for (int i_state = 0; i_state < _index.size(); i_state++) {
			if(i_state == start_state)
				out.println("	" + i_state + " [label=\"" + i_state + "\", shape=ellipse]");
			else {
				boolean isAcceptance = false;
				for (int ap_i = 0; ap_i < _acceptance.size(); ap_i++) {
					if(_acceptance.isStateInAcceptance_L(ap_i, i_state)) {
						out.println("	" + i_state + " [label=\"" + i_state + "\", shape=doublecircle]");
						isAcceptance = true;
						break;
					} else if(_acceptance.isStateInAcceptance_U(ap_i, i_state)) {
						out.println("	" + i_state + " [label=\"" + i_state + "\", shape=box]");
						isAcceptance = true;
						break;
					}
				}
				if(!isAcceptance)
					out.println("	" + i_state + " [label=\"" + i_state + "\", shape=circle]");
			}
		}
		for (int i_state = 0; i_state < _index.size(); i_state++) {
			DA_State cur_state = _index.get(i_state);
			for (Map.Entry<APElement, DA_State> transition : cur_state.edges().entrySet()) {
				out.println("	" + i_state + " -> " + transition.getValue().getName() + 
						" [label=\"" + transition.getKey().toString(_ap_set, true) + "\"]");
			}
		}
		out.println("}");
		
	}
}