Skip to content
Snippets Groups Projects
Commit fd435a87 authored by Jens Bendisposto's avatar Jens Bendisposto
Browse files

and the same for contexts

parent 69fe12d1
No related branches found
No related tags found
No related merge requests found
......@@ -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,12 +182,12 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
private void collectProofInfo(IEventBRoot origin) throws RodinDBException {
List<String> bugs = new LinkedList<String>();
try {
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();
......@@ -221,6 +223,16 @@ public final class ContextTranslator extends AbstractComponentTranslator {
}
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);
}
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment