charts for future task runtime statistics;
authorwenzelm
Fri Jan 18 22:31:57 2013 +0100 (2013-01-18)
changeset 50980bc746aa3e8d5
parent 50979 21da2a03b9d2
child 50981 1791a90a94fb
charts for future task runtime statistics;
src/Pure/Tools/task_statistics.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/task_statistics.scala	Fri Jan 18 22:31:57 2013 +0100
     1.3 @@ -0,0 +1,59 @@
     1.4 +/*  Title:      Pure/ML/task_statistics.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Future task runtime statistics.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import scala.swing.{Frame, Component}
    1.14 +
    1.15 +import org.jfree.data.statistics.HistogramDataset
    1.16 +import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
    1.17 +import org.jfree.chart.plot.{XYPlot, PlotOrientation}
    1.18 +import org.jfree.chart.renderer.xy.{XYBarRenderer, StandardXYBarPainter}
    1.19 +
    1.20 +
    1.21 +object Task_Statistics
    1.22 +{
    1.23 +  def apply(stats: List[Properties.T]): Task_Statistics = new Task_Statistics(stats)
    1.24 +}
    1.25 +
    1.26 +final class Task_Statistics private(val stats: List[Properties.T])
    1.27 +{
    1.28 +  val Task_Name = new Properties.String("task_name")
    1.29 +  val Run = new Properties.Int("run")
    1.30 +
    1.31 +  def chart(bins: Int = 100): JFreeChart =
    1.32 +  {
    1.33 +    val values = new Array[Double](stats.length)
    1.34 +    for ((Run(x), i) <- stats.iterator.zipWithIndex) values(i) =
    1.35 +      Math.log10(x.toDouble / 1000000)
    1.36 +
    1.37 +    val data = new HistogramDataset
    1.38 +    data.addSeries("tasks", values, bins)
    1.39 +
    1.40 +    val c =
    1.41 +      ChartFactory.createHistogram("Task runtime distribution",
    1.42 +        "log10(runtime / s)", "number of tasks", data,
    1.43 +        PlotOrientation.VERTICAL, true, true, true)
    1.44 +
    1.45 +    val renderer = c.getPlot.asInstanceOf[XYPlot].getRenderer.asInstanceOf[XYBarRenderer]
    1.46 +    renderer.setMargin(0.1)
    1.47 +    renderer.setBarPainter(new StandardXYBarPainter)
    1.48 +
    1.49 +    c
    1.50 +  }
    1.51 +
    1.52 +  def show_frame(bins: Int = 100): Unit =
    1.53 +    Swing_Thread.later {
    1.54 +      new Frame {
    1.55 +        iconImage = Isabelle_System.get_icon().getImage
    1.56 +        title = "Statistics"
    1.57 +        contents = Component.wrap(new ChartPanel(chart(bins)))
    1.58 +        visible = true
    1.59 +      }
    1.60 +    }
    1.61 +}
    1.62 +
     2.1 --- a/src/Pure/build-jars	Fri Jan 18 20:31:22 2013 +0100
     2.2 +++ b/src/Pure/build-jars	Fri Jan 18 22:31:57 2013 +0100
     2.3 @@ -65,6 +65,7 @@
     2.4    Tools/build.scala
     2.5    Tools/build_dialog.scala
     2.6    Tools/main.scala
     2.7 +  Tools/task_statistics.scala
     2.8    library.scala
     2.9    package.scala
    2.10    term.scala