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