diff --git a/de.prob.ui/src/de/prob/ui/ltl/CounterExamplePropositionFigure.java b/de.prob.ui/src/de/prob/ui/ltl/CounterExamplePropositionFigure.java index abbe2e88fd15cd393d7ca9b4466620b6f022ea5f..08bac75624e8cdfd82190f3b114193c03aaa4900 100644 --- a/de.prob.ui/src/de/prob/ui/ltl/CounterExamplePropositionFigure.java +++ b/de.prob.ui/src/de/prob/ui/ltl/CounterExamplePropositionFigure.java @@ -292,129 +292,158 @@ public abstract class CounterExamplePropositionFigure extends Figure implements add(panel); for (int i = 0; i < values.size(); i++) { - final CounterExampleValueType value = values.get(i); - final Ellipse ellipse = new Ellipse(); + createColumn(bounds, argument, positions, ellipses1, ellipses2, + argumentHeight, pathType, values, panel, i); + } - if (!positions.contains(i)) { - ellipse.setAlpha(Alpha.MASKED); - } + if (parent != null) { + final Ellipse ellipse = ellipses2.get(stateId); + drawChildParentConnection(ellipse, stateId, parent); + } - ellipse.setAntialias(SWT.ON); - ellipse.setLineWidth(2); - ellipse.setOpaque(true); - ellipse.addMouseListener(this); - ellipse.addMouseMotionListener(this); - ellipse.setBackgroundColor(getEllipseColor(value)); + return panel; + } - ellipses1.put(ellipse, i); - ellipses2.put(i, ellipse); + private void createColumn(final Rectangle bounds, + final CounterExampleProposition argument, + final List<Integer> positions, + final Hashtable<Ellipse, Integer> ellipses1, + final Hashtable<Integer, Ellipse> ellipses2, + final int argumentHeight, final PathType pathType, + final List<CounterExampleValueType> values, Panel panel, int i) { + final CounterExampleValueType value = values.get(i); + final Ellipse ellipse = new Ellipse(); - final Label label = new Label(value.toString()); - label.setOpaque(false); + if (!positions.contains(i)) { + ellipse.setAlpha(Alpha.MASKED); + } - ellipse.setLayoutManager(new BorderLayout()); - ellipse.add(label, BorderLayout.CENTER); + ellipse.setAntialias(SWT.ON); + ellipse.setLineWidth(2); + ellipse.setOpaque(true); + ellipse.addMouseListener(this); + ellipse.addMouseMotionListener(this); + ellipse.setBackgroundColor(getEllipseColor(value)); - panel.add(ellipse); + ellipses1.put(ellipse, i); + ellipses2.put(i, ellipse); - final int x = (bounds.x + size) * (i + 1); - final int y = bounds.y + argumentHeight - + (pathType == PathType.INFINITE ? size / 10 : 0); - ellipse.setBounds(new Rectangle(x, y, size, size)); + final Label label = new Label(value.toString()); + label.setOpaque(false); - if (i > 0) { - final ChopboxAnchor source = new ChopboxAnchor(ellipse); - final Ellipse targetEllipse = ellipses2.get(i - 1); + ellipse.setLayoutManager(new BorderLayout()); + ellipse.add(label, BorderLayout.CENTER); - if (targetEllipse == null) - continue; + panel.add(ellipse); - final ChopboxAnchor target = new ChopboxAnchor(targetEllipse); + final int x = (bounds.x + size) * (i + 1); + final int y = bounds.y + argumentHeight + + (pathType == PathType.INFINITE ? size / 10 : 0); + ellipse.setBounds(new Rectangle(x, y, size, size)); - final PolylineConnection connection = new PolylineConnection(); - connection.setAlpha(Alpha.MASKED); - connection.setAntialias(SWT.ON); - connection.setLineStyle(SWT.LINE_SOLID); - connection.setLineWidth(2); - connection.setToolTip(new Label(getOperationName(i - 1))); - connection.setSourceAnchor(source); - connection.setTargetAnchor(target); + if (i > 0) { + final ChopboxAnchor source = new ChopboxAnchor(ellipse); + final Ellipse targetEllipse = ellipses2.get(i - 1); - final PolygonDecoration decoration = new PolygonDecoration(); - decoration.setAlpha(Alpha.MASKED); - decoration.setAntialias(SWT.ON); + if (targetEllipse == null) + return; - final PointList decorationPointList = new PointList(); - decorationPointList.addPoint(0, 0); - decorationPointList.addPoint(-1, 1); - decorationPointList.addPoint(-1, 0); - decorationPointList.addPoint(-1, -1); - decoration.setTemplate(decorationPointList); + final ChopboxAnchor target = new ChopboxAnchor(targetEllipse); - // highlight the transition - if (positions.contains(i) && positions.contains(i - 1)) { - connection.setAlpha(Alpha.HIGHLIGHED); - decoration.setAlpha(Alpha.HIGHLIGHED); - } + final PolylineConnection connection = new PolylineConnection(); + connection.setAlpha(Alpha.MASKED); + connection.setAntialias(SWT.ON); + connection.setLineStyle(SWT.LINE_SOLID); + connection.setLineWidth(2); + connection.setToolTip(new Label(getOperationName(i - 1))); + connection.setSourceAnchor(source); + connection.setTargetAnchor(target); - // highlight and color the transition - if (model.isTransition() || argument.isTransition()) { - if (positions.contains(i - 1)) { - connection.setAlpha(Alpha.HIGHLIGHED); - decoration.setAlpha(Alpha.HIGHLIGHED); - Color transitionColor = getEllipseColor(values - .get(i - 1)); - connection.setForegroundColor(transitionColor); - decoration.setForegroundColor(transitionColor); - } - } + final PolygonDecoration decoration = new PolygonDecoration(); + decoration.setAlpha(Alpha.MASKED); + decoration.setAntialias(SWT.ON); - connection.setSourceDecoration(decoration); + final PointList decorationPointList = new PointList(); + decorationPointList.addPoint(0, 0); + decorationPointList.addPoint(-1, 1); + decorationPointList.addPoint(-1, 0); + decorationPointList.addPoint(-1, -1); + decoration.setTemplate(decorationPointList); - panel.add(connection); + // highlight the transition + if (positions.contains(i) && positions.contains(i - 1)) { + connection.setAlpha(Alpha.HIGHLIGHED); + decoration.setAlpha(Alpha.HIGHLIGHED); } - if (i == values.size() - 1) { - if (pathType.equals(PathType.INFINITE)) { - final String operationName = getOperationName(ellipses1 - .get(ellipse)); - final Ellipse target = ellipses2.get(model.getLoopEntry()); - - int alpha = Alpha.MASKED; - Color loopTransitionColor = ColorConstants.black; + // highlight and color the transition + if (model.isTransition() || argument.isTransition()) { + if (positions.contains(i - 1)) { + connection.setAlpha(Alpha.HIGHLIGHED); + decoration.setAlpha(Alpha.HIGHLIGHED); + Color transitionColor = getEllipseColor(values.get(i - 1)); + connection.setForegroundColor(transitionColor); + decoration.setForegroundColor(transitionColor); + } + } - if (positions.contains(i) && positions.contains(i - 1)) { - alpha = Alpha.HIGHLIGHED; - } + connection.setSourceDecoration(decoration); - if (model.isTransition() || argument.isTransition()) { - if (positions.contains(i)) { - alpha = Alpha.HIGHLIGHED; - loopTransitionColor = getEllipseColor(values.get(i)); - } - } + panel.add(connection); + } - final PolylineConnection loop = createLoop(getInsets(), - ellipse, target, alpha, operationName, - loopTransitionColor); + boolean isLastElement = i == values.size() - 1; + if (isLastElement) { + createEnd(argument, positions, ellipses1, ellipses2, pathType, + values, panel, i, ellipse); + } + } - panel.add(loop); - } else if (pathType.equals(PathType.REDUCED)) { - final Polyline reduced = createReduced(getInsets(), - ellipse, positions.contains(i) ? Alpha.HIGHLIGHED - : Alpha.MASKED); + private void createEnd(final CounterExampleProposition argument, + final List<Integer> positions, + final Hashtable<Ellipse, Integer> ellipses1, + final Hashtable<Integer, Ellipse> ellipses2, + final PathType pathType, + final List<CounterExampleValueType> values, Panel panel, int i, + final Ellipse ellipse) { + final IFigure figure; + switch (pathType) { + case INFINITE: + final String operationName = getOperationName(ellipses1 + .get(ellipse)); + final Ellipse target = ellipses2.get(model.getLoopEntry()); + + int alpha = Alpha.MASKED; + Color loopTransitionColor = ColorConstants.black; + + final boolean highlightLoop = positions.contains(i) + && positions.contains(i - 1); + if (highlightLoop) { + alpha = Alpha.HIGHLIGHED; + } - panel.add(reduced); + if (model.isTransition() || argument.isTransition()) { + if (positions.contains(i)) { + alpha = Alpha.HIGHLIGHED; + loopTransitionColor = getEllipseColor(values.get(i)); } } + figure = createLoop(getInsets(), ellipse, target, alpha, + operationName, loopTransitionColor); + break; + + case REDUCED: + figure = createReduced(getInsets(), ellipse, + positions.contains(i) ? Alpha.HIGHLIGHED : Alpha.MASKED); + break; + + default: + figure = null; + break; } - - if (parent != null) { - final Ellipse ellipse = ellipses2.get(stateId); - drawChildParentConnection(ellipse, stateId, parent); + if (figure != null) { + panel.add(figure); } - - return panel; } @Override