code: package formulae.cltloc.operators.binary;
  
  import com.google.common.base.Preconditions;
  
  import formulae.BinaryFormula;
  import formulae.cltloc.CLTLocFormula;
  import formulae.cltloc.visitor.CLTLocVisitor;
  
  public class CLTLocImplies extends CLTLocFormula implements BinaryFormula<CLTLocFormula> {
  
  	private final CLTLocFormula subformula1;
  	private final CLTLocFormula subformula2;
  	public final String operator = "->";
  	private final int hash;
  
  	private CLTLocImplies(CLTLocFormula subformula1, CLTLocFormula subformula2) {
  		super();
  		Preconditions.checkNotNull(subformula1, "The first subformula cannot be null");
  		Preconditions.checkNotNull(subformula2, "The second subformula cannot be null");
  		this.subformula1 = subformula1;
  		this.subformula2 = subformula2;
  		this.hash = this.hashComputation();
  	}
  
  	/**
  	 * {@inheritDoc}
  	 */
  	@Override
  	public CLTLocFormula getLeftChild() {
  		return subformula1;
  	}
  
  	/**
  	 * {@inheritDoc}
  	 */
  	@Override
  	public CLTLocFormula getRightChild() {
  		return subformula2;
  	}
  
  	/**
  	 * {@inheritDoc}
  	 */
  	@Override
  	public <T> T accept(CLTLocVisitor<T> t) {
  		return t.visit(this);
  	}
  
  	private int hashComputation() {
  		final int prime = 31;
  		int result = 1;
  		result = prime * result + ((operator == null) ? 0 : operator.hashCode());
  		result = prime * result + ((subformula1 == null) ? 0 : subformula1.hashCode());
  		result = prime * result + ((subformula2 == null) ? 0 : subformula2.hashCode());
  		return result;
  	}
  
  	/**
  	 * {@inheritDoc}
  	 */
  	@Override
  	public int hashCode() {
  		return hash;
  	}
  
  	/**
  	 * {@inheritDoc}
  	 */
  	@Override
  	public boolean equals(Object obj) {
  		if (this == obj)
  			return true;
  		if (obj == null)
  			return false;
  		if (getClass() != obj.getClass())
  			return false;
  		CLTLocImplies other = (CLTLocImplies) obj;
  		if (operator == null) {
  			if (other.operator != null)
  				return false;
  		} else if (!operator.equals(other.operator))
  			return false;
  		if (subformula1 == null) {
  			if (other.subformula1 != null)
  				return false;
  		} else if (!subformula1.equals(other.subformula1))
  			return false;
  		if (subformula2 == null) {
  			if (other.subformula2 != null)
  				return false;
  		} else if (!subformula2.equals(other.subformula2))
  			return false;
  		return true;
  	}
  
  	/**
  	 * {@inheritDoc}
  	 */
  	@Override
  	public String toString() {
  		return "(" + subformula1 + ") " + operator + " (" + subformula2 + ")";
  	}
  
  	public static CLTLocFormula create(CLTLocFormula subformula1, CLTLocFormula subformula2) {
  		Preconditions.checkNotNull(subformula1, "The first subformula cannot be null");
  		Preconditions.checkNotNull(subformula2, "The second subformula cannot be null");
  
  		if (subformula2.equals(CLTLocFormula.TRUE)) {
  			return CLTLocFormula.TRUE;
  		}
  		if (subformula2.equals(CLTLocFormula.FALSE)) {
  			return CLTLocFormula.getNeg(subformula1);
  		}
  		if (subformula1.equals(CLTLocFormula.TRUE)) {
  			return subformula2;
  		}
  		if (subformula1.equals(CLTLocFormula.FALSE)) {
  			return CLTLocFormula.TRUE;
  		}
  		return new CLTLocImplies(subformula1, subformula2);
  	}
  }
  