code: package ta.visitors;
  
  import formulae.cltloc.CLTLocFormula;
  import formulae.cltloc.atoms.CLTLocClock;
  import formulae.cltloc.atoms.CLTLocSelector;
  import formulae.cltloc.atoms.Constant;
  import formulae.cltloc.operators.binary.CLTLocDisjunction;
  import formulae.cltloc.operators.unary.CLTLocNegation;
  import formulae.cltloc.relations.CLTLocRelation;
  import formulae.cltloc.relations.Relation;
  import ta.Clock;
  import ta.TA;
  import ta.state.EmptyInvariant;
  import ta.state.ExpInvariant;
  
  public class ReverseInvariantVisitor implements InvariantVisitor{
  
  	public CLTLocFormula visit(TA ta, EmptyInvariant emptyInvariant) {
  		return CLTLocFormula.TRUE;
  		
  	}
  	
  	public CLTLocFormula visit(TA ta, ExpInvariant inv) {
  		String variableName=inv.getId().getId();
  		String prefix = ta.getLocalClocks().contains(new Clock(variableName)) ? ta.getIdentifier() + "_" : "";
  		return (CLTLocFormula) CLTLocDisjunction.getCLTLocDisjunction(
  				CLTLocFormula.getAnd(
  						new CLTLocSelector(prefix + variableName + "_v"),
  						new CLTLocRelation(new CLTLocClock(prefix +variableName+ "_0"),
  								new Constant(inv.getExp().evaluate()), Relation.parse(inv.getOperator())
  								)),
  				CLTLocFormula.getAnd(
  						new CLTLocNegation(new CLTLocSelector(prefix + variableName + "_v")),
  						new CLTLocRelation(new CLTLocClock(prefix + variableName + "_1"),
  								new Constant(inv.getExp().evaluate()), Relation.parse(inv.getOperator()))));
  	}
  	
  }
  
  