Merge branch 'develop' of github.com:bendisposto/prob into develop

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

@@ -53,6 +53,7 @@ import de.be4.classicalb.core.parser.node.PSet;
 import de.be4.classicalb.core.parser.node.TIdentifierLiteral;
 import de.hhu.stups.sablecc.patch.SourcePosition;
 import de.prob.core.translator.TranslationFailedException;
+import de.prob.eventb.translator.internal.EProofStatus;
 import de.prob.eventb.translator.internal.ProofObligation;
 import de.prob.eventb.translator.internal.SequentSource;
 
@@ -69,7 +70,6 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			throws TranslationFailedException {
 		ContextTranslator contextTranslator = new ContextTranslator(context);
 		try {
-			(new TheoryTranslator()).translate();
 			contextTranslator.translate();
 		} catch (RodinDBException e) {
 			final String message = "A Rodin exception occured during translation process. Possible cause: building aborted or still in progress. Please wait until building has finished before starting ProB. If this does not help, perform a clean and start ProB after building has finished. Original Exception: ";
@@ -136,8 +136,12 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 			final int confidence = status.getConfidence();
 			boolean broken = status.isBroken();
 
-			boolean discharged = !broken
-					&& confidence == IConfidence.DISCHARGED_MAX;
+			EProofStatus pstatus = EProofStatus.UNPROVEN;
+
+			if (!broken && confidence == IConfidence.REVIEWED_MAX)
+				pstatus = EProofStatus.REVIEWED;
+			if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+				pstatus = EProofStatus.PROVEN;
 
 			IPOSequent sequent = status.getPOSequent();
 			IPOSource[] sources = sequent.getSources();
@@ -161,7 +165,7 @@ public final class ContextTranslator extends AbstractComponentTranslator {
 						.getLabel()));
 
 			}
-			proofs.add(new ProofObligation(origin, s, name, discharged));
+			proofs.add(new ProofObligation(origin, s, name, pstatus));
 		}
 
 	}

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

+package de.prob.eventb.translator.internal;
+
+public enum EProofStatus {
+	UNPROVEN("false"), PROVEN("true"), REVIEWED("reviewed");
+	private final String text;
+
+	private EProofStatus(String text) {
+		this.text = text;
+	}
+
+	@Override
+	public String toString() {
+		return text;
+	}
+}

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

@@ -104,7 +104,7 @@ public abstract class EventBTranslator implements ITranslator {
 			}
 			pout.closeList();
 
-			pout.printAtom(Boolean.toString(proof.discharged));
+			pout.printAtom(proof.discharged.toString());
 			pout.closeTerm();
 		}
 

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

@@ -177,8 +177,12 @@ public class ModelTranslator extends AbstractComponentTranslator {
 			final int confidence = status.getConfidence();
 			boolean broken = status.isBroken();
 
-			boolean discharged = !broken
-					&& confidence == IConfidence.DISCHARGED_MAX;
+			EProofStatus pstatus = EProofStatus.UNPROVEN;
+
+			if (!broken && (confidence > IConfidence.PENDING && confidence <= IConfidence.REVIEWED_MAX))
+				pstatus = EProofStatus.REVIEWED;
+			if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+				pstatus = EProofStatus.PROVEN;
 
 			IPOSequent sequent = status.getPOSequent();
 			IPOSource[] sources = sequent.getSources();
@@ -202,7 +206,7 @@ public class ModelTranslator extends AbstractComponentTranslator {
 				s.add(new SequentSource(type, le.getLabel()));
 
 			}
-			proofs.add(new ProofObligation(origin, s, name, discharged));
+			proofs.add(new ProofObligation(origin, s, name, pstatus));
 		}
 
 		if (!bugs.isEmpty()) {

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

@@ -9,14 +9,14 @@ public class ProofObligation {
 	public final IEventBRoot origin;
 	public final ArrayList<SequentSource> sources;
 	public final String kind;
-	public final boolean discharged;
+	public final EProofStatus discharged;
 
 	public ProofObligation(IEventBRoot origin, ArrayList<SequentSource> s,
-			String name, boolean discharged) {
+			String name, EProofStatus pstatus) {
 		this.origin = origin;
 		this.sources = s;
 		this.kind = name;
-		this.discharged = discharged;
+		this.discharged = pstatus;
 	}
 
 }