diff --git a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java index 87d6fb7f4339bed2e99ffa60a56dff9a71875350..36eb4f7f411da20884885b4a7ce911fcf419c96e 100644 --- a/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java +++ b/de.prob.core/src/de/prob/eventb/translator/internal/TranslationVisitor.java @@ -616,10 +616,8 @@ public class TranslationVisitor implements ISimpleVisitor { // I've encountered null types. Maybe that was a bug but just to be // sure (in most cases, missing type information won't hurt): if (type != null) { - // put a translation of the identifier on the stack ... - decl.accept(this); - // ... and take it - final PExpression expr = expressions.pop(); + final PExpression expr = createIdentifierExpression(decl + .getName()); // construct "expr:type" final PPredicate member = new AMemberPredicate(expr, translateType(type)); 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 abab61b75326085b544e8704b0de7dda2541923b..f2d5d87b2e85eb5be776b3ce573fa8b818cb0a50 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 @@ -2,10 +2,13 @@ package de.prob.eventb.disprover.core.internal; import java.util.Set; +import org.eclipse.core.runtime.Platform; import org.eclipse.core.runtime.jobs.Job; +import org.eclipse.core.runtime.preferences.InstanceScope; import org.eventb.core.IEventBProject; import org.eventb.core.ast.Predicate; import org.eventb.core.seqprover.IProofMonitor; +import org.osgi.service.prefs.Preferences; import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog; import de.be4.classicalb.core.parser.node.AEventBContextParseUnit; @@ -39,36 +42,47 @@ public class DisproverCommand implements IComposableCommand { private final Set<Predicate> allHypotheses; private final Set<Predicate> selectedHypotheses; private final Predicate goal; - private final int timeoutFactor; + private final int timeout; private static ComposedCommand composed; public DisproverCommand(Set<Predicate> allHypotheses, - Set<Predicate> selectedHypotheses, Predicate goal, int timeoutFactor) { + Set<Predicate> selectedHypotheses, Predicate goal, int timeout) { this.allHypotheses = allHypotheses; this.selectedHypotheses = selectedHypotheses; this.goal = goal; - this.timeoutFactor = timeoutFactor; + this.timeout = timeout; } public static ICounterExample disprove(Animator animator, IEventBProject project, Set<Predicate> allHypotheses, - Set<Predicate> selectedHypotheses, Predicate goal, - int timeoutFactor, AEventBContextParseUnit context, IProofMonitor pm) + Set<Predicate> selectedHypotheses, Predicate goal, int timeout, + AEventBContextParseUnit context, IProofMonitor pm) throws ProBException, InterruptedException { + Preferences prefNode = Platform.getPreferencesService().getRootNode() + .node(InstanceScope.SCOPE).node("prob_disprover_preferences"); final ClearMachineCommand clear = new ClearMachineCommand(); + final SetPreferencesCommand setPrefs = SetPreferencesCommand .createSetPreferencesCommand(animator); + // set clpfd and chr preference + final SetPreferenceCommand setCLPFD = new SetPreferenceCommand("CLPFD", + Boolean.toString(prefNode.getBoolean("clpfd", true))); + final SetPreferenceCommand setCHR = new SetPreferenceCommand("CHR", + Boolean.toString(prefNode.getBoolean("clpfd", true))); + DisproverLoadCommand load = new DisproverLoadCommand(project, context); StartAnimationCommand start = new StartAnimationCommand(); DisproverCommand disprove = new DisproverCommand(allHypotheses, - selectedHypotheses, goal, timeoutFactor); + selectedHypotheses, goal, timeout + * prefNode.getInt("timeout", 1000)); - composed = new ComposedCommand(clear, setPrefs, load, start, disprove); + composed = new ComposedCommand(clear, setPrefs, setCLPFD, setCHR, load, + start, disprove); final Job job = new ProBCommandJob("Disproving", animator, composed); job.setUser(true); @@ -107,7 +121,7 @@ public class DisproverCommand implements IComposableCommand { translatePredicate(pto, p); } pto.closeList(); - pto.printNumber(timeoutFactor); + pto.printNumber(timeout); pto.printVariable(RESULT); pto.closeTerm(); } diff --git a/de.prob.eventb.disprover.ui/plugin.xml b/de.prob.eventb.disprover.ui/plugin.xml index 093b599d9f70c2ce814067ab83867a4f65341227..7518659c1c1a9942bcb13f5034489f98f82c05c7 100644 --- a/de.prob.eventb.disprover.ui/plugin.xml +++ b/de.prob.eventb.disprover.ui/plugin.xml @@ -64,42 +64,13 @@ tooltip="%tactic.disprover.tooltip-relevant" /> --> </extension> <extension - point="org.eclipse.ui.commands"> - <command - id="de.prob.eventb.disprover.exportastest" - name="Export as ProB Disprover Testcase"> - </command> - </extension> - <extension - point="org.eclipse.ui.handlers"> - <handler - commandId="de.prob.eventb.disprover.exportastest"> - <class - class="de.prob.eventb.disprover.ui.export.ExportAsTestHandler"> - </class> - </handler> - </extension> - <extension - point="org.eclipse.ui.menus"> - <menuContribution - locationURI="popup:fr.systerel.explorer.navigator.view"> - <command - commandId="de.prob.eventb.disprover.exportastest" - label="Export as ProB Disprover Testcase" - style="push"> - <visibleWhen> - <with - variable="selection"> - <iterate - operator="or"> - <instanceof - value="org.eventb.core.IPSStatus"> - </instanceof> - </iterate> - </with> - </visibleWhen> - </command> - </menuContribution> + point="org.eclipse.ui.preferencePages"> + <page + category="probpreferences" + class="de.prob.eventb.disprover.ui.DisproverPreferences" + id="de.prob.ui.probclassic" + name="ProB (Dis-)Prover"> + </page> </extension> </plugin> diff --git a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java new file mode 100644 index 0000000000000000000000000000000000000000..6e32ed679ff21cbb8c92d9bfb4625100ba2da458 --- /dev/null +++ b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/DisproverPreferences.java @@ -0,0 +1,152 @@ +package de.prob.eventb.disprover.ui; + +import org.eclipse.core.runtime.Platform; +import org.eclipse.core.runtime.preferences.InstanceScope; +import org.eclipse.jface.preference.PreferencePage; +import org.eclipse.jface.resource.ImageDescriptor; +import org.eclipse.swt.SWT; +import org.eclipse.swt.events.*; +import org.eclipse.swt.layout.*; +import org.eclipse.swt.widgets.*; +import org.eclipse.ui.*; +import org.osgi.service.prefs.*; + +public class DisproverPreferences extends PreferencePage implements + IWorkbenchPreferencePage { + + public static final class PushButton extends SelectionAdapter { + + private final Text text; + private final Shell shell; + + public PushButton(final Shell shell, final Text text) { + this.shell = shell; + this.text = text; + } + + @Override + public void widgetSelected(final SelectionEvent e) { + super.widgetSelected(e); + FileDialog dialog = new FileDialog(shell, SWT.OPEN); + String open = dialog.open(); + text.setText(open); + } + + } + + private Preferences prefNode; + private Text timeoutTextField; + private Button checkCLPFD; + private Button checkCHR; + + public DisproverPreferences() { + super(); + } + + public DisproverPreferences(final String title) { + super(title); + } + + public DisproverPreferences(final String title, final ImageDescriptor image) { + super(title, image); + } + + @Override + protected Control createContents(final Composite parent) { + Composite pageComponent = new Composite(parent, SWT.NULL); + + GridLayout layout = new GridLayout(); + layout.numColumns = 2; + layout.marginHeight = 0; + layout.marginWidth = 0; + + pageComponent.setLayout(layout); + + new Label(pageComponent, SWT.NONE).setText("Time-out:"); + timeoutTextField = new Text(pageComponent, SWT.NONE); + int timeout = prefNode.getInt("timeout", 1000); + timeoutTextField.setText(Integer.toString(timeout)); + timeoutTextField.addVerifyListener(new VerifyListener() { + @Override + public void verifyText(VerifyEvent e) { + if (e.text.length() >= 1) { + e.doit = true; + for (int i = 0; i < e.text.length(); i++) { + if (!Character.isDigit(e.text.charAt(i))) { + e.doit = false; + } + } + } + } + }); + + Label timeoutRemark = new Label(pageComponent, SWT.WRAP); + timeoutRemark + .setText("Note: The time-out is applied to each constraint-solving action.\nThe maximum time-out is thus twice as long (solving with all hypotheses and with the selected hypotheses only)."); + GridData gridData2 = new GridData(); + gridData2.horizontalSpan = 2; + timeoutRemark.setLayoutData(gridData2); + + new Label(pageComponent, SWT.NONE).setText("Use CLP(FD) Solver:"); + checkCLPFD = new Button(pageComponent, SWT.CHECK); + checkCLPFD.setSelection(prefNode.getBoolean("clpfd", true)); + checkCLPFD.addSelectionListener(new SelectionListener() { + @Override + public void widgetSelected(SelectionEvent e) { + if (!checkCLPFD.getSelection()) { + checkCHR.setSelection(false); + } + } + + @Override + public void widgetDefaultSelected(SelectionEvent e) { + // TODO Auto-generated method stub + + } + }); + + new Label(pageComponent, SWT.NONE).setText("Use CHR Solver:"); + checkCHR = new Button(pageComponent, SWT.CHECK); + checkCHR.setSelection(prefNode.getBoolean("chr", true)); + checkCHR.addSelectionListener(new SelectionListener() { + @Override + public void widgetSelected(SelectionEvent e) { + if (checkCHR.getSelection()) { + checkCLPFD.setSelection(true); + } + } + + @Override + public void widgetDefaultSelected(SelectionEvent e) { + // TODO Auto-generated method stub + + } + }); + + Label chrRemark = new Label(pageComponent, SWT.WRAP); + chrRemark + .setText("Note: The CHR Solver can only be used in conjunction with the CLP(FD) solver."); + + return pageComponent; + } + + @Override + public boolean performOk() { + prefNode.put("timeout", timeoutTextField.getText()); + prefNode.putBoolean("clpfd", checkCLPFD.getSelection()); + prefNode.putBoolean("chr", checkCHR.getSelection()); + try { + prefNode.flush(); + } catch (BackingStoreException e) { + e.printStackTrace(); + } + return super.performOk(); + } + + @Override + public void init(final IWorkbench workbench) { + prefNode = Platform.getPreferencesService().getRootNode() + .node(InstanceScope.SCOPE).node("prob_disprover_preferences"); + } + +} diff --git a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportAsTestHandler.java b/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportAsTestHandler.java deleted file mode 100644 index d9aebc084f63a3110499f57c302334f11b168e19..0000000000000000000000000000000000000000 --- a/de.prob.eventb.disprover.ui/src/de/prob/eventb/disprover/ui/export/ExportAsTestHandler.java +++ /dev/null @@ -1,214 +0,0 @@ -package de.prob.eventb.disprover.ui.export; - -import java.io.*; - -import org.eclipse.core.commands.*; -import org.eclipse.core.runtime.Platform; -import org.eclipse.core.runtime.preferences.InstanceScope; -import org.eclipse.jface.dialogs.MessageDialog; -import org.eclipse.jface.viewers.*; -import org.eclipse.swt.SWT; -import org.eclipse.swt.widgets.*; -import org.eclipse.ui.handlers.HandlerUtil; -import org.eventb.core.*; -import org.eventb.core.ast.Predicate; -import org.eventb.core.pm.*; -import org.eventb.core.seqprover.*; -import org.osgi.service.prefs.*; -import org.rodinp.core.*; - -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.*; - -public class ExportAsTestHandler extends AbstractHandler implements IHandler { - @Override - public Object execute(final ExecutionEvent event) throws ExecutionException { - try { - final IPOSequent poSequent = getSelectedSequent(event); - final IProverSequent sequent = toProverSequent(poSequent); - - if (sequent != 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, sequent); - if (fileName != null) { - StringBuffer sb; - - sb = toDisproverMachine(sequent); - appendDisproverTestCase(sb, sequent, poSequent); - dumpStringBufferToFile(sb, fileName); - } - } - } catch (RodinDBException e) { - throw new ExecutionException(e.getMessage()); - } - return null; - } - - private void dumpStringBufferToFile(StringBuffer sb, String fileName) { - final boolean isSafeToWrite = isSafeToWrite(fileName); - - if (isSafeToWrite) { - PrintWriter out = null; - try { - out = new PrintWriter(new FileWriter(fileName)); - out.println(sb.toString()); - } catch (IOException e) { - Logger.notifyUser("Unable to append to file '" + fileName + "'"); - } finally { - if (out != null) { - out.close(); - } - } - } - - } - - 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(), - "Disprover Translation", null); - IProofTree proofTree = pa.getProofTree(); - - IProverSequent proverSequent = proofTree.getSequent(); - pa.dispose(); - - return proverSequent; - } - - private void appendDisproverTestCase(StringBuffer export, - IProverSequent sequent, IPOSequent poSequent) - throws RodinDBException { - - StringWriter st = new StringWriter(); - PrintWriter pw = new PrintWriter(st); - PrologTermOutput pto = new PrologTermOutput(pw, false); - - pto.openTerm("disprover_test"); - predicateToProlog(pto, sequent.goal()); - - pto.openList(); - for (Predicate p : sequent.hypIterable()) { - predicateToProlog(pto, p); - } - pto.closeList(); - - pto.printAtom("unknown"); - - pto.closeTerm(); - - if (pw != null) { - pw.close(); - } - - // add new testcase terms to the additional information list - int index = export.indexOf("],_Error))."); - export.insert(index, "," + st.toString()); - } - - private void predicateToProlog(IPrologTermOutput pto, Predicate pred) { - TranslationVisitor v = new TranslationVisitor(); - pred.accept(v); - ASTProlog p = new ASTProlog(pto, null); - v.getPredicate().apply(p); - } - - private IPOSequent getSelectedSequent(final ExecutionEvent event) { - final ISelection fSelection = HandlerUtil.getCurrentSelection(event); - IPSStatus status = null; - if (fSelection instanceof IStructuredSelection) { - final IStructuredSelection ssel = (IStructuredSelection) fSelection; - if (ssel.size() == 1 && ssel.getFirstElement() instanceof IPSStatus) { - status = (IPSStatus) ssel.getFirstElement(); - } - } - - return status.getPOSequent(); - } - - private String askForExportFile(final Preferences prefs, final Shell shell, - final IProverSequent sequent) { - final String path = prefs.get("dir", System.getProperty("user.home")); - - final FileDialog dialog = new FileDialog(shell, SWT.SAVE); - dialog.setFilterExtensions(new String[] { "*.eventb" }); - - dialog.setFilterPath(path); - dialog.setFileName("disprover_testcase.eventb"); - 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(".eventb")) { - result += ".eventb"; - } - } - return result; - } - - public static StringBuffer toDisproverMachine(final IProverSequent sequent) - throws RodinDBException { - AEventBContextParseUnit context = DisproverContextCreator - .createDisproverContext(sequent); - - StringWriter st = new StringWriter(); - PrintWriter pw = new PrintWriter(st); - PrologTermOutput pto = new PrologTermOutput(pw, false); - - pto.openTerm("package"); - pto.openTerm("load_event_b_project"); - pto.emptyList(); - - pto.openList(); - ASTProlog modelAst = new ASTProlog(pto, null); - context.apply(modelAst); - pto.closeList(); - - pto.openList(); - - pto.openTerm("exporter_version"); - pto.printNumber(3); - pto.closeTerm(); - - // try to export theories if available - IPOSequent x = (IPOSequent) sequent.getOrigin(); - IRodinProject project = x.getSources()[0].getRodinProject(); - - pto.closeList(); - - pto.printVariable("_Error"); - pto.closeTerm(); - pto.closeTerm(); - - st.append("."); - - return st.getBuffer(); - } - - 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; - } -}