Now using the TranslationVisitor, comparing with old version

de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java

@@ -31,6 +31,7 @@ import org.eventb.core.ISCExtendsContext;
 import org.eventb.core.ISCInternalContext;
 import org.eventb.core.ast.FormulaFactory;
 import org.eventb.core.ast.ITypeEnvironment;
+import org.eventb.core.ast.Predicate;
 import org.eventb.core.seqprover.IConfidence;
 import org.rodinp.core.IAttributeType;
 import org.rodinp.core.IInternalElement;
@@ -61,6 +62,7 @@ import de.prob.core.translator.pragmas.UnitPragma;
 import de.prob.eventb.translator.internal.EProofStatus;
 import de.prob.eventb.translator.internal.ProofObligation;
 import de.prob.eventb.translator.internal.SequentSource;
+import de.prob.eventb.translator.internal.TranslationVisitor;
 
 public final class ContextTranslator extends AbstractComponentTranslator {
 
@@ -382,8 +384,10 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			if (element.isTheorem() == theorems) {
 				final PredicateVisitor visitor = new PredicateVisitor(
 						new LinkedList<String>());
-				element.getPredicate(ff, te).accept(visitor);
+				final Predicate p = element.getPredicate(ff, te);
+				p.accept(visitor);
 				final PPredicate predicate = visitor.getPredicate();
+				TranslationVisitor.checkNewImplementation(p, predicate);
 				list.add(predicate);
 				labelMapping.put(predicate, element);
 				proofspragmas.add(new ClassifiedPragma("discharged", predicate,

de.prob.core/src/de/prob/eventb/translator/internal/ModelTranslator.java

@@ -430,6 +430,8 @@ public class ModelTranslator extends AbstractComponentTranslator {
 			// + guardPredicate);
 			guardPredicate.accept(visitor);
 			final PPredicate predicate = visitor.getPredicate();
+			TranslationVisitor
+					.checkNewImplementation(guardPredicate, predicate);
 			if (guard.isTheorem()) {
 				theoremsList.add(predicate);
 			} else {
@@ -533,8 +535,10 @@ public class ModelTranslator extends AbstractComponentTranslator {
 			if (!isDefinedInAbstraction(evPredicate)) {
 				final PredicateVisitor visitor = new PredicateVisitor(
 						new LinkedList<String>());
-				evPredicate.getPredicate(ff, te).accept(visitor);
+				Predicate p = evPredicate.getPredicate(ff, te);
+				p.accept(visitor);
 				final PPredicate predicate = visitor.getPredicate();
+				TranslationVisitor.checkNewImplementation(p, predicate);
 				list.add(predicate);
 				labelMapping.put(predicate, evPredicate);
 			}

de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java

@@ -328,8 +328,8 @@ public class TranslationVisitor implements ISimpleVisitor {
 	}
 
 	public void visitBinaryPredicate(final BinaryPredicate predicate) {
-		final PPredicate right = getPredicate(predicate.getLeft());
-		final PPredicate left = getPredicate(predicate.getRight());
+		final PPredicate left = getPredicate(predicate.getLeft());
+		final PPredicate right = getPredicate(predicate.getRight());
 		final PPredicate result;
 		switch (predicate.getTag()) {
 		case Formula.LIMP:
@@ -676,4 +676,39 @@ public class TranslationVisitor implements ISimpleVisitor {
 
 		}
 	}
+
+	public PPredicate getPredicate() {
+		assertExactStacksize(predicates);
+		return predicates.pop();
+	}
+
+	public PExpression getExpression() {
+		assertExactStacksize(expressions);
+		return expressions.pop();
+	}
+
+	public PSubstitution getSubstitution() {
+		assertExactStacksize(substitutions);
+		return substitutions.pop();
+	}
+
+	private void assertExactStacksize(LookupStack<?> stack) {
+		if (stack.size() != 1) {
+			throw new AssertionError(
+					"Exactly one element on the stack expected, but were "
+							+ predicates.size());
+
+		}
+	}
+
+	public static void checkNewImplementation(Predicate p, PPredicate predicate) {
+		TranslationVisitor visitor = new TranslationVisitor();
+		p.accept(visitor);
+		final String expected = predicate.toString();
+		final String actual = visitor.getPredicate().toString();
+		if (!expected.equals(actual)) {
+			throw new AssertionError("Expected:\n" + expected + "\n but was:\n"
+					+ actual);
+		}
+	}
 }