From 8aac321f5e142b5de45c29003a0bc47dbb1372d0 Mon Sep 17 00:00:00 2001 From: Vojtech Forejt Date: Fri, 21 Dec 2012 13:09:08 +0000 Subject: [PATCH] Pareto points in GUI must be added in the right order to be shown git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6259 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../properties/GUIMultiProperties.java | 20 ++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/prism/src/userinterface/properties/GUIMultiProperties.java b/prism/src/userinterface/properties/GUIMultiProperties.java index 4f42db4f..887f0598 100644 --- a/prism/src/userinterface/properties/GUIMultiProperties.java +++ b/prism/src/userinterface/properties/GUIMultiProperties.java @@ -54,6 +54,9 @@ import java.io.FileWriter; import java.io.IOException; import java.io.PrintWriter; import java.util.ArrayList; +import java.util.List; +import java.util.Comparator; +import java.util.Collections; import javax.swing.AbstractAction; import javax.swing.Action; @@ -905,7 +908,22 @@ public class GUIMultiProperties extends GUIPlugin implements MouseListener, List graph.getYAxisSettings().setHeading(TileList.getStoredFormulasY().get(i).toString()); SeriesKey sk = graph.addSeries("Pareto curve"); - for (prism.Point p : tl.getPoints()) { + //Get points in tilelist and sort them. This is required for the graph to show them right + List l = tl.getPoints(); + Comparator c = new Comparator() + { + public int compare(prism.Point o1, prism.Point o2) + { + if (o1.getCoord(0) == o2.getCoord(0)) + return Double.compare(o1.getCoord(1), o2.getCoord(1)); + else + return Double.compare(o1.getCoord(0), o2.getCoord(0)); + }; + }; + + Collections.sort(l, c); + + for (prism.Point p : l) { prism.Point pReal = p.toRealProperties(tl.getOpsAndBoundsList()); XYDataItem di = new XYDataItem(pReal.getCoord(0), pReal.getCoord(1)); graph.addPointToSeries(sk, di);