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 c5993717ea796244cc3f5a6478a42f6c520504a0..53b96a69f6d6b315e7b947d5e6194dfb74177100 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; @@ -38,36 +41,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); @@ -106,7 +120,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 88397d1d524b2ad433a0943927f6062d091bc38b..7518659c1c1a9942bcb13f5034489f98f82c05c7 100644 --- a/de.prob.eventb.disprover.ui/plugin.xml +++ b/de.prob.eventb.disprover.ui/plugin.xml @@ -63,5 +63,14 @@ target="global" tooltip="%tactic.disprover.tooltip-relevant" /> --> </extension> + <extension + 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"); + } + +}