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):
pass
+
def run_solver(self, formula):
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
+
class CoolExperiment(SolverExperiment):
inputs = { 'cool' : GitArchive() }
outputs = {}
+
def __init__(self):
CoolExperiment.inputs.update(SolverExperiment.inputs)
CoolExperiment.outputs.update(SolverExperiment.outputs)
super(CoolExperiment, self).__init__()
-
+
+
def build_solver(self):
with self.inputs.cool as path:
shell("make")
+
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):
+ 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:
+ 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)
projects / master / cool-versuchung.git / blobdiff