From fd435a879cda7079633b794fd8227a62e1b4253e Mon Sep 17 00:00:00 2001
From: Jens Bendisposto <jens@bendisposto.de>
Date: Wed, 5 Feb 2014 18:40:39 +0100
Subject: [PATCH] and the same for contexts
---
.../eventb/translator/ContextTranslator.java | 68 +++++++++++--------
1 file changed, 40 insertions(+), 28 deletions(-)
diff --git a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
index eff85650..8be07b5b 100644
--- a/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
+++ b/de.prob.core/src/de/prob/eventb/translator/ContextTranslator.java
@@ -13,6 +13,7 @@ import java.util.LinkedList;
import java.util.List;
import java.util.Map;
+import org.apache.commons.lang.StringUtils;
import org.eclipse.core.runtime.Assert;
import org.eventb.core.IContextRoot;
import org.eventb.core.IEventBRoot;
@@ -61,6 +62,7 @@ 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;
+import de.prob.logging.Logger;
public final class ContextTranslator extends AbstractComponentTranslator {
@@ -180,47 +182,57 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
private void collectProofInfo(IEventBRoot origin) throws RodinDBException {
-
- IPSRoot proofStatus = origin.getPSRoot();
- IPSStatus[] statuses = proofStatus.getStatuses();
-
List<String> bugs = new LinkedList<String>();
- for (IPSStatus status : statuses) {
- final int confidence = status.getConfidence();
- boolean broken = status.isBroken();
+ try {
+ IPSRoot proofStatus = origin.getPSRoot();
+ IPSStatus[] statuses = proofStatus.getStatuses();
- EProofStatus pstatus = EProofStatus.UNPROVEN;
+ for (IPSStatus status : statuses) {
+ final int confidence = status.getConfidence();
+ boolean broken = status.isBroken();
- if (!broken && confidence == IConfidence.REVIEWED_MAX)
- pstatus = EProofStatus.REVIEWED;
- if (!broken && confidence == IConfidence.DISCHARGED_MAX)
- pstatus = EProofStatus.PROVEN;
+ EProofStatus pstatus = EProofStatus.UNPROVEN;
- IPOSequent sequent = status.getPOSequent();
- IPOSource[] sources = sequent.getSources();
+ if (!broken && confidence == IConfidence.REVIEWED_MAX)
+ pstatus = EProofStatus.REVIEWED;
+ if (!broken && confidence == IConfidence.DISCHARGED_MAX)
+ pstatus = EProofStatus.PROVEN;
- String name = sequent.getDescription();
+ IPOSequent sequent = status.getPOSequent();
+ IPOSource[] sources = sequent.getSources();
- ArrayList<SequentSource> s = new ArrayList<SequentSource>(
- sources.length);
- for (IPOSource source : sources) {
+ String name = sequent.getDescription();
- IRodinElement srcElement = source.getSource();
- if (!srcElement.exists()
- || !(srcElement instanceof ILabeledElement)) {
- bugs.add(status.getElementName());
- break;
- }
+ ArrayList<SequentSource> s = new ArrayList<SequentSource>(
+ sources.length);
+ for (IPOSource source : sources) {
+
+ IRodinElement srcElement = source.getSource();
+ if (!srcElement.exists()
+ || !(srcElement instanceof ILabeledElement)) {
+ bugs.add(status.getElementName());
+ break;
+ }
- ILabeledElement le = (ILabeledElement) srcElement;
+ ILabeledElement le = (ILabeledElement) srcElement;
- s.add(new SequentSource(srcElement.getElementType(), le
- .getLabel()));
+ s.add(new SequentSource(srcElement.getElementType(), le
+ .getLabel()));
+ }
+ addProof(new ProofObligation(origin, s, name, pstatus));
}
- addProof(new ProofObligation(origin, s, name, pstatus));
+ } catch (RodinDBException e) {
+ bugs.add(e.getLocalizedMessage());
}
+
+ if (!bugs.isEmpty()) {
+ String message = "Translation incomplete due to a Bug in Rodin. This does not affect correctness of the Animation/Model Checking but can decrease its performance. Skipped discharged information about: "
+ + StringUtils.join(bugs, ",");
+ Logger.notifyUser(message);
+ }
+
}
--
GitLab