X-Git-Url: https://git.siccegge.de//index.cgi?p=master%2Fcool-versuchung.git;a=blobdiff_plain;f=cool.py;h=63e364d18e73506968f2bc8021afaa25ddc42f22;hp=0bfdc15b8beb3e8f7ecc92bab77ce409d7acf4ae;hb=92ab77e199ac18da7119b164f9715e08a19af385;hpb=7e366195bd15c04e9051659582222dd2c21c50c3 diff --git a/cool.py b/cool.py index 0bfdc15..63e364d 100755 --- a/cool.py +++ b/cool.py @@ -4,17 +4,29 @@ 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 +import subprocess 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 float(seconds) + 60 * float(minutes) + class SolverExperiment(Experiment): inputs = { 'formulas' : TarArchive() } - outputs = { 'timing' : Directory() } + outputs = { 'output' : Directory('output'), + 'timing' : CSV_File('timing.csv') } def build_solver(self): @@ -25,17 +37,33 @@ class SolverExperiment(Experiment): pass + def execute_timed(self, formula, command, **kwargs): + with self.outputs.output as directory: + with open(os.path.join(directory, '%s_stdout' % formula), 'w') as stdoutfd: + with open(os.path.join(directory, '%s_stderr' % formula), 'w') as stderrfd: + p = subprocess.Popen(command, stdout=stdoutfd, stderr=stderrfd, **kwargs) + _pid, ret, ru = os.wait4(p.pid, 0) + p.wait() + + if ret != 0: + raise CommandFailed(command, ret) + + self.outputs.timing.append([formula, ru.ru_utime, ru.ru_maxrss]) + return ret + + def run(self): print("Building Solver ...") self.build_solver() - formulas = sorted(os.listdir(self.inputs.formulas.path), key=natural_key) - shell.track(self.outputs.timing.path) - for formula in formulas: - print("Running for %s ..." % formula) - try: - self.run_solver(os.path.join(self.inputs.formulas.path, formula)) - except CommandFailed: - break + with self.inputs.formulas as path: + formulas = sorted(os.listdir(path), key=natural_key) + + for formula in formulas: + print("Running for %s ..." % formula) + try: + self.run_solver(os.path.join(path, formula)) + except CommandFailed: + break @@ -57,8 +85,11 @@ class CoolExperiment(SolverExperiment): def run_solver(self, formula): with self.inputs.cool as path: - shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula) - + executable = os.path.join(path, 'coalg.native') + self.execute_timed(os.path.basename(formula), + "timeout 1000 %s sat KD --verbose < %s" + % (executable, formula), + shell=True) class TreeTabExperiment(SolverExperiment): @@ -79,12 +110,132 @@ class TreeTabExperiment(SolverExperiment): def run_solver(self, formula): with self.inputs.treetab as path: - shell("timeout 1001 ./ctl tree --verbose < %s" % formula) + executable = os.path.join(path, 'ctl') + self.execute_timed(os.path.basename(formula), + "timeout 1001 %s tree --verbose < %s" + % (executable, formula), + shell=True) + + +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: + executable = os.path.join(path, 'ctl') + self.execute_timed(os.path.basename(formula), + "timeout 1001 %s tr --verbose < %s" + % (executable, formula), + shell=True) + + +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()) + time = time if time > 0 else 0.001 + 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: + # Time + plt.title("Time spent: %s" % + os.path.basename(self.inputs.treetab.metadata['formulas'])) + plt.yscale('log') + plt.ylabel('time / s') + plt.ylim(0.001, 10000) + 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.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.legend(loc=2) + 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.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.legend(loc=2) + 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)