Skip to content
Snippets Groups Projects
Commit d00782ef authored by Sebastian Krings's avatar Sebastian Krings
Browse files

add preference page for disprover

parent a8d433df
No related branches found
No related tags found
No related merge requests found
...@@ -2,10 +2,13 @@ package de.prob.eventb.disprover.core.internal; ...@@ -2,10 +2,13 @@ package de.prob.eventb.disprover.core.internal;
import java.util.Set; import java.util.Set;
import org.eclipse.core.runtime.Platform;
import org.eclipse.core.runtime.jobs.Job; import org.eclipse.core.runtime.jobs.Job;
import org.eclipse.core.runtime.preferences.InstanceScope;
import org.eventb.core.IEventBProject; import org.eventb.core.IEventBProject;
import org.eventb.core.ast.Predicate; import org.eventb.core.ast.Predicate;
import org.eventb.core.seqprover.IProofMonitor; 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.analysis.prolog.ASTProlog;
import de.be4.classicalb.core.parser.node.AEventBContextParseUnit; import de.be4.classicalb.core.parser.node.AEventBContextParseUnit;
...@@ -38,36 +41,47 @@ public class DisproverCommand implements IComposableCommand { ...@@ -38,36 +41,47 @@ public class DisproverCommand implements IComposableCommand {
private final Set<Predicate> allHypotheses; private final Set<Predicate> allHypotheses;
private final Set<Predicate> selectedHypotheses; private final Set<Predicate> selectedHypotheses;
private final Predicate goal; private final Predicate goal;
private final int timeoutFactor; private final int timeout;
private static ComposedCommand composed; private static ComposedCommand composed;
public DisproverCommand(Set<Predicate> allHypotheses, public DisproverCommand(Set<Predicate> allHypotheses,
Set<Predicate> selectedHypotheses, Predicate goal, int timeoutFactor) { Set<Predicate> selectedHypotheses, Predicate goal, int timeout) {
this.allHypotheses = allHypotheses; this.allHypotheses = allHypotheses;
this.selectedHypotheses = selectedHypotheses; this.selectedHypotheses = selectedHypotheses;
this.goal = goal; this.goal = goal;
this.timeoutFactor = timeoutFactor; this.timeout = timeout;
} }
public static ICounterExample disprove(Animator animator, public static ICounterExample disprove(Animator animator,
IEventBProject project, Set<Predicate> allHypotheses, IEventBProject project, Set<Predicate> allHypotheses,
Set<Predicate> selectedHypotheses, Predicate goal, Set<Predicate> selectedHypotheses, Predicate goal, int timeout,
int timeoutFactor, AEventBContextParseUnit context, IProofMonitor pm) AEventBContextParseUnit context, IProofMonitor pm)
throws ProBException, InterruptedException { throws ProBException, InterruptedException {
Preferences prefNode = Platform.getPreferencesService().getRootNode()
.node(InstanceScope.SCOPE).node("prob_disprover_preferences");
final ClearMachineCommand clear = new ClearMachineCommand(); final ClearMachineCommand clear = new ClearMachineCommand();
final SetPreferencesCommand setPrefs = SetPreferencesCommand final SetPreferencesCommand setPrefs = SetPreferencesCommand
.createSetPreferencesCommand(animator); .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); DisproverLoadCommand load = new DisproverLoadCommand(project, context);
StartAnimationCommand start = new StartAnimationCommand(); StartAnimationCommand start = new StartAnimationCommand();
DisproverCommand disprove = new DisproverCommand(allHypotheses, 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); final Job job = new ProBCommandJob("Disproving", animator, composed);
job.setUser(true); job.setUser(true);
...@@ -106,7 +120,7 @@ public class DisproverCommand implements IComposableCommand { ...@@ -106,7 +120,7 @@ public class DisproverCommand implements IComposableCommand {
translatePredicate(pto, p); translatePredicate(pto, p);
} }
pto.closeList(); pto.closeList();
pto.printNumber(timeoutFactor); pto.printNumber(timeout);
pto.printVariable(RESULT); pto.printVariable(RESULT);
pto.closeTerm(); pto.closeTerm();
} }
......
...@@ -63,5 +63,14 @@ ...@@ -63,5 +63,14 @@
target="global" target="global"
tooltip="%tactic.disprover.tooltip-relevant" /> --> tooltip="%tactic.disprover.tooltip-relevant" /> -->
</extension> </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> </plugin>
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");
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment