/*
 * 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
 *
 * 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 prism.PrismException;
import java.util.Iterator;
import java.util.BitSet;

import jltl2ba.APElement;
import jltl2ba.APSet;

/** @file 
 * Provides class DBA2DRA, which can convert a 
 * deterministic B�chi automaton to a deterministic Rabin
 * automaton.
 */

/**
 * Provides conversion from deterministic B�chi to 
 * deterministic Rabin.
 */
public class DBA2DRA {
	/**
	 * Convert a deterministic B�chi automaton
	 * (a nondeterministic B�chi automaton NBA, where every transition
	 * has at most one target state) to an equivalent deterministic 
	 * Rabin automaton.
	 * <p>
	 * This involves generation of the appropriate acceptance condition
	 * and making sure that the transition function is complete.
	 * </p>
	 * <p>
	 * The DBA can also be complemented on the fly 
	 * (by modifying the acceptance condition of the DRA). The resulting DRA can then be
	 * regarded as a Streett automaton of the original DBA.
	 * @param nba the NBA, the transitions have to be deterministic!
	 * @param complement complement the DBA?
	 * @return a shared_ptr to the created DRA
	 */
	public static DRA dba2dra(NBA nba, boolean complement) throws PrismException {
		APSet ap_set = nba.getAPSet();
		DRA dra = new DRA(ap_set);

		dra.acceptance().newAcceptancePair();

		for (int i = 0; i < nba.size(); i++) {
			dra.newState();

			if (complement) {
				// Final states -> U_0, all states -> L_0
				if (nba.get(i).isFinal()) {
					dra.acceptance().stateIn_U(0, i, true);
				}
				dra.acceptance().stateIn_L(0, i, true);
			} else {
				// Final states -> L_0, U_0 is empty
				if (nba.get(i).isFinal()) {
					dra.acceptance().stateIn_L(0, i, true);
				}
			}
		}

		if (nba.getStartState() != null) {
			dra.setStartState(dra.get(nba.getStartState().getName()));
		}

		DA_State sink_state = null;

		for (int i = 0; i < nba.size();	i++) {
			NBA_State nba_state = nba.get(i);
			DA_State dra_from = dra.get(i);

			for (Iterator<APElement> it = ap_set.elementIterator(); it.hasNext(); ) {
				APElement label = it.next(); 
				BitSet to = nba_state.getEdge(label);

				int to_cardinality = 0;
				if (to != null) {
					to_cardinality = to.cardinality();
				}

				DA_State dra_to = null;
				if (to == null || to_cardinality == 0) {
					// empty to -> go to sink state
					if (sink_state == null) {
						// we have to create the sink
						sink_state = dra.newState();

						// if we complement, we have to add the sink to
						// L_0 
						if (complement) {
							sink_state.acceptance().addTo_L(0);
						}	    
					}
					dra_to = sink_state;
				} else if (to_cardinality == 1) {
					int to_index = to.nextSetBit(0);

					//	  std::cerr << "to: " << to_index << std::endl;

					dra_to = dra.get(to_index);
				} else {
					// to_cardinality>1 !
					throw new PrismException("NBA is no DBA!");
				}

				dra_from.edges().put(label, dra_to);
			}
		}

		if (sink_state != null) {
			// there is a sink state
			// make true-loop from sink state to itself
			for (Iterator<APElement> it = ap_set.elementIterator(); it.hasNext(); ) {
				sink_state.edges().put(it.next(), sink_state);
			}
		}
		return dra;
	}
}