From 5395045c3b1c23944648f661407da0c7c443a6ff Mon Sep 17 00:00:00 2001
From: Sebastian Krings <sebastian@krin.gs>
Date: Mon, 15 Sep 2014 09:41:32 +0200
Subject: [PATCH] export proof status together with the pos
---
.../disprover/ui/export/ExportPOsHandler.java | 20 ++++++++++++++++---
1 file changed, 17 insertions(+), 3 deletions(-)
diff --git a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java
index a5872981..65424a65 100644
--- a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java
+++ b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java
@@ -24,10 +24,13 @@ import org.eventb.core.IEventBRoot;
import org.eventb.core.IMachineRoot;
import org.eventb.core.IPORoot;
import org.eventb.core.IPOSequent;
+import org.eventb.core.IPSRoot;
+import org.eventb.core.IPSStatus;
import org.eventb.core.ast.Predicate;
import org.eventb.core.pm.IProofAttempt;
import org.eventb.core.pm.IProofComponent;
import org.eventb.core.pm.IProofManager;
+import org.eventb.core.seqprover.IConfidence;
import org.eventb.core.seqprover.IProofTree;
import org.eventb.core.seqprover.IProverSequent;
import org.osgi.service.prefs.BackingStoreException;
@@ -111,11 +114,13 @@ public class ExportPOsHandler extends AbstractHandler implements IHandler {
if (root instanceof IContextRoot) {
IContextRoot croot = (IContextRoot) root;
IPORoot poRoot = croot.getSCContextRoot().getPORoot();
- exportPOs(fw, poRoot);
+ IPSRoot psRoot = croot.getSCContextRoot().getPSRoot();
+ exportPOs(fw, poRoot, psRoot);
} else if (root instanceof IMachineRoot) {
IMachineRoot croot = (IMachineRoot) root;
IPORoot poRoot = croot.getSCMachineRoot().getPORoot();
- exportPOs(fw, poRoot);
+ IPSRoot psRoot = croot.getSCMachineRoot().getPSRoot();
+ exportPOs(fw, poRoot, psRoot);
} else {
throw new IllegalArgumentException(
"Not a Context or Machine root.");
@@ -137,7 +142,7 @@ public class ExportPOsHandler extends AbstractHandler implements IHandler {
}
}
- private static void exportPOs(PrintWriter fw, IPORoot poRoot)
+ private static void exportPOs(PrintWriter fw, IPORoot poRoot, IPSRoot psRoot)
throws RodinDBException {
PrologTermOutput pto = new PrologTermOutput(fw, false);
ASTProlog modelAst = new ASTProlog(pto, null);
@@ -184,6 +189,15 @@ public class ExportPOsHandler extends AbstractHandler implements IHandler {
tVisitor.getPredicate().apply(modelAst);
}
pto.closeList();
+
+ // The result: true = proven in rodin, unknown else
+ IPSStatus status = psRoot.getStatus(ipoSequent.getElementName());
+ if (status.getConfidence() == IConfidence.DISCHARGED_MAX) {
+ pto.printAtom("true");
+ } else {
+ pto.printAtom("unknown");
+ }
+
pto.closeTerm();
pto.fullstop();
}
--
GitLab