from versuchung.archives import TarArchive, GitArchive
from versuchung.files import Directory
from versuchung.execute import shell, CommandFailed
+from versuchung.files import CSV_File
+
+from matplotlib import pyplot as plt
+import matplotlib
import re
import os
+import glob
import argparse
def natural_key(string_):
return [int(s) if s.isdigit() else s for s in re.split(r'(\d+)', string_)]
+def parse_timedelta(strrep):
+ minutes, seconds = strrep.split(":")
+ return seconds + 60 * minutes
+
class SolverExperiment(Experiment):
inputs = { 'formulas' : TarArchive() }
shell("timeout 1001 ./ctl tr --verbose < %s" % formula)
+class ComparisonExperiment(Experiment):
+ outputs = { 'cool_data' : CSV_File('cool.csv'),
+ 'treetab_data' : CSV_File('treetab.csv'),
+ 'graphs' : Directory('graphs')
+ }
+ inputs = { 'cool' : CoolExperiment(),
+ 'treetab' : TreeTabExperiment()
+ }
+
+ def folder_to_csv(self, folder, csv):
+ timings = sorted(glob.glob(os.path.join(folder, "shell_*_time")), key=natural_key)
+ for timing in timings:
+ with open(timing) as fd:
+ lines = fd.readlines()
+ command = list(filter(lambda x: "Command being timed" in x, lines))[0]
+ timeline = list(filter(lambda x: "Elapsed (wall clock) time" in x, lines))[0]
+ memoryline = list(filter(lambda x: "Maximum resident set size" in x, lines))[0]
+
+ command = command.split(": ")[1]
+ command = command.split("<")[1].strip().strip('"')
+ formula = os.path.basename(command)
+ time = parse_timedelta(timeline.split(": ")[1].strip())
+ memory = memoryline.split(": ")[1].strip()
+ csv.append([formula, time, memory])
+ csv.flush()
+
+
+ def run(self):
+ self.folder_to_csv(self.inputs.cool.timing.path, self.outputs.cool_data)
+ self.folder_to_csv(self.inputs.treetab.timing.path, self.outputs.treetab_data)
+
+ with self.outputs.graphs as path:
+ # Time
+ plt.title("Time spent: %s" %
+ os.path.basename(self.inputs.treetab.metadata['formulas']))
+ plt.yscale('log')
+ plt.ylabel('time / s')
+ plt.xlabel('problem size')
+ plt.plot(range(1,21),
+ [x[1] for x in self.outputs.cool_data.value],
+ 'bo', label="cool")
+ plt.plot(range(1,21),
+ [x[1] for x in self.outputs.treetab_data.value],
+ 'gv', label="TreeTab")
+ plt.legend()
+ plt.savefig('time.svg', format='svg')
+ plt.close()
+
+ # Memory
+ plt.title("Memory usage: %s" %
+ os.path.basename(self.inputs.treetab.metadata['formulas']))
+ plt.yscale('log')
+ plt.ylabel('memory / kB')
+ plt.xlabel('problem size')
+ plt.plot(range(1,21),
+ [x[2] for x in self.outputs.cool_data.value],
+ 'bo', label="cool")
+ plt.plot(range(1,21),
+ [x[2] for x in self.outputs.treetab_data.value],
+ 'gv', label="TreeTab")
+ plt.legend()
+ plt.savefig('memory.svg', format='svg')
+
+
if __name__ == "__main__":
parser = argparse.ArgumentParser(description="CTL Experiment runnter", add_help=False)
parser.add_argument("experiment", choices=['cool', 'treetab', 'gmul', 'comparison'])
elif local.experiment == 'gmul':
experiment = GMULExperiment()
+ elif local.experiment == 'comparison':
+ experiment = ComparisonExperiment()
+
dirname = experiment(unknown)
print(dirname)