code: package formulae.mitli.converters;
  
  import java.io.PrintStream;
  import java.util.HashMap;
  import java.util.Map;
  import java.util.Set;
  
  import com.google.common.base.Preconditions;
  import com.google.common.collect.BiMap;
  
  import formulae.cltloc.CLTLocFormula;
  import formulae.cltloc.atoms.CLTLocClock;
  import formulae.cltloc.atoms.Constant;
  import formulae.cltloc.operators.unary.CLTLocGlobally;
  import formulae.cltloc.operators.unary.CLTLocNext;
  import formulae.cltloc.relations.CLTLocEQRelation;
  import formulae.cltloc.relations.CLTLocGEQRelation;
  import formulae.cltloc.relations.CLTLocGERelation;
  import formulae.cltloc.visitor.CLTLoc2StringVisitor;
  import formulae.cltloc.visitor.GetClocksVisitor;
  import formulae.mitli.MITLIFormula;
  import formulae.mitli.visitors.MITLI2CLTLocVisitor;
  import formulae.mitli.visitors.SubformulaeVisitor;
  
  public class MITLI2CLTLoc {
  
  	private final MITLI2CLTLocVisitor visitor;
  	private final MITLIFormula formula;
  
  	private boolean converted = false;
  	private final Map<MITLIFormula, CLTLocFormula> generatedFormulaMap;
  	private final Map<MITLIFormula, CLTLocFormula> clockcontraintFormulaMap;
  
  	private final Map<MITLIFormula, MITLIFormula> parentRelation;
  
  	public MITLI2CLTLoc(MITLIFormula formula) {
  		this.formula = formula;
  		this.visitor = new MITLI2CLTLocVisitor(formula);
  		this.generatedFormulaMap = new HashMap<>();
  		this.clockcontraintFormulaMap = new HashMap<>();
  		this.parentRelation = new HashMap<>();
  
  	}
  
  	private void populateParentRelation(MITLIFormula f) {
  		Set<MITLIFormula> chidren = f.getChildren();
  		chidren.forEach(c -> parentRelation.put(c, f));
  
  		chidren.forEach(c -> this.populateParentRelation(c));
  
  	}
  
  	public CLTLocFormula apply() {
  
  		this.populateParentRelation(formula);
  
  		
  		//CLTLocFormula init = 
  		//	  (formula instanceof MITLINegation )? 
  		//				  CLTLocFormula.getNeg(MITLI2CLTLocVisitor.first.apply(visitor.formulaIdMap.get(formula)))
  		CLTLocFormula init = MITLI2CLTLocVisitor.first.apply(visitor.formulaIdMap.get(formula));
  		// init  =CLTLocFormula.TRUE;
  				
  
  		CLTLocFormula conjunction = CLTLocFormula.TRUE;
  		for (MITLIFormula f : formula.accept(new SubformulaeVisitor())) {
  
  			CLTLocFormula f1 = visitor.getckTheta(f, parentRelation);
  			CLTLocFormula f2 = f.accept(visitor);
  			
  			CLTLocFormula formula = MITLI2CLTLocVisitor.AND.apply(f1, f2);
  			this.generatedFormulaMap.put(f, f1);
  			this.clockcontraintFormulaMap.put(f, f2);
  			
  			
  			
  			conjunction = CLTLocFormula.getAnd( conjunction, formula);
  		
  		}
  
  		
  		CLTLocFormula nowConstraint=
  				CLTLocFormula.getAnd(
  						new CLTLocEQRelation(new CLTLocClock("Now"), new Constant(0)),
  						new CLTLocNext(CLTLocGlobally.create(new CLTLocGERelation(new CLTLocClock("Now"), new Constant(0))))
  						);
  		
  
  		Set<CLTLocClock> clocks = conjunction.accept(new GetClocksVisitor());
  		
  		CLTLocFormula clockConstraint=CLTLocFormula.TRUE;
  		
  		for(CLTLocClock clock:  clocks){
  			clockConstraint=CLTLocFormula.getAnd(clockConstraint, new CLTLocGEQRelation(clock, new Constant(0)));
  		}
  				
  				
  		CLTLocFormula formula = CLTLocFormula.getAnd( nowConstraint, clockConstraint, init, conjunction);
  
  		converted = true;
  		return formula;
  
  	}
  
  	public CLTLocFormula getTheta(MITLIFormula f) {
  
  		Preconditions.checkArgument(converted, "Run the converter before getting the expression");
  		Preconditions.checkArgument(this.clockcontraintFormulaMap.containsKey(f),
  				"The formula must be a subformula of the original formula");
  		return this.clockcontraintFormulaMap.get(f);
  	}
  
  	public BiMap<Integer, MITLIFormula> getVocabulary() {
  		return this.visitor.formulaIdMap.inverse();
  	}
  
  	public void printFancy(PrintStream fancyprint) {
  		generatedFormulaMap.entrySet().forEach(e -> {
  
  			fancyprint.println("---");
  			fancyprint.println("Subformula: " + this.visitor.formulaIdMap.get(e.getKey()) + "\t" + e.getKey());
  			fancyprint.println("---Clock constraint");
  			fancyprint.println(e.getValue().accept(new CLTLoc2StringVisitor()).getKey());
  			fancyprint.println("---Subformula");
  			fancyprint.println(
  					clockcontraintFormulaMap.get(e.getKey()).accept(new CLTLoc2StringVisitor()).getKey() + "\n");
  
  		}
  
  		);
  	}
  
  }
  