/* Written by Denis Oddoux, LIAFA, France                                 *
 * Copyright (c) 2001  Denis Oddoux                                       *
 * Modified by Paul Gastin, LSV, France                                   *
 * Copyright (c) 2007  Paul Gastin                                        *
 * Ported by Carlos Bederian, FaMAF, Argentina                            *
 * Copyright (c) 2007  Carlos Bederian                                    *
 *                                                                        *
 * This program is free software; you can redistribute it and/or modify   *
 * it under the terms of the GNU General Public License as published by   *
 * the Free Software Foundation; either version 2 of the License, or      *
 * (at your option) any later version.                                    *
 *                                                                        *
 * 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*
 *                                                                        *
 * Based on the translation algorithm by Gastin and Oddoux,               *
 * presented at the 13th International Conference on Computer Aided       *
 * Verification, CAV 2001, Paris, France.                                 *
 * Proceedings - LNCS 2102, pp. 53-65                                     *
 *                                                                        */

package jltl2ba;

import java.util.Vector;
import java.io.PrintStream;

import jltl2ba.SimpleLTL;
import prism.PrismException;

public class Alternating {
	public int astate_count;
	public int atrans_count;
	private Vector<SimpleLTL> done;
	public Vector<ATrans> transition;
	public MyBitSet final_set;
	public APSet sym_table;

	public static class ATrans {
		public MyBitSet to; // nodes
		public MyBitSet pos; // syms
		public MyBitSet neg; // syms
		public ATrans nxt;

		public ATrans() {
			to = new MyBitSet();
			pos = new MyBitSet();
			neg = new MyBitSet();
			nxt = null;
		}

		public ATrans(MyBitSet _to, MyBitSet _pos, MyBitSet _neg) {
			to = (MyBitSet) _to.clone();
			pos = (MyBitSet) _pos.clone();
			neg = (MyBitSet) _neg.clone();
			nxt = null;
		}

		public ATrans clone() {
			ATrans rv = new ATrans(to, pos, neg);
			rv.nxt = nxt;
			return rv;
		}

		public ATrans merge(ATrans other) {
			if (other == null)
				return null;

			ATrans rv = this.clone();

			rv.to.or(other.to);
			rv.pos.or(other.pos);
			rv.neg.or(other.neg);

			if (rv.pos.intersects(rv.neg))
				rv = null;
			return rv;
		}
	}

	public static class AProd {
		public int astate;
		public ATrans prod;
		public ATrans trans;
		public AProd nxt;
		public AProd prv;

		public AProd() {
			;
		}
	}

	public Alternating(SimpleLTL formula, APSet apset) throws PrismException {
		astate_count = 0;
		atrans_count = 0;
		final_set = new MyBitSet();
		transition = new Vector<ATrans>();
		done = new Vector<SimpleLTL>();
		sym_table = apset;
		SimpleLTL p = formula.clone();
		// System.out.println("formula: " + p.toString());
		p = p.simplify();
		// System.out.println("after simplification: " + p.toString());

		done.add(null); // Reserve 0
		transition.add(null);
		transition.set(0, _boolean(p));
		// System.out.println("Alternating automaton before simplification");
		// print(System.out);
		simplifyAStates();
		// System.out.println("Alternating automaton after simplification");
		// print(System.out);
		done.clear();
	}

	/* computes the transitions to boolean nodes -> next & init */
	private ATrans _boolean(SimpleLTL p) {
		ATrans t1, t2, lft, rgt, result = null;

		switch (p.kind) {
		case TRUE:
			result = new ATrans();
			break;
		case FALSE:
			break;
		case AND:
			lft = _boolean(p.left);
			rgt = _boolean(p.right);
			for (t1 = lft; t1 != null; t1 = t1.nxt) {
				for (t2 = rgt; t2 != null; t2 = t2.nxt) {
					ATrans tmp = t1.merge(t2);
					if (tmp != null) {
						tmp.nxt = result;
						result = tmp;
					}
				}
			}
			break;
		case OR:
			lft = _boolean(p.left);
			for (t1 = lft; t1 != null; t1 = t1.nxt) {
				ATrans tmp = t1.clone();
				tmp.nxt = result;
				result = tmp;
			}
			rgt = _boolean(p.right);
			for (t1 = rgt; t1 != null; t1 = t1.nxt) {
				ATrans tmp = t1.clone();
				tmp.nxt = result;
				result = tmp;
			}
			break;
		default:
			buildAlternating(p);
			result = new ATrans();
			result.to.set(done.indexOf(p));
		}
		return result;
	}

	private int getSymID(String ap) {
		return sym_table.addAP(ap);
	}

	/* builds an alternating automaton for p */
	private ATrans buildAlternating(SimpleLTL p) {
		ATrans t1, t2, t = null;

		if (done.contains(p))
			return transition.get(done.indexOf(p));

		switch (p.kind) {

		case TRUE:
			t = new ATrans();
			break;

		case FALSE:
			break;

		case AP:
			t = new ATrans();
			t.pos.set(getSymID(p.ap));
			break;

		case NOT:
			t = new ATrans();
			t.neg.set(getSymID(p.left.ap)); // Should be in negated normal form
			break;

		case NEXT:
			t = _boolean(p.left);
			break;

		case UNTIL: /* p U q <-> q || (p && X (p U q)) */
			for (t2 = buildAlternating(p.right); t2 != null; t2 = t2.nxt) {
				ATrans tmp = t2.clone(); /* q */
				tmp.nxt = t;
				t = tmp;
			}
			for (t1 = buildAlternating(p.left); t1 != null; t1 = t1.nxt) {
				ATrans tmp = t1.clone(); /* p */
				tmp.to.set(done.size()); /* X (p U q) */
				tmp.nxt = t;
				t = tmp;
			}
			final_set.set(done.size());
			break;

		case RELEASE: /* p V q <-> (p && q) || (p && X (p V q)) */
			for (t1 = buildAlternating(p.right); t1 != null; t1 = t1.nxt) {
				ATrans tmp;

				for (t2 = buildAlternating(p.left); t2 != null; t2 = t2.nxt) {
					tmp = t1.merge(t2); /* p && q */
					if (tmp != null) {
						tmp.nxt = t;
						t = tmp;
					}
				}

				tmp = t1.clone(); /* p */
				tmp.to.set(done.size()); /* X (p V q) */
				tmp.nxt = t;
				t = tmp;
			}
			break;

		case AND:
			for (t1 = buildAlternating(p.left); t1 != null; t1 = t1.nxt) {
				for (t2 = buildAlternating(p.right); t2 != null; t2 = t2.nxt) {
					ATrans tmp = t1.merge(t2);
					if (tmp != null) {
						tmp.nxt = t;
						t = tmp;
					}
				}
			}
			break;

		case OR:
			for (t1 = buildAlternating(p.left); t1 != null; t1 = t1.nxt) {
				ATrans tmp = t1.clone();
				tmp.nxt = t;
				t = tmp;
			}
			for (t1 = buildAlternating(p.right); t1 != null; t1 = t1.nxt) {
				ATrans tmp = t1.clone();
				tmp.nxt = t;
				t = tmp;
			}
			break;

		default:
			break;
		}
		transition.add(t);
		done.add(p);
		return t;
	}

	private ATrans simplifyATrans(ATrans trans) {
		ATrans t, father = null;
		ATrans _trans = trans;
		for (t = _trans; t != null;) {
			ATrans t1;
			for (t1 = _trans; t1 != null; t1 = t1.nxt) {
				if ((t1 != t) && t.to.containsAll(t1.to)
						&& t.pos.containsAll(t1.pos)
						&& t.neg.containsAll(t1.neg))
					break;
			}
			if (t1 != null) {
				if (father != null)
					father.nxt = t.nxt;
				else
					_trans = t.nxt;
				if (father != null)
					t = father.nxt;
				else
					t = _trans;
				continue;
			}
			atrans_count++;
			father = t;
			t = t.nxt;
		}
		return _trans;
	}

	/* simplifies the alternating automaton */
	private void simplifyAStates() {
		ATrans t;
		int i;
		MyBitSet acc = new MyBitSet(); /* no state is accessible initially */

		for (t = transition.get(0); t != null; t = t.nxt, i = 0)
			acc.or(t.to); /* all initial states are accessible */

		for (i = transition.size() - 1; i > 0; i--) {
			if (!acc.get(i)) { // frees unaccessible states
				done.set(i, null);
				transition.set(i, null);
				continue;
			}
			astate_count++;
			transition.set(i, simplifyATrans(transition.get(i)));
			for (t = transition.get(i); t != null; t = t.nxt)
				acc.or(t.to);
		}
	}

	/* dumps the alternating automaton */
	public void print(PrintStream out) {
		int i;
		ATrans t;

		out.print("init :\n");
		for (t = transition.get(0); t != null; t = t.nxt) {
			t.to.print(out);
			out.println();
		}

		for (i = done.size() - 1; i > 0; i--) {
			if (done.get(i) == null)
				continue;
			out.format("state %d : ", i);
			out.print(done.get(i).toString());
			out.println();
			for (t = transition.get(i); t != null; t = t.nxt) {
				if (t.pos.isEmpty() && t.neg.isEmpty())
					out.print("1");
				t.pos.print(out, sym_table, true);
				if (!t.pos.isEmpty() && !t.neg.isEmpty())
					out.print(" & ");
				t.neg.print(out, sym_table, false);
				out.print(" -> ");
				t.to.print(out);
				out.println();
			}
		}
	}
}