Skip to content
Snippets Groups Projects
Commit df7ef677 authored by dgelessus's avatar dgelessus
Browse files

Remove commented out "Analyze Invariant" command and related code

parent 32224f8a
No related branches found
No related tags found
No related merge requests found
package de.prob.core.command;
import de.prob.parser.ISimplifiedROMap;
import de.prob.prolog.output.IPrologTermOutput;
import de.prob.prolog.term.ListPrologTerm;
import de.prob.prolog.term.PrologTerm;
public class AnalyseInvariantCommand implements ISimpleTextCommand {
private static final String UNKNOWN = "Unknown";
private static final String FALSE = "False";
private static final String TOTAL = "Total";
private static final String RESULT = "Result";
private static final String DESCRIPTION = "Desc";
private StringBuffer text;
@Override
public void writeCommand(IPrologTermOutput pto) {
// analyse_predicate(Type,Desc,Result,Total,False,Unknown)
pto.openTerm("analyse_predicate").printAtom("invariant")
.printVariable(DESCRIPTION).printVariable(RESULT)
.printVariable(TOTAL).printVariable(FALSE)
.printVariable(UNKNOWN).closeTerm();
}
@Override
public void processResult(ISimplifiedROMap<String, PrologTerm> bindings)
throws CommandException {
text = new StringBuffer();
text.append("Analysed: " + bindings.get(DESCRIPTION) + "\n");
text.append("-------------------------------------\n");
ListPrologTerm r = (ListPrologTerm) bindings.get(RESULT);
for (PrologTerm term : r) {
text.append(term);
text.append('\n');
}
text.append("-------------------------------------\n");
text.append("Total: " + bindings.get(TOTAL)+ "\n");
text.append("False: " + bindings.get(FALSE)+ "\n");
text.append("Unknown: " + bindings.get(UNKNOWN));
}
@Override
public String getResultingText() {
return text.toString();
}
}
package de.prob.core.command;
public interface ISimpleTextCommand extends IComposableCommand{
String getResultingText();
}
...@@ -30,13 +30,6 @@ ...@@ -30,13 +30,6 @@
name="contact"> name="contact">
</separator> </separator>
</menu> </menu>
<menu
id="analyze"
label="Analyze">
<separator
name="analyze">
</separator>
</menu>
</menu> </menu>
</menuContribution> </menuContribution>
<menuContribution <menuContribution
......
...@@ -320,11 +320,6 @@ ...@@ -320,11 +320,6 @@
id="de.prob.ui.opview.checks" id="de.prob.ui.opview.checks"
name="Checks"> name="Checks">
</command> </command>
<command
categoryId="de.prob.ui.commands.category"
id="de.prob.ui.exampleanalyzecommand"
name="Example for Analyze Commands">
</command>
<!-- <command <!-- <command
id="de.prob.ui.startdmc" id="de.prob.ui.startdmc"
name="Start Distributed Modelcheck"> name="Start Distributed Modelcheck">
...@@ -678,12 +673,6 @@ ...@@ -678,12 +673,6 @@
</enabledWhen> </enabledWhen>
</handler> </handler>
<handler
commandId="de.prob.ui.exampleanalyzecommand">
<class
class="de.prob.ui.internal.InvariantAnalyzeHandler">
</class>
</handler>
<handler commandId="de.prob.ui.ltl.counterexampleviewmenuhandler"> <handler commandId="de.prob.ui.ltl.counterexampleviewmenuhandler">
<class class="de.prob.ui.ltl.handler.CounterExampleViewMenuHandler"/> <class class="de.prob.ui.ltl.handler.CounterExampleViewMenuHandler"/>
<enabledWhen> <enabledWhen>
...@@ -1194,18 +1183,6 @@ ...@@ -1194,18 +1183,6 @@
</command> </command>
</menu> </menu>
</menuContribution> </menuContribution>
<!--
<menuContribution
allPopups="false"
locationURI="menu:analyze">
<command
commandId="de.prob.ui.exampleanalyzecommand"
label="Analyze Invariant"
mnemonic="I"
style="toggle">
</command>
</menuContribution>
-->
<menuContribution locationURI="menu:de.prob.ui.ltl.CounterExampleView"> <menuContribution locationURI="menu:de.prob.ui.ltl.CounterExampleView">
<menu <menu
label="Show as"> label="Show as">
......
package de.prob.ui.internal;
import org.eclipse.core.commands.AbstractHandler;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.commands.ExecutionException;
import org.eclipse.jface.dialogs.TitleAreaDialog;
import org.eclipse.swt.SWT;
import org.eclipse.swt.layout.GridData;
import org.eclipse.swt.widgets.Composite;
import org.eclipse.swt.widgets.Control;
import org.eclipse.swt.widgets.Shell;
import org.eclipse.swt.widgets.Text;
import org.eclipse.ui.handlers.HandlerUtil;
import de.prob.core.Animator;
import de.prob.core.ProBCommandJob;
import de.prob.core.ProBJobFinishedListener;
import de.prob.core.command.CommandException;
import de.prob.core.command.IComposableCommand;
import de.prob.core.command.ISimpleTextCommand;
import de.prob.logging.Logger;
public abstract class GenericAnalyzeHandler extends AbstractHandler {
public class GenericAnalyzeFinishedHandler extends ProBJobFinishedListener {
private final Shell shell;
public GenericAnalyzeFinishedHandler(Shell shell) {
this.shell = shell;
}
@Override
protected void showResult(IComposableCommand command, Animator animator) {
if (command instanceof ISimpleTextCommand) {
ISimpleTextCommand textcommand = (ISimpleTextCommand) command;
String text = textcommand.getResultingText();
display(text);
} else {
Logger.notifyUser(
"The invoked command did not implement the correct interface. Please report this bug.",
new CommandException(
"Error in "
+ command.getClass()
+ ". Class should implement ISimpleTextCommand."));
}
}
private void display(final String text) {
final TitleAreaDialog titleAreaDialog = new TitleAreaDialog(shell) {
@Override
protected Control createDialogArea(Composite parent) {
setTitle(name);
Composite composite = (Composite) super
.createDialogArea(parent);
Text t = new Text(composite, SWT.WRAP | SWT.MULTI | SWT.BORDER
| SWT.H_SCROLL | SWT.V_SCROLL);
GridData gridData =
new GridData(
GridData.HORIZONTAL_ALIGN_FILL | GridData.VERTICAL_ALIGN_FILL);
gridData.grabExcessVerticalSpace = true;
t.setLayoutData(gridData);
t.append(text);
return composite;
}
};
final Runnable runnable = new Runnable() {
@Override
public void run() {
titleAreaDialog.open();
}
};
shell.getDisplay().asyncExec(runnable);
}
}
private final ISimpleTextCommand command;
private final String name;
public GenericAnalyzeHandler(ISimpleTextCommand command, String name) {
this.command = command;
this.name = name;
}
@Override
public Object execute(ExecutionEvent event) throws ExecutionException {
final Shell shell = HandlerUtil.getActiveShell(event);
Animator animator = Animator.getAnimator();
if (animator.isMachineLoaded()) {
final ProBCommandJob job = new ProBCommandJob(name, animator,
command);
GenericAnalyzeFinishedHandler finishedHandler = new GenericAnalyzeFinishedHandler(
shell);
job.setUser(true);
job.addJobChangeListener(finishedHandler);
job.schedule();
} else {
Logger.notifyUser("No ProB animation running. This is a bug. Please submit a report. Error in declaraion of class "+this.getClass());
}
return null;
}
}
package de.prob.ui.internal;
import de.prob.core.command.AnalyseInvariantCommand;
public class InvariantAnalyzeHandler extends GenericAnalyzeHandler {
public InvariantAnalyzeHandler() {
super(new AnalyseInvariantCommand(), "Analyze Invariant");
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment