1/* Title: Pure/Tools/task_statistics.scala 2 Author: Makarius 3 4Future task runtime statistics. 5*/ 6 7package isabelle 8 9 10import scala.swing.{Frame, Component} 11 12import org.jfree.data.statistics.HistogramDataset 13import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory} 14import org.jfree.chart.plot.{XYPlot, PlotOrientation} 15import org.jfree.chart.renderer.xy.{XYBarRenderer, StandardXYBarPainter} 16 17 18object Task_Statistics 19{ 20 def apply(session_name: String, task_statistics: List[Properties.T]): Task_Statistics = 21 new Task_Statistics(session_name, task_statistics) 22} 23 24final class Task_Statistics private( 25 val session_name: String, val task_statistics: List[Properties.T]) 26{ 27 private val Task_Name = new Properties.String("task_name") 28 private val Run = new Properties.Int("run") 29 30 def chart(bins: Int = 100): JFreeChart = 31 { 32 val values = new Array[Double](task_statistics.length) 33 for ((Run(x), i) <- task_statistics.iterator.zipWithIndex) 34 values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000) 35 36 val data = new HistogramDataset 37 data.addSeries("tasks", values, bins) 38 39 val c = 40 ChartFactory.createHistogram("Task runtime distribution", 41 "log10(runtime / s)", "number of tasks", data, 42 PlotOrientation.VERTICAL, true, true, true) 43 44 val renderer = c.getPlot.asInstanceOf[XYPlot].getRenderer.asInstanceOf[XYBarRenderer] 45 renderer.setMargin(0.1) 46 renderer.setBarPainter(new StandardXYBarPainter) 47 48 c 49 } 50 51 def show_frame(bins: Int = 100): Unit = 52 GUI_Thread.later { 53 new Frame { 54 iconImage = GUI.isabelle_image() 55 title = session_name 56 contents = Component.wrap(new ChartPanel(chart(bins))) 57 visible = true 58 } 59 } 60} 61 62