X-Git-Url: https://git.siccegge.de//index.cgi?p=master%2Fcool-versuchung.git;a=blobdiff_plain;f=cool.py;h=18ed21d850bbddce0139ca8ab8276f2d253ffc67;hp=d6b400cc873677a773ffc733839d44c352edabb8;hb=0d5c7d931d1b5a5cb8a758ffb433726c930f4e4d;hpb=7dd24bbce0f1e7d103e95ac90a6b43e69afc646a diff --git a/cool.py b/cool.py index d6b400c..18ed21d 100755 --- a/cool.py +++ b/cool.py @@ -4,13 +4,23 @@ from versuchung.experiment import Experiment 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() } @@ -61,9 +71,141 @@ class CoolExperiment(SolverExperiment): +class TreeTabExperiment(SolverExperiment): + inputs = { 'treetab' : TarArchive('ctlProver_r1368.tar') } + outputs = {} + + + def __init__(self): + TreeTabExperiment.inputs.update(SolverExperiment.inputs) + TreeTabExperiment.outputs.update(SolverExperiment.outputs) + super(TreeTabExperiment, self).__init__() + + + def build_solver(self): + with self.inputs.treetab as path: + shell("make") + + + def run_solver(self, formula): + with self.inputs.treetab as path: + shell("timeout 1001 ./ctl tree --verbose < %s" % formula) + + +class GMULExperiment(SolverExperiment): + inputs = { 'gmul' : TarArchive('ctlgraph.tar') } + outputs = {} + + + def __init__(self): + GMULExperiment.inputs.update(SolverExperiment.inputs) + GMULExperiment.outputs.update(SolverExperiment.outputs) + super(GMULExperiment, self).__init__() + + + def build_solver(self): + with self.inputs.gmul as path: + shell("make") + + + def run_solver(self, formula): + with self.inputs.gmul as path: + shell("timeout 1001 ./ctl tr --verbose < %s" % formula) + + +class ComparisonExperiment(Experiment): + outputs = { 'cool_data' : CSV_File('cool.csv'), + 'treetab_data' : CSV_File('treetab.csv'), + 'gmul_data' : CSV_File('gmul.csv'), + 'graphs' : Directory('graphs') + } + inputs = { 'cool' : CoolExperiment(), + 'treetab' : TreeTabExperiment(), + 'gmul' : GMULExperiment() + } + + 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) + self.folder_to_csv(self.inputs.gmul.timing.path, self.outputs.gmul_data) + + with self.outputs.graphs as path: + samplecount = len(self.outputs.cool_data.value) + # 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([x[0].split('.')[1] for x in self.outputs.cool_data.value], + [x[1] for x in self.outputs.cool_data.value], + 'bo', label="cool") + plt.plot([x[0].split('.')[1] for x in self.outputs.treetab_data.value], + [x[1] for x in self.outputs.treetab_data.value], + 'gv', label="TreeTab") + plt.legend() + plt.plot([x[0].split('.')[1] for x in self.outputs.gmul_data.value], + [x[1] for x in self.outputs.gmul_data.value], + 'r*', label="GMUL") + + 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([x[0].split('.')[1] for x in self.outputs.cool_data.value], + [x[2] for x in self.outputs.cool_data.value], + 'bo', label="cool") + plt.plot([x[0].split('.')[1] for x in self.outputs.treetab_data.value], + [x[2] for x in self.outputs.treetab_data.value], + 'gv', label="TreeTab") + plt.legend() + plt.plot([x[0].split('.')[1] for x in self.outputs.gmul_data.value], + [x[2] for x in self.outputs.gmul_data.value], + 'r*', label="GMUL") + + plt.savefig('memory.svg', format='svg') + + if __name__ == "__main__": - import sys - experiment = CoolExperiment() - dirname = experiment(sys.argv) + parser = argparse.ArgumentParser(description="CTL Experiment runnter", add_help=False) + parser.add_argument("experiment", choices=['cool', 'treetab', 'gmul', 'comparison']) + + local, unknown = parser.parse_known_args() + + if local.experiment == 'cool': + experiment = CoolExperiment() + + elif local.experiment == 'treetab': + experiment = TreeTabExperiment() + + elif local.experiment == 'gmul': + experiment = GMULExperiment() + + elif local.experiment == 'comparison': + experiment = ComparisonExperiment() + dirname = experiment(unknown) print(dirname)