Properties returning intervals are plotted correctly in GUI graphs.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2905 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/graph/Graph.java

@@ -1592,8 +1592,11 @@ public class Graph extends ChartPanel implements SettingOwner, EntityResolver, O
 	 * Previously this was done using integers, which was unsafe if removeSeries
 	 * was used. The hashcode() and equals() implementation of Object (based on
 	 * object identity) are sufficient to use this as the key of a HashMap.
+	 * In addition, we add a 'next' field, to allow the same class to be used
+	 * to store (linked) lists of keys.
 	 */
 	public class SeriesKey 
 	{
+		public SeriesKey next = null;
 	}
 }

prism/src/userinterface/graph/GraphResultListener.java

@@ -83,23 +83,30 @@ public class GraphResultListener implements ResultListener
 			} else return; // Cancel if non integer/double			
 			
 			// Cancel if x = +/- infinity or NaN
-			if (x == Double.POSITIVE_INFINITY || x == Double.NEGATIVE_INFINITY || x != x) 
+			if (x == Double.POSITIVE_INFINITY || x == Double.NEGATIVE_INFINITY || Double.isNaN(x)) 
 				return;
 						
-            // For now, to plot intervals, just pick lower value
-            if (result instanceof Interval) {
-            	result = ((Interval) result).lower;
-            }
-            
-			// Get y coordinate
-			if(result instanceof Integer) {	
-				y = ((Integer)result).intValue(); 
-			} else if(result instanceof Double)	{
-				y = ((Double)result).doubleValue();
-			} else return; // Cancel if non integer/double
-
-			// Add point to graph
-			graph.addPointToSeries(seriesKey, new XYDataItem(x,y));
+			// Add point to graph (if of valid type) 
+			if (result instanceof Double) {
+				y = ((Double) result).doubleValue();
+				graph.addPointToSeries(seriesKey, new XYDataItem(x, y));
+			} else if (result instanceof Integer) {
+				y = ((Integer) result).intValue();
+				graph.addPointToSeries(seriesKey, new XYDataItem(x, y));
+			} else if (result instanceof Interval) {
+				Interval interval = (Interval) result;
+				if (interval.lower instanceof Double) {
+					y = ((Double) interval.lower).doubleValue();
+					graph.addPointToSeries(seriesKey, new XYDataItem(x, y));
+					y = ((Double) interval.upper).doubleValue();
+					graph.addPointToSeries(seriesKey.next, new XYDataItem(x, y));
+				} else if (result instanceof Integer) {
+					y = ((Integer) interval.lower).intValue();
+					graph.addPointToSeries(seriesKey, new XYDataItem(x, y));
+					y = ((Integer) interval.upper).intValue();
+					graph.addPointToSeries(seriesKey.next, new XYDataItem(x, y));
+				}
+			}
 		}
 	}