diff --git a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java
index f2d5d87b2e85eb5be776b3ce573fa8b818cb0a50..8596f053818fcf67b9bc9360990fa697f13d31b8 100644
--- a/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java
+++ b/de.prob.eventb.disprover.core/src/de/prob/eventb/disprover/core/internal/DisproverCommand.java
@@ -12,15 +12,23 @@ import org.osgi.service.prefs.Preferences;
import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
-import de.prob.core.*;
-import de.prob.core.command.*;
+import de.prob.core.Animator;
+import de.prob.core.ProBCommandJob;
+import de.prob.core.command.ClearMachineCommand;
+import de.prob.core.command.CommandException;
+import de.prob.core.command.ComposedCommand;
+import de.prob.core.command.IComposableCommand;
+import de.prob.core.command.SetPreferenceCommand;
+import de.prob.core.command.SetPreferencesCommand;
+import de.prob.core.command.StartAnimationCommand;
import de.prob.eventb.disprover.core.DisproverReasoner;
import de.prob.eventb.disprover.core.command.DisproverLoadCommand;
import de.prob.eventb.translator.internal.TranslationVisitor;
import de.prob.exceptions.ProBException;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
-import de.prob.prolog.term.*;
+import de.prob.prolog.term.ListPrologTerm;
+import de.prob.prolog.term.PrologTerm;
/**
* The DisproverCommand takes two sets of ASTs (one for the machine and a list
@@ -109,8 +117,7 @@ public class DisproverCommand implements IComposableCommand {
public void writeCommand(final IPrologTermOutput pto) {
pto.openTerm("cbc_disprove");
- Predicate pred = goal;
- translatePredicate(pto, pred);
+ translatePredicate(pto, goal);
pto.openList();
for (Predicate p : this.allHypotheses) {
translatePredicate(pto, p);
diff --git a/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF b/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF
index 01f62e3ae5639352456797082f2693b6a3c58ff1..7da02f437ed882118a388b45023b6872d0761fbb 100644
--- a/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF
+++ b/de.prob.eventb.disprover.ui/META-INF/MANIFEST.MF
@@ -13,7 +13,8 @@ Require-Bundle: org.eclipse.core.runtime,
org.eventb.core.seqprover;bundle-version="[3.0.0,3.2.0)",
org.eclipse.osgi,
org.rodinp.core;bundle-version="[1.7.0,1.8.0)",
- org.eventb.core;bundle-version="[3.0.0,3.2.0)"
+ org.eventb.core;bundle-version="[3.0.0,3.2.0)",
+ de.prob.ui;bundle-version="7.4.0"
Bundle-RequiredExecutionEnvironment: J2SE-1.5
Bundle-ActivationPolicy: lazy
Bundle-Localization: plugin
diff --git a/de.prob.eventb.disprover.ui/icons/prob_mini_logo.gif b/de.prob.eventb.disprover.ui/icons/prob_mini_logo.gif
new file mode 100644
index 0000000000000000000000000000000000000000..c6867d469651f80e12a2021e619563e3f2a39b64
Binary files /dev/null and b/de.prob.eventb.disprover.ui/icons/prob_mini_logo.gif differ
diff --git a/de.prob.eventb.disprover.ui/plugin.xml b/de.prob.eventb.disprover.ui/plugin.xml
index 7518659c1c1a9942bcb13f5034489f98f82c05c7..9d24e750d23e001f5df639f2575b21f6dc5cef3e 100644
--- a/de.prob.eventb.disprover.ui/plugin.xml
+++ b/de.prob.eventb.disprover.ui/plugin.xml
@@ -72,5 +72,32 @@
name="ProB (Dis-)Prover">
</page>
</extension>
+ <extension
+ point="org.eclipse.ui.commands">
+ <command
+ id="de.prob.eventb.disprover.ui.exportpos"
+ name="Export Proof Obligations for ProB">
+ </command>
+ </extension>
+ <extension
+ point="org.eclipse.ui.handlers">
+ <handler
+ class="de.prob.eventb.disprover.ui.export.ExportPOsHandler"
+ commandId="de.prob.eventb.disprover.ui.exportpos">
+ </handler>
+ </extension>
+ <extension
+ point="org.eclipse.ui.menus">
+ <menuContribution
+ allPopups="false"
+ locationURI="popup:more_commands">
+ <command
+ commandId="de.prob.eventb.disprover.ui.exportpos"
+ icon="icons/prob_mini_logo.gif"
+ label="Export POs for ProB"
+ style="push">
+ </command>
+ </menuContribution>
+ </extension>
</plugin>
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
new file mode 100644
index 0000000000000000000000000000000000000000..c8f37a36960ca87cab6bc79d9007774b83d9c27f
--- /dev/null
+++ b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportPOsHandler.java
@@ -0,0 +1,202 @@
+package de.prob.eventb.disprover.ui.export;
+
+import java.io.File;
+import java.io.IOException;
+import java.io.PrintWriter;
+
+import org.eclipse.core.commands.AbstractHandler;
+import org.eclipse.core.commands.ExecutionEvent;
+import org.eclipse.core.commands.ExecutionException;
+import org.eclipse.core.commands.IHandler;
+import org.eclipse.core.runtime.Platform;
+import org.eclipse.core.runtime.preferences.InstanceScope;
+import org.eclipse.jface.dialogs.MessageDialog;
+import org.eclipse.jface.viewers.ISelection;
+import org.eclipse.jface.viewers.IStructuredSelection;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.widgets.FileDialog;
+import org.eclipse.swt.widgets.Shell;
+import org.eclipse.ui.handlers.HandlerUtil;
+import org.eventb.core.EventBPlugin;
+import org.eventb.core.IContextRoot;
+import org.eventb.core.IEventBRoot;
+import org.eventb.core.IMachineRoot;
+import org.eventb.core.IPORoot;
+import org.eventb.core.IPOSequent;
+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.IProofTree;
+import org.eventb.core.seqprover.IProverSequent;
+import org.osgi.service.prefs.BackingStoreException;
+import org.osgi.service.prefs.Preferences;
+import org.rodinp.core.RodinDBException;
+
+import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
+import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
+import de.prob.eventb.disprover.core.translation.DisproverContextCreator;
+import de.prob.eventb.translator.internal.TranslationVisitor;
+import de.prob.logging.Logger;
+import de.prob.prolog.output.PrologTermOutput;
+
+public class ExportPOsHandler extends AbstractHandler implements IHandler {
+
+ @Override
+ public Object execute(final ExecutionEvent event) throws ExecutionException {
+ final IEventBRoot root = getSelectedEventBRoot(event);
+ if (root != null) {
+ final Preferences prefs = Platform.getPreferencesService()
+ .getRootNode().node(InstanceScope.SCOPE)
+ .node("prob_export_preferences");
+ final Shell shell = HandlerUtil.getActiveShell(event);
+ final String fileName = askForExportFile(prefs, shell, root);
+ if (fileName != null) {
+ exportPOs(fileName, root);
+ }
+ }
+ return null;
+ }
+
+ private IEventBRoot getSelectedEventBRoot(final ExecutionEvent event) {
+ final ISelection fSelection = HandlerUtil.getCurrentSelection(event);
+ IEventBRoot root = null;
+ if (fSelection instanceof IStructuredSelection) {
+ final IStructuredSelection ssel = (IStructuredSelection) fSelection;
+ if (ssel.size() == 1
+ && ssel.getFirstElement() instanceof IEventBRoot) {
+ root = (IEventBRoot) ssel.getFirstElement();
+ }
+ }
+ return root;
+ }
+
+ private String askForExportFile(final Preferences prefs, final Shell shell,
+ final IEventBRoot root) {
+ final String path = prefs.get("dir", System.getProperty("user.home"));
+
+ final FileDialog dialog = new FileDialog(shell, SWT.SAVE);
+ dialog.setFilterExtensions(new String[] { "*.pl" });
+
+ dialog.setFilterPath(path);
+ final String subext = (root instanceof IMachineRoot) ? "_mch" : "_ctx";
+ dialog.setFileName(root.getComponentName() + subext + ".pl");
+ String result = dialog.open();
+ if (result != null) {
+ final String newPath = dialog.getFilterPath();
+ if (!path.equals(newPath)) {
+ prefs.put("dir", newPath);
+ try {
+ prefs.flush();
+ } catch (BackingStoreException e) {
+ // Ignore, if preferences are not stored correctly we simply
+ // ignore it (annoying, but not critical)
+ }
+ }
+ if (!result.endsWith(".pl")) {
+ result += ".pl";
+ }
+ }
+ return result;
+ }
+
+ public static void exportPOs(final String filename, final IEventBRoot root) {
+ final boolean isSafeToWrite = isSafeToWrite(filename);
+
+ if (isSafeToWrite) {
+ PrintWriter fw = null;
+ try {
+ fw = new PrintWriter(filename);
+ if (root instanceof IContextRoot) {
+ IContextRoot croot = (IContextRoot) root;
+ IPORoot poRoot = croot.getSCContextRoot().getPORoot();
+ exportPOs(fw, poRoot);
+ } else if (root instanceof IMachineRoot) {
+ IMachineRoot croot = (IMachineRoot) root;
+ IPORoot poRoot = croot.getSCMachineRoot().getPORoot();
+ exportPOs(fw, poRoot);
+ } else {
+ throw new IllegalArgumentException(
+ "Not a Context or Machine root.");
+ }
+ fw.append('\n');
+
+ } catch (IllegalArgumentException e) {
+ Logger.notifyUser(e.getMessage());
+ } catch (IOException e) {
+ Logger.notifyUser("Unable to create file '" + filename + "'");
+ } catch (RodinDBException e) {
+ // TODO Auto-generated catch block
+ e.printStackTrace();
+ } finally {
+ if (fw != null) {
+ fw.close();
+ }
+ }
+ }
+ }
+
+ private static void exportPOs(PrintWriter fw, IPORoot poRoot)
+ throws RodinDBException {
+ PrologTermOutput pto = new PrologTermOutput(fw);
+ ASTProlog modelAst = new ASTProlog(pto, null);
+ TranslationVisitor tVisitor = new TranslationVisitor();
+
+ IPOSequent[] sequents = poRoot.getSequents();
+ for (IPOSequent ipoSequent : sequents) {
+ IProverSequent proverSequent = toProverSequent(ipoSequent);
+ AEventBContextParseUnit disproverContext = DisproverContextCreator
+ .createDisproverContext(proverSequent);
+
+ // disprover_po(Name,Context,Goal,Hyps,SelectedHyps)
+ pto.openTerm("disprover_po");
+
+ pto.printAtom(proverSequent.toString());
+
+ disproverContext.apply(modelAst);
+
+ proverSequent.goal().accept(tVisitor);
+ tVisitor.getPredicate().apply(modelAst);
+
+ pto.openList();
+ for (Predicate hyp : proverSequent.hypIterable()) {
+ hyp.accept(tVisitor);
+ tVisitor.getPredicate().apply(modelAst);
+ }
+ pto.closeList();
+
+ pto.openList();
+ for (Predicate hyp : proverSequent.selectedHypIterable()) {
+ hyp.accept(tVisitor);
+ tVisitor.getPredicate().apply(modelAst);
+ }
+ pto.closeList();
+ }
+ }
+
+ public static IProverSequent toProverSequent(IPOSequent sequent)
+ throws RodinDBException {
+ IPORoot poRoot = (IPORoot) sequent.getRoot();
+ IProofManager pm = EventBPlugin.getProofManager();
+ IProofComponent pc = pm.getProofComponent(poRoot);
+ IProofAttempt pa = pc.createProofAttempt(sequent.getElementName(),
+ "ProB PO Export", null);
+
+ IProofTree proofTree = pa.getProofTree();
+
+ IProverSequent proverSequent = proofTree.getSequent();
+ pa.dispose();
+
+ return proverSequent;
+ }
+
+ private static boolean isSafeToWrite(final String filename) {
+ if (new File(filename).exists()) {
+ final MessageDialog dialog = new MessageDialog(null, "File exists",
+ null, "The file exists. Do you want to overwrite it?",
+ MessageDialog.QUESTION, new String[] { "Yes", "No" }, 0);
+ return dialog.open() == 0;
+ } else
+ return true;
+ }
+}