/* Title: Pure/ML/task_statistics.ML
Author: Makarius
Future task runtime statistics.
*/
package isabelle
import scala.swing.{Frame, Component}
import org.jfree.data.statistics.HistogramDataset
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
import org.jfree.chart.plot.{XYPlot, PlotOrientation}
import org.jfree.chart.renderer.xy.{XYBarRenderer, StandardXYBarPainter}
object Task_Statistics
{
def apply(stats: List[Properties.T]): Task_Statistics = new Task_Statistics(stats)
}
final class Task_Statistics private(val stats: List[Properties.T])
{
val Task_Name = new Properties.String("task_name")
val Run = new Properties.Int("run")
def chart(bins: Int = 100): JFreeChart =
{
val values = new Array[Double](stats.length)
for ((Run(x), i) <- stats.iterator.zipWithIndex) values(i) =
Math.log10(x.toDouble / 1000000)
val data = new HistogramDataset
data.addSeries("tasks", values, bins)
val c =
ChartFactory.createHistogram("Task runtime distribution",
"log10(runtime / s)", "number of tasks", data,
PlotOrientation.VERTICAL, true, true, true)
val renderer = c.getPlot.asInstanceOf[XYPlot].getRenderer.asInstanceOf[XYBarRenderer]
renderer.setMargin(0.1)
renderer.setBarPainter(new StandardXYBarPainter)
c
}
def show_frame(bins: Int = 100): Unit =
Swing_Thread.later {
new Frame {
iconImage = Isabelle_System.get_icon().getImage
title = "Statistics"
contents = Component.wrap(new ChartPanel(chart(bins)))
visible = true
}
}
}