prism-accumulation/prism/src/jltl2dstar/UnionState.java

/*
 * 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;

/** A state representing a union state from two DA. */
public class UnionState implements Comparable<UnionState>,NBA2DAState {
	
	public static class Result implements NBA2DAResult<UnionState> {
		private UnionState state;
		public Result(UnionState state_) {
			state = state_;
		}
		public UnionState getState() {
			return state;
		}
	}
	
	/** Index of the state from the first automaton */
	protected int da_state_1;
	/** Index of the state from the second automaton */
	protected int da_state_2;
	/** A shared_ptr with the acceptance signature of this state */
	RabinSignature signature;
	/** A shared_ptr to a string containing a detailed description of this state */
	String description;

	/** Constructor.
	 * @param da_state_1_ index of the state in the first automaton
	 * @param da_state_2_ index of the state in the second automaton
	 * @param acceptance_calculator UnionAcceptanceCalculator
	 */
	public UnionState(int da_state_1_, int da_state_2_,	UnionAcceptanceCalculator acceptance_calculator) {
		da_state_1 = da_state_1_;
		da_state_2 = da_state_2_;
		signature = acceptance_calculator.calculateAcceptance(da_state_1, da_state_2);
		description = "";
	}

	public int compareTo(UnionState other) {
		if (da_state_1 != other.da_state_1)
			return da_state_1 - other.da_state_1;
		else return da_state_2 - other.da_state_2;
	}
	
	public boolean equals(UnionState other) {
		return ((da_state_1 == other.da_state_1) && (da_state_2 == other.da_state_2));
	}
	
	public boolean equals(Object o) {
		return (o instanceof UnionState && this.equals((UnionState) o));
	}
	
	/** Copy acceptance signature for this state
	 * @param acceptance (<b>out</b>) AcceptanceForState for the state in the result automaton 
	 */
	public void generateAcceptance(AcceptanceForState acceptance) {
		acceptance.setSignature(signature);
	}

	/** Copy acceptance signature for this state
	 * @param acceptance (<b>out</b>) acceptance signature for the state in the result automaton 
	 */
	// void generateAcceptance(da_signature_t& acceptance) const {
//		acceptance=*signature;
//	}

	/** Return the acceptance acceptance signature for this state
	 * @return the acceptance signature for this state
	 */
	public RabinSignature generateAcceptance() {
		return signature;
	}

	/**
	 * Set the detailed description for this state
	 * @param description_ the description
	 */
	public void setDescription(String description_) {
		description = description_;
	}

	/** Generate a simple representation of this state 
	 * @return a string with the representation
	 */
	public String toString() {
		return "(" + da_state_1 + "," + da_state_1 + ")";
	}
	
    /** Return the detailed description 
     * @return the detailed description
     */
    public String toHTML() {
        return description;
    }

	/** Calculates the hash for the union state. 
	 * @param hash the HashFunction functor used for the calculation
	 */
	// template <class HashFunction>
	// void hashCode(HashFunction& hash) {
	// 		hash.hash(da_state_1);
	// 		hash.hash(da_state_2);
		// we don't have to consider the signature as there is a 
		// 1-on-1 mapping between <da_state_1, da_state_2> -> signature
	// }
    public int hashCode() {
    	return da_state_1 + da_state_2 * 31;
    }

}