+ # Export the metric set in CSV format
+ fun to_csv: CsvDocument do
+ var csv = new CsvDocument
+
+ csv.format = new CsvFormat('"', ';', "\n")
+
+ # set csv headers
+ csv.header.add("entry")
+ for metric in metrics do csv.header.add(metric.name)
+
+ # collect all entries to merge metric results
+ var entries = new HashSet[ELM]
+ for metric in metrics do
+ for entry in metric.values.keys do entries.add(entry)
+ end
+
+ # collect results
+ for entry in entries do
+ var line = [entry.to_s]
+ for metric in metrics do
+ if metric.has_element(entry) then
+ line.add(metric[entry].to_s)
+ else
+ line.add("n/a")
+ end
+ end
+ csv.records.add(line)
+ end
+ return csv
+ end