Skip to content
Snippets Groups Projects
Commit 887a197d authored by Daniel Plagge's avatar Daniel Plagge
Browse files

refactored LTL counter-example view (extracted class to represent view 

of a single tab)
parent 8cf04483
Branches
Tags
No related merge requests found
Show whitespace changes
Inline Side-by-side
de.prob.ui/src/de/prob/ui/ltl/CounterExamplePropositionFigure.java
+ 6
− 2
View file @ 887a197d
...@@ -32,8 +32,10 @@ import org.eclipse.swt.graphics.Font; ...@@ -32,8 +32,10 @@ import org.eclipse.swt.graphics.Font;
import org.eclipse.swt.widgets.Display; import org.eclipse.swt.widgets.Display;
import de.prob.core.command.LtlCheckingCommand.PathType; import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.core.domainobjects.Operation;
import de.prob.core.domainobjects.ltl.CounterExample; import de.prob.core.domainobjects.ltl.CounterExample;
import de.prob.core.domainobjects.ltl.CounterExampleProposition; import de.prob.core.domainobjects.ltl.CounterExampleProposition;
import de.prob.core.domainobjects.ltl.CounterExampleState;
import de.prob.core.domainobjects.ltl.CounterExampleValueType; import de.prob.core.domainobjects.ltl.CounterExampleValueType;
public abstract class CounterExamplePropositionFigure extends Figure implements public abstract class CounterExamplePropositionFigure extends Figure implements
...@@ -145,8 +147,10 @@ public abstract class CounterExamplePropositionFigure extends Figure implements ...@@ -145,8 +147,10 @@ public abstract class CounterExamplePropositionFigure extends Figure implements
protected String getOperationName(final int index) { protected String getOperationName(final int index) {
final CounterExampleFigure parentFigure = (CounterExampleFigure) getParent(); final CounterExampleFigure parentFigure = (CounterExampleFigure) getParent();
final CounterExample parentModel = parentFigure.getModel(); final CounterExample parentModel = parentFigure.getModel();
final String operationName = parentModel.getStates().get(index) final List<CounterExampleState> states = parentModel.getStates();
.getOperation().getName(); final CounterExampleState state = states.get(index);
final Operation operation = state.getOperation();
final String operationName = operation.getName();
return operationName; return operationName;
} }
......
de.prob.ui/src/de/prob/ui/ltl/CounterExampleTab.java 0 → 100644
+ 369
− 0
View file @ 887a197d
/**
*
*/
package de.prob.ui.ltl;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.List;
import org.eclipse.gef.DefaultEditDomain;
import org.eclipse.gef.EditDomain;
import org.eclipse.gef.EditPart;
import org.eclipse.gef.GraphicalViewer;
import org.eclipse.gef.editparts.ScalableRootEditPart;
import org.eclipse.gef.editparts.ZoomManager;
import org.eclipse.gef.print.PrintGraphicalViewerOperation;
import org.eclipse.gef.ui.parts.ScrollingGraphicalViewer;
import org.eclipse.jface.layout.TableColumnLayout;
import org.eclipse.jface.viewers.ArrayContentProvider;
import org.eclipse.jface.viewers.ColumnWeightData;
import org.eclipse.jface.viewers.TableViewer;
import org.eclipse.jface.viewers.TableViewerColumn;
import org.eclipse.jface.viewers.TreeViewer;
import org.eclipse.jface.viewers.TreeViewerColumn;
import org.eclipse.swt.SWT;
import org.eclipse.swt.SWTException;
import org.eclipse.swt.custom.CTabFolder;
import org.eclipse.swt.custom.CTabItem;
import org.eclipse.swt.custom.SashForm;
import org.eclipse.swt.custom.StackLayout;
import org.eclipse.swt.layout.FillLayout;
import org.eclipse.swt.printing.PrintDialog;
import org.eclipse.swt.printing.Printer;
import org.eclipse.swt.printing.PrinterData;
import org.eclipse.swt.widgets.Composite;
import org.eclipse.swt.widgets.Control;
import org.eclipse.swt.widgets.Display;
import de.prob.core.Animator;
import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.core.domainobjects.History;
import de.prob.core.domainobjects.HistoryItem;
import de.prob.core.domainobjects.Operation;
import de.prob.core.domainobjects.State;
import de.prob.core.domainobjects.ltl.CounterExample;
import de.prob.core.domainobjects.ltl.CounterExampleProposition;
import de.prob.core.domainobjects.ltl.CounterExampleState;
import de.prob.logging.Logger;
import de.prob.ui.ltl.CounterExampleViewPart.ViewType;
/**
* @author plagge
*
*/
public class CounterExampleTab {
private final CounterExample counterExample;
private final CTabItem tabItem;
private final StackLayout layout;
// Table view
private final TableViewer tableViewer;
// Tree view
private final TreeViewer treeViewer;
// Graphical view
private final ScalableRootEditPart rootEditPart;
private final GraphicalViewer graphicalViewer;
private final Control interactiveView;
// TODO remove it!
private int currentIndex = -1;
public CounterExampleTab(final CTabFolder tabFolder,
final CounterExample counterExample) {
this.counterExample = counterExample;
tabItem = new CTabItem(tabFolder, SWT.CLOSE);
tabItem.setText(counterExample.getPropositionRoot().toString());
final Composite sashForm = new SashForm(tabFolder, SWT.HORIZONTAL);
tabItem.setControl(sashForm);
final Composite composite = new Composite(sashForm, SWT.None);
layout = new StackLayout();
composite.setLayout(layout);
final Composite tableView = new Composite(composite, SWT.None);
tableViewer = createTableViewer(tableView, counterExample);
// createPopupMenu(tableViewer.getTable(), tableViewer);
final Composite treeView = new Composite(composite, SWT.None);
treeView.setLayout(new FillLayout());
treeViewer = createTreeViewer(treeView, counterExample);
// createPopupMenu(treeViewer.getTree(), treeViewer);
rootEditPart = new ScalableRootEditPart();
graphicalViewer = new ScrollingGraphicalViewer();
interactiveView = graphicalViewer.createControl(composite);
interactiveView.setBackground(Display.getDefault().getSystemColor(
SWT.COLOR_WHITE));
// createPopupMenu(interactiveView, graphicalViewer);
graphicalViewer.setRootEditPart(rootEditPart);
graphicalViewer.setEditPartFactory(new CounterExampleEditPartFactory());
graphicalViewer.setContents(counterExample);
EditDomain editDomain = new DefaultEditDomain(null);
editDomain.addViewer(graphicalViewer);
}
public CTabItem getTabitem() {
return tabItem;
}
private TableViewer createTableViewer(Composite parent,
final CounterExample counterExample) {
final CounterExampleTableViewer tableViewer = new CounterExampleTableViewer(
parent, SWT.BORDER | SWT.H_SCROLL | SWT.V_SCROLL);
tableViewer.getTable().setHeaderVisible(true);
tableViewer.getTable().setLinesVisible(true);
final TableColumnLayout layout = new TableColumnLayout();
parent.setLayout(layout);
createEventColumn(tableViewer, layout);
final Collection<CounterExampleProposition> propositions = counterExample
.getPropositionRoot().getChildren();
for (CounterExampleProposition proposition : propositions) {
createPropositionColumn(tableViewer, layout, proposition);
}
tableViewer.getTable().setToolTipText(
"Click to show the state in the history");
tableViewer.getTable()
.addMouseListener(
new CounterExampleTableMouseAdapter(tableViewer,
counterExample));
tableViewer.setContentProvider(new ArrayContentProvider());
tableViewer.setInput(counterExample.getStates());
return tableViewer;
}
private void createEventColumn(final TableViewer tableViewer,
final TableColumnLayout layout) {
final TableViewerColumn tableViewerColumn = new TableViewerColumn(
tableViewer, SWT.NONE);
tableViewerColumn.setLabelProvider(new TableColumnEventLabelProvider());
tableViewerColumn.getColumn().setText("Event");
tableViewerColumn.getColumn().setAlignment(SWT.CENTER);
layout.setColumnData(tableViewerColumn.getColumn(),
new ColumnWeightData(1));
}
private void createPropositionColumn(final TableViewer tableViewer,
final TableColumnLayout layout,
final CounterExampleProposition proposition) {
final TableViewerColumn tableViewerColumn = new TableViewerColumn(
tableViewer, SWT.NONE);
tableViewerColumn.setLabelProvider(new TableColumnValueLabelProvider(
proposition));
tableViewerColumn.getColumn().setText(proposition.toString());
tableViewerColumn.getColumn().setAlignment(SWT.CENTER);
layout.setColumnData(tableViewerColumn.getColumn(),
new ColumnWeightData(1));
}
private TreeViewer createTreeViewer(Composite parent,
CounterExample counterExample) {
final CounterExampleTreeViewer treeViewer = new CounterExampleTreeViewer(
parent, SWT.BORDER | SWT.H_SCROLL | SWT.V_SCROLL);
treeViewer.getTree().setHeaderVisible(true);
treeViewer.getTree().setLinesVisible(true);
TreeViewerColumn propositionColumn = new TreeViewerColumn(treeViewer,
SWT.CENTER);
propositionColumn
.setLabelProvider(new TreeColumnPropositionLabelProvider());
propositionColumn.getColumn().setAlignment(SWT.CENTER);
propositionColumn.getColumn().setText("Proposition");
for (int j = 0; j < counterExample.getStates().size(); j++) {
TreeViewerColumn column = new TreeViewerColumn(treeViewer,
SWT.CENTER);
column.getColumn().setAlignment(SWT.CENTER);
CounterExampleState state = counterExample.getStates().get(j);
column.setLabelProvider(new TreeColumnValueLabelProvider(state));
Operation operation = state.getOperation();
if (operation != null)
column.getColumn().setText(operation.getName());
else
column.getColumn().setText("No operation");
column.getColumn().pack();
}
treeViewer.getTree().setToolTipText(
"Click to show the state in the history");
treeViewer.getTree().addMouseListener(
new CounterExampleTreeMouseAdapter(treeViewer, counterExample));
// treeViewer.getTree().addMouseMoveListener(
// new CounterExampleTreeMouseMoveAdapter(treeViewer));
treeViewer.setContentProvider(new CounterExampleContentProvider());
treeViewer.setInput(Arrays
.asList(new CounterExampleProposition[] { counterExample
.getPropositionRoot() }));
treeViewer.expandAll();
propositionColumn.getColumn().pack();
return treeViewer;
}
public void printCounterExample(final String title) {
final PrintDialog dialog = new PrintDialog(graphicalViewer.getControl()
.getShell(), SWT.NULL);
try {
final PrinterData printerData = dialog.open();
if (printerData != null) {
final PrintGraphicalViewerOperation viewerOperation = new PrintGraphicalViewerOperation(
new Printer(printerData), graphicalViewer);
viewerOperation.run(title);
}
} catch (SWTException e) {
Logger.notifyUser("Failed to print the LTL counter example.", e);
}
}
public void updateTopControl(final ViewType viewType) {
final Control topControl;
switch (viewType) {
case TABLE:
topControl = tableViewer.getControl();
break;
case TREE:
topControl = treeViewer.getControl();
break;
case INTERACTIVE:
topControl = interactiveView;
break;
default:
throw new IllegalStateException(
"Unexpected view type in LTL counter-example view");
}
layout.topControl = topControl;
if (layout.topControl != null) {
final Composite parent = layout.topControl.getParent();
if (parent != null) {
parent.layout();
}
}
}
public CounterExample getCounterExample() {
return counterExample;
}
public void zoomIn() {
final ZoomManager zoomManager = rootEditPart.getZoomManager();
if (zoomManager != null) {
if (zoomManager != null && zoomManager.canZoomIn()) {
zoomManager.setZoom(zoomManager.getNextZoomLevel());
}
}
}
public void zoomOut() {
final ZoomManager zoomManager = rootEditPart.getZoomManager();
if (zoomManager != null) {
if (zoomManager != null && zoomManager.canZoomOut()) {
zoomManager.setZoom(zoomManager.getPreviousZoomLevel());
}
}
}
protected void stateChanged(final State activeState,
final Operation operation) {
if (activeState.isInitialized()) {
final List<Operation> fullPath = counterExample.getFullPath();
final Animator animator = Animator.getAnimator();
final History history = animator.getHistory();
if (isCounterExampleLoadedInHistory(counterExample)) {
final int initPathSize = counterExample.getInitPath().size();
currentIndex = history.getCurrentPosition() - initPathSize;
// HistoryItem item = history.getCurrent();
if (counterExample.getPathType() == PathType.INFINITE
&& currentIndex == fullPath.size() - initPathSize) {
currentIndex = counterExample.getLoopEntry();
}
}
treeViewer.refresh();
tableViewer.refresh();
// We know that each element is of type
// EditPart, but AbstractEditPart.getChildren() returns just
// a list
@SuppressWarnings("unchecked")
List<EditPart> children = rootEditPart.getChildren();
for (EditPart child : children) {
child.refresh();
}
currentIndex = -1;
}
}
private boolean isCounterExampleLoadedInHistory(final CounterExample ce) {
final List<Operation> fullPath = ce.getFullPath();
final Animator animator = Animator.getAnimator();
final History history = animator.getHistory();
final List<HistoryItem> historyItems = new ArrayList<HistoryItem>(
Arrays.asList(history.getAllItems()));
final boolean isLoaded;
if (!historyItems.isEmpty()) {
if (historyItems.get(historyItems.size() - 1).getOperation() == null) {
historyItems.remove(historyItems.size() - 1);
}
if (fullPath.size() == historyItems.size()) {
boolean ceIsEqual = true;
for (int i = 0; i < fullPath.size(); i++) {
final Operation ceOperation = fullPath.get(i);
final Operation histOperation = historyItems.get(i)
.getOperation();
if (!ceOperation.equals(histOperation)) {
ceIsEqual = false;
break;
}
}
isLoaded = ceIsEqual;
} else {
isLoaded = false;
}
} else {
isLoaded = false;
}
return isLoaded;
}
public int getCurrentIndex() {
return currentIndex;
}
}
de.prob.ui/src/de/prob/ui/ltl/CounterExampleViewPart.java
+ 33
− 377
View file @ 887a197d
package de.prob.ui.ltl; package de.prob.ui.ltl;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.List;
import org.eclipse.core.commands.Command; import org.eclipse.core.commands.Command;
import org.eclipse.core.commands.ExecutionException; import org.eclipse.core.commands.ExecutionException;
import org.eclipse.core.commands.ParameterizedCommand; import org.eclipse.core.commands.ParameterizedCommand;
import org.eclipse.gef.DefaultEditDomain;
import org.eclipse.gef.EditDomain;
import org.eclipse.gef.EditPart;
import org.eclipse.gef.GraphicalViewer;
import org.eclipse.gef.editparts.ScalableRootEditPart;
import org.eclipse.gef.editparts.ZoomManager;
import org.eclipse.gef.print.PrintGraphicalViewerOperation;
import org.eclipse.gef.ui.parts.ScrollingGraphicalViewer;
import org.eclipse.jface.action.MenuManager; import org.eclipse.jface.action.MenuManager;
import org.eclipse.jface.layout.TableColumnLayout;
import org.eclipse.jface.viewers.ArrayContentProvider;
import org.eclipse.jface.viewers.ColumnWeightData;
import org.eclipse.jface.viewers.TableViewer;
import org.eclipse.jface.viewers.TableViewerColumn;
import org.eclipse.jface.viewers.TreeViewer;
import org.eclipse.jface.viewers.TreeViewerColumn;
import org.eclipse.swt.SWT; import org.eclipse.swt.SWT;
import org.eclipse.swt.SWTException;
import org.eclipse.swt.custom.CTabFolder; import org.eclipse.swt.custom.CTabFolder;
import org.eclipse.swt.custom.CTabFolder2Adapter; import org.eclipse.swt.custom.CTabFolder2Adapter;
import org.eclipse.swt.custom.CTabFolderEvent; import org.eclipse.swt.custom.CTabFolderEvent;
import org.eclipse.swt.custom.CTabItem; import org.eclipse.swt.custom.CTabItem;
import org.eclipse.swt.custom.SashForm;
import org.eclipse.swt.custom.StackLayout;
import org.eclipse.swt.layout.FillLayout;
import org.eclipse.swt.printing.PrintDialog;
import org.eclipse.swt.printing.Printer;
import org.eclipse.swt.printing.PrinterData;
import org.eclipse.swt.widgets.Composite; import org.eclipse.swt.widgets.Composite;
import org.eclipse.swt.widgets.Control; import org.eclipse.swt.widgets.Control;
import org.eclipse.swt.widgets.Display; import org.eclipse.swt.widgets.Display;
...@@ -46,15 +19,9 @@ import org.eclipse.ui.handlers.HandlerUtil; ...@@ -46,15 +19,9 @@ import org.eclipse.ui.handlers.HandlerUtil;
import org.eclipse.ui.menus.CommandContributionItem; import org.eclipse.ui.menus.CommandContributionItem;
import org.eclipse.ui.services.ISourceProviderService; import org.eclipse.ui.services.ISourceProviderService;
import de.prob.core.Animator;
import de.prob.core.command.LtlCheckingCommand.PathType;
import de.prob.core.domainobjects.History;
import de.prob.core.domainobjects.HistoryItem;
import de.prob.core.domainobjects.Operation; import de.prob.core.domainobjects.Operation;
import de.prob.core.domainobjects.State; import de.prob.core.domainobjects.State;
import de.prob.core.domainobjects.ltl.CounterExample; import de.prob.core.domainobjects.ltl.CounterExample;
import de.prob.core.domainobjects.ltl.CounterExampleProposition;
import de.prob.core.domainobjects.ltl.CounterExampleState;
import de.prob.logging.Logger; import de.prob.logging.Logger;
import de.prob.ui.StateBasedViewPart; import de.prob.ui.StateBasedViewPart;
...@@ -73,44 +40,6 @@ public final class CounterExampleViewPart extends StateBasedViewPart { ...@@ -73,44 +40,6 @@ public final class CounterExampleViewPart extends StateBasedViewPart {
INTERACTIVE, TREE, TABLE INTERACTIVE, TREE, TABLE
}; };
private static class TabData {
private final CounterExample counterExample;
private final StackLayout layout;
// Table view
private final Composite tableView;
private final TableViewer tableViewer;
// Tree view
private final Composite treeView;
private final TreeViewer treeViewer;
// Graphical view
private final ScalableRootEditPart editPart;
private final GraphicalViewer graphicalViewer;
private final Control interactiveView;
public TabData(CounterExample counterExample, StackLayout layout,
Composite tableView, TableViewer tableViewer,
Composite treeView, TreeViewer treeViewer,
ScalableRootEditPart editPart, GraphicalViewer graphicalViewer,
Control interactiveView) {
super();
this.counterExample = counterExample;
this.layout = layout;
this.tableView = tableView;
this.tableViewer = tableViewer;
this.treeView = treeView;
this.treeViewer = treeViewer;
this.editPart = editPart;
this.graphicalViewer = graphicalViewer;
this.interactiveView = interactiveView;
}
}
private final List<CounterExample> counterExamples = new ArrayList<CounterExample>();
private CTabFolder tabFolder; private CTabFolder tabFolder;
private ViewType viewType = ViewType.INTERACTIVE; private ViewType viewType = ViewType.INTERACTIVE;
private int currentIndex = -1; private int currentIndex = -1;
...@@ -151,9 +80,7 @@ public final class CounterExampleViewPart extends StateBasedViewPart { ...@@ -151,9 +80,7 @@ public final class CounterExampleViewPart extends StateBasedViewPart {
public void addCounterExample(final CounterExample counterExample) { public void addCounterExample(final CounterExample counterExample) {
initializeMenuSetting(); initializeMenuSetting();
updateCounterExampleLoadedProvider(true); updateCounterExampleLoadedProvider(true);
counterExamples.add(counterExample);
final Runnable runnable = new Runnable() { final Runnable runnable = new Runnable() {
@Override @Override
...@@ -198,137 +125,48 @@ public final class CounterExampleViewPart extends StateBasedViewPart { ...@@ -198,137 +125,48 @@ public final class CounterExampleViewPart extends StateBasedViewPart {
} }
public void zoomInCounterExample() { public void zoomInCounterExample() {
final ZoomManager zoomManager = getZoomManager(); final CounterExampleTab tab = getCurrentTab();
if (zoomManager != null) { if (tab != null) {
if (zoomManager != null && zoomManager.canZoomIn()) { tab.zoomIn();
zoomManager.setZoom(zoomManager.getNextZoomLevel());
}
} }
} }
public void zoomOutCounterExample() { public void zoomOutCounterExample() {
final ZoomManager zoomManager = getZoomManager(); final CounterExampleTab tab = getCurrentTab();
if (zoomManager != null) { if (tab != null) {
if (zoomManager != null && zoomManager.canZoomOut()) { tab.zoomOut();
zoomManager.setZoom(zoomManager.getPreviousZoomLevel());
}
} }
} }
private ZoomManager getZoomManager() {
final TabData data = getCurrentTabData();
return data == null ? null : data.editPart.getZoomManager();
}
public void printCounterExample() { public void printCounterExample() {
final TabData data = getCurrentTabData(); final CounterExampleTab tab = getCurrentTab();
if (data != null) { if (tab != null) {
final GraphicalViewer graphicalViewer = data.graphicalViewer; tab.printCounterExample(getTitle());
final PrintDialog dialog = new PrintDialog(graphicalViewer
.getControl().getShell(), SWT.NULL);
try {
final PrinterData printerData = dialog.open();
if (printerData != null) {
final PrintGraphicalViewerOperation viewerOperation = new PrintGraphicalViewerOperation(
new Printer(printerData), graphicalViewer);
viewerOperation.run(getTitle());
}
} catch (SWTException e) {
Logger.notifyUser("Failed to print the LTL counter example.", e);
}
} }
} }
public void setViewType(ViewType viewType) { public void setViewType(ViewType viewType) {
this.viewType = viewType; this.viewType = viewType;
for (CTabItem tabItem : tabFolder.getItems()) { for (CTabItem tabItem : tabFolder.getItems()) {
final TabData data = getTabData(tabItem); final CounterExampleTab tab = getTab(tabItem);
updateTopControl(data); tab.updateTopControl(viewType);
} }
} }
public int getCurrentIndex() { public int getCurrentIndex() {
return currentIndex; final CounterExampleTab tab = getCurrentTab();
return tab != null ? tab.getCurrentIndex() : -1;
} }
@Override @Override
protected void stateChanged(final State activeState, protected void stateChanged(final State activeState,
final Operation operation) { final Operation operation) {
final TabData data = getCurrentTabData(); final CounterExampleTab tab = getCurrentTab();
if (data != null) { if (tab != null) {
if (activeState.isInitialized()) { tab.stateChanged(activeState, operation);
final CounterExample ce = data.counterExample;
final List<Operation> fullPath = ce.getFullPath();
final Animator animator = Animator.getAnimator();
final History history = animator.getHistory();
if (isCounterExampleLoadedInHistory(data.counterExample)) {
final int initPathSize = ce.getInitPath().size();
currentIndex = history.getCurrentPosition() - initPathSize;
// HistoryItem item = history.getCurrent();
if (ce.getPathType() == PathType.INFINITE
&& currentIndex == fullPath.size() - initPathSize) {
currentIndex = ce.getLoopEntry();
} }
} }
data.treeViewer.refresh();
data.tableViewer.refresh();
// We know that each element is of type
// EditPart, but AbstractEditPart.getChildren() returns just
// a list
@SuppressWarnings("unchecked")
List<EditPart> children = data.editPart.getChildren();
for (EditPart child : children) {
child.refresh();
}
currentIndex = -1;
}
}
}
private boolean isCounterExampleLoadedInHistory(final CounterExample ce) {
final List<Operation> fullPath = ce.getFullPath();
final Animator animator = Animator.getAnimator();
final History history = animator.getHistory();
final List<HistoryItem> historyItems = new ArrayList<HistoryItem>(
Arrays.asList(history.getAllItems()));
final boolean isLoaded;
if (!historyItems.isEmpty()) {
if (historyItems.get(historyItems.size() - 1).getOperation() == null) {
historyItems.remove(historyItems.size() - 1);
}
if (fullPath.size() == historyItems.size()) {
boolean ceIsEqual = true;
for (int i = 0; i < fullPath.size(); i++) {
final Operation ceOperation = fullPath.get(i);
final Operation histOperation = historyItems.get(i)
.getOperation();
if (!ceOperation.equals(histOperation)) {
ceIsEqual = false;
break;
}
}
isLoaded = ceIsEqual;
} else {
isLoaded = false;
}
} else {
isLoaded = false;
}
return isLoaded;
}
@Override @Override
protected void stateReset() { protected void stateReset() {
super.stateReset(); super.stateReset();
...@@ -341,6 +179,11 @@ public final class CounterExampleViewPart extends StateBasedViewPart { ...@@ -341,6 +179,11 @@ public final class CounterExampleViewPart extends StateBasedViewPart {
updateCounterExampleLoadedProvider(false); updateCounterExampleLoadedProvider(false);
} }
public CounterExample getCurrentCounterExample() {
final CounterExampleTab data = getCurrentTab();
return data == null ? null : data.getCounterExample();
}
private void updateCounterExampleLoadedProvider(boolean enabled) { private void updateCounterExampleLoadedProvider(boolean enabled) {
ISourceProviderService service = (ISourceProviderService) getSite() ISourceProviderService service = (ISourceProviderService) getSite()
.getService(ISourceProviderService.class); .getService(ISourceProviderService.class);
...@@ -351,214 +194,27 @@ public final class CounterExampleViewPart extends StateBasedViewPart { ...@@ -351,214 +194,27 @@ public final class CounterExampleViewPart extends StateBasedViewPart {
} }
private CTabItem createTabItem(final CounterExample counterExample) { private CTabItem createTabItem(final CounterExample counterExample) {
final CTabItem tabItem = new CTabItem(tabFolder, SWT.CLOSE); final CounterExampleTab ceTab = new CounterExampleTab(tabFolder,
tabItem.setText(counterExample.getPropositionRoot().toString()); counterExample);
final CTabItem tabItem = ceTab.getTabitem();
final Composite sashForm = new SashForm(tabFolder, SWT.HORIZONTAL); tabItem.setData(DATA_KEY, ceTab);
tabItem.setControl(sashForm); ceTab.updateTopControl(viewType);
final Composite composite = new Composite(sashForm, SWT.None);
final StackLayout layout = new StackLayout();
composite.setLayout(layout);
final Composite tableView = new Composite(composite, SWT.None);
TableViewer tableViewer = createTableViewer(tableView, counterExample);
// createPopupMenu(tableViewer.getTable(), tableViewer);
final Composite treeView = new Composite(composite, SWT.None);
treeView.setLayout(new FillLayout());
TreeViewer treeViewer = createTreeViewer(treeView, counterExample);
// createPopupMenu(treeViewer.getTree(), treeViewer);
final ScalableRootEditPart rootEditPart = new ScalableRootEditPart();
final GraphicalViewer graphicalViewer = new ScrollingGraphicalViewer();
final Control interactiveView = graphicalViewer
.createControl(composite);
interactiveView.setBackground(Display.getDefault().getSystemColor(
SWT.COLOR_WHITE));
// createPopupMenu(interactiveView, graphicalViewer);
graphicalViewer.setRootEditPart(rootEditPart);
graphicalViewer.setEditPartFactory(new CounterExampleEditPartFactory());
graphicalViewer.setContents(counterExample);
EditDomain editDomain = new DefaultEditDomain(null);
editDomain.addViewer(graphicalViewer);
final TabData tabData = new TabData(counterExample, layout, tableView,
tableViewer, treeView, treeViewer, rootEditPart,
graphicalViewer, interactiveView);
tabItem.setData(DATA_KEY, tabData);
updateTopControl(tabData);
return tabItem; return tabItem;
} }
private void updateTopControl(final TabData data) { private CounterExampleTab getCurrentTab() {
final Control topControl; final CounterExampleTab tab;
switch (viewType) {
case TABLE:
topControl = data.tableView;
break;
case TREE:
topControl = data.treeView;
break;
case INTERACTIVE:
topControl = data.interactiveView;
break;
default:
throw new IllegalStateException(
"Unexpected view type in LTL counter-example view");
}
final StackLayout layout = data.layout;
layout.topControl = topControl;
if (layout.topControl != null) {
final Composite parent = layout.topControl.getParent();
if (parent != null) {
parent.layout();
}
}
}
private TableViewer createTableViewer(Composite parent,
final CounterExample counterExample) {
final CounterExampleTableViewer tableViewer = new CounterExampleTableViewer(
parent, SWT.BORDER | SWT.H_SCROLL | SWT.V_SCROLL);
tableViewer.getTable().setHeaderVisible(true);
tableViewer.getTable().setLinesVisible(true);
final TableColumnLayout layout = new TableColumnLayout();
parent.setLayout(layout);
createEventColumn(tableViewer, layout);
final Collection<CounterExampleProposition> propositions = counterExample
.getPropositionRoot().getChildren();
for (CounterExampleProposition proposition : propositions) {
createPropositionColumn(tableViewer, layout, proposition);
}
tableViewer.getTable().setToolTipText(
"Click to show the state in the history");
tableViewer.getTable()
.addMouseListener(
new CounterExampleTableMouseAdapter(tableViewer,
counterExample));
tableViewer.setContentProvider(new ArrayContentProvider());
tableViewer.setInput(counterExample.getStates());
return tableViewer;
}
private void createEventColumn(final TableViewer tableViewer,
final TableColumnLayout layout) {
final TableViewerColumn tableViewerColumn = new TableViewerColumn(
tableViewer, SWT.NONE);
tableViewerColumn.setLabelProvider(new TableColumnEventLabelProvider());
tableViewerColumn.getColumn().setText("Event");
tableViewerColumn.getColumn().setAlignment(SWT.CENTER);
layout.setColumnData(tableViewerColumn.getColumn(),
new ColumnWeightData(1));
}
private void createPropositionColumn(final TableViewer tableViewer,
final TableColumnLayout layout,
final CounterExampleProposition proposition) {
final TableViewerColumn tableViewerColumn = new TableViewerColumn(
tableViewer, SWT.NONE);
tableViewerColumn.setLabelProvider(new TableColumnValueLabelProvider(
proposition));
tableViewerColumn.getColumn().setText(proposition.toString());
tableViewerColumn.getColumn().setAlignment(SWT.CENTER);
layout.setColumnData(tableViewerColumn.getColumn(),
new ColumnWeightData(1));
}
private TreeViewer createTreeViewer(Composite parent,
CounterExample counterExample) {
final CounterExampleTreeViewer treeViewer = new CounterExampleTreeViewer(
parent, SWT.BORDER | SWT.H_SCROLL | SWT.V_SCROLL);
treeViewer.getTree().setHeaderVisible(true);
treeViewer.getTree().setLinesVisible(true);
TreeViewerColumn propositionColumn = new TreeViewerColumn(treeViewer,
SWT.CENTER);
propositionColumn
.setLabelProvider(new TreeColumnPropositionLabelProvider());
propositionColumn.getColumn().setAlignment(SWT.CENTER);
propositionColumn.getColumn().setText("Proposition");
for (int j = 0; j < counterExample.getStates().size(); j++) {
TreeViewerColumn column = new TreeViewerColumn(treeViewer,
SWT.CENTER);
column.getColumn().setAlignment(SWT.CENTER);
CounterExampleState state = counterExample.getStates().get(j);
column.setLabelProvider(new TreeColumnValueLabelProvider(state));
Operation operation = state.getOperation();
if (operation != null)
column.getColumn().setText(operation.getName());
else
column.getColumn().setText("No operation");
column.getColumn().pack();
}
treeViewer.getTree().setToolTipText(
"Click to show the state in the history");
treeViewer.getTree().addMouseListener(
new CounterExampleTreeMouseAdapter(treeViewer, counterExample));
// treeViewer.getTree().addMouseMoveListener(
// new CounterExampleTreeMouseMoveAdapter(treeViewer));
treeViewer.setContentProvider(new CounterExampleContentProvider());
treeViewer.setInput(Arrays
.asList(new CounterExampleProposition[] { counterExample
.getPropositionRoot() }));
treeViewer.expandAll();
propositionColumn.getColumn().pack();
return treeViewer;
}
public CounterExample getCurrentCounterExample() {
final TabData data = getCurrentTabData();
return data == null ? null : data.counterExample;
}
private TabData getCurrentTabData() {
final TabData data;
if (tabFolder != null) { if (tabFolder != null) {
final CTabItem selection = tabFolder.getSelection(); final CTabItem selection = tabFolder.getSelection();
data = getTabData(selection); tab = getTab(selection);
} else { } else {
data = null; tab = null;
} }
return data; return tab;
} }
private TabData getTabData(final CTabItem item) { private CounterExampleTab getTab(final CTabItem item) {
return item == null ? null : (TabData) item.getData(DATA_KEY); return item == null ? null : (CounterExampleTab) item.getData(DATA_KEY);
} }
// private void createPopupMenu(Control control,
// ISelectionProvider selectionProvider) {
// MenuManager menuManager = new MenuManager();
// Menu viewMenu = menuManager.createContextMenu(control);
// control.setMenu(viewMenu);
// getSite().registerContextMenu(menuManager, selectionProvider);
// getSite().setSelectionProvider(selectionProvider);
// }
} }
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment