finalclass Task_Statistics private( val session_name: String, val task_statistics: List[Properties.T]
) { privateval Task_Name = new Properties.String("task_name") privateval Run = new Properties.Int("run")
def chart(bins: Int = 100): JFreeChart = { val values = new Array[Double](task_statistics.length) for (case (Run(x), i) <- task_statistics.iterator.zipWithIndex)
values(i) = java.lang.Math.log10((x max 1).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 =
GUI_Thread.later { new Frame {
iconImage = GUI.isabelle_image()
title = session_name
contents = Component.wrap(new ChartPanel(chart(bins)))
visible = true
}
}
}
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung:
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.