code: package formulae.cltloc;
  
  import java.util.Arrays;
  
  import com.google.common.base.Preconditions;
  
  import formulae.Formula;
  import formulae.cltloc.atoms.CLTLocAP;
  import formulae.cltloc.operators.binary.CLTLocConjunction;
  import formulae.cltloc.operators.binary.CLTLocDisjunction;
  import formulae.cltloc.operators.binary.CLTLocIff;
  import formulae.cltloc.operators.unary.CLTLocNegation;
  import formulae.cltloc.operators.unary.CLTLocYesterday;
  import formulae.cltloc.visitor.CLTLocVisitor;
  
  public abstract class CLTLocFormula extends Formula {
  
  	public static final CLTLocFormula TRUE = new CLTLocAP("True");
  	public static final CLTLocFormula FALSE = new CLTLocAP("False");
  
  	public CLTLocFormula() {
  		super();
  
  	}
  
  	public abstract <T> T accept(CLTLocVisitor<T> t);
  
  	
  	public static CLTLocFormula getAnd(CLTLocFormula f1, CLTLocFormula f2) {
  		Preconditions.checkNotNull(f1, "The first subformula cannot be null");
  		Preconditions.checkNotNull(f2, "The second subformula cannot be null");
  
  		if (f1.equals(CLTLocFormula.TRUE)) {
  			return f2;
  		}
  		if (f2.equals(CLTLocFormula.TRUE)) {
  			return f1;
  		}
  		return CLTLocConjunction.getCLTLocConjunction(f1, f2);
  	}
  	
  	public static CLTLocFormula getOr(CLTLocFormula f1, CLTLocFormula f2) {
  		Preconditions.checkNotNull(f1, "The first subformula cannot be null");
  		Preconditions.checkNotNull(f2, "The second subformula cannot be null");
  
  		if (f1.equals(CLTLocFormula.FALSE)) {
  			return f2;
  		}
  		if (f2.equals(CLTLocFormula.FALSE)) {
  			return f1;
  		}
  		return CLTLocDisjunction.getCLTLocDisjunction(f1, f2);
  	}
  
  	public static CLTLocFormula getIff(CLTLocFormula f1, CLTLocFormula f2) {
  		Preconditions.checkNotNull(f1, "The first subformula cannot be null");
  		Preconditions.checkNotNull(f2, "The second subformula cannot be null");
  
  		if (f1.equals(CLTLocFormula.TRUE)) {
  			return f2;
  		}
  		if (f2.equals(CLTLocFormula.TRUE)) {
  			return f1;
  		}
  		return new CLTLocIff(f1, f2);
  	}
  
  	public static CLTLocFormula getAnd(CLTLocFormula subformula1, CLTLocFormula... formulae) {
  		
  	
  		Preconditions.checkNotNull(subformula1, "No CLTLoc formula specified");
  		CLTLocFormula tmpsubformula1 = subformula1;
  		if(formulae==null){
  			return subformula1;
  		}
  		if(formulae.length==0){
  			return subformula1;
  		}
  		CLTLocFormula tmpsubformula2;
  				
  		if (formulae.length == 1) {
  			tmpsubformula2 = formulae[0];
  		} else {
  			tmpsubformula2 =getAnd(formulae[0], Arrays.copyOfRange(formulae, 1, formulae.length));		
  		}
  		return getAnd(tmpsubformula1, tmpsubformula2);
  	}
  
  	
  	public static CLTLocFormula getOr(CLTLocFormula subformula1, CLTLocFormula... formulae) {
  		Preconditions.checkNotNull(subformula1, "No CLTLoc formula specified");
  		CLTLocFormula tmpsubformula1 = subformula1;
  		if(formulae==null){
  			return subformula1;
  		}
  		if(formulae.length==0){
  			return subformula1;
  		}
  		CLTLocFormula tmpsubformula2;
  		if (formulae.length > 1) {
  			tmpsubformula2 = getOr(formulae[0], Arrays.copyOfRange(formulae, 1, formulae.length));
  		} else {
  			tmpsubformula2 = formulae[0];
  		}
  		return getOr(tmpsubformula1, tmpsubformula2);
  	}
  	
  	public static CLTLocFormula Y(CLTLocFormula subformula) {
  		Preconditions.checkNotNull(subformula, "No CLTLoc formula specified");
  		
  		return new CLTLocYesterday(subformula);
  	}
  	public static CLTLocFormula getNeg(CLTLocFormula f1) {
  		
  		if (f1 instanceof CLTLocNegation) {
  			return ((CLTLocNegation) f1).getChild();
  		} else {
  			return new CLTLocNegation(f1);
  		}
  	}
  
  }
  