cool.py

   1 #!/usr/bin/env python3
   2
   3 from versuchung.experiment import Experiment
   4 from versuchung.archives import TarArchive, GitArchive
   5 from versuchung.files import Directory
   6 from versuchung.execute import shell, CommandFailed
   7 from versuchung.files import CSV_File
   8
   9 from matplotlib import pyplot as plt
  10 import matplotlib
  11
  12 import re
  13 import os
  14 import glob
  15 import argparse
  16
  17 def natural_key(string_):
  18     return [int(s) if s.isdigit() else s for s in re.split(r'(\d+)', string_)]
  19
  20 def parse_timedelta(strrep):
  21     minutes, seconds = strrep.split(":")
  22     return float(seconds) + 60 * float(minutes)
  23
  24
  25 class SolverExperiment(Experiment):
  26     inputs = { 'formulas' : TarArchive() }
  27     outputs = { 'timing' : Directory() }
  28
  29
  30     def build_solver(self):
  31         pass
  32
  33
  34     def run_solver(self, formula):
  35         pass
  36
  37
  38     def run(self):
  39         print("Building Solver ...")
  40         self.build_solver()
  41         formulas = sorted(os.listdir(self.inputs.formulas.path), key=natural_key)
  42         shell.track(self.outputs.timing.path)
  43         for formula in formulas:
  44             print("Running for %s ..." % formula)
  45             try:
  46                 self.run_solver(os.path.join(self.inputs.formulas.path, formula))
  47             except CommandFailed:
  48                 break
  49
  50
  51
  52 class CoolExperiment(SolverExperiment):
  53     inputs = { 'cool' : GitArchive() }
  54     outputs = {}
  55
  56
  57     def __init__(self):
  58         CoolExperiment.inputs.update(SolverExperiment.inputs)
  59         CoolExperiment.outputs.update(SolverExperiment.outputs)
  60         super(CoolExperiment, self).__init__()
  61
  62
  63     def build_solver(self):
  64         with self.inputs.cool as path:
  65             shell("make")
  66
  67
  68     def run_solver(self, formula):
  69         with self.inputs.cool as path:
  70             shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula)
  71
  72
  73
  74 class TreeTabExperiment(SolverExperiment):
  75     inputs = { 'treetab' : TarArchive('ctlProver_r1368.tar') }
  76     outputs = {}
  77
  78
  79     def __init__(self):
  80         TreeTabExperiment.inputs.update(SolverExperiment.inputs)
  81         TreeTabExperiment.outputs.update(SolverExperiment.outputs)
  82         super(TreeTabExperiment, self).__init__()
  83
  84
  85     def build_solver(self):
  86         with self.inputs.treetab as path:
  87             shell("make")
  88
  89
  90     def run_solver(self, formula):
  91         with self.inputs.treetab as path:
  92             shell("timeout 1001 ./ctl tree --verbose < %s" % formula)
  93
  94
  95 class GMULExperiment(SolverExperiment):
  96     inputs = { 'gmul' : TarArchive('ctlgraph.tar') }
  97     outputs = {}
  98
  99
 100     def __init__(self):
 101         GMULExperiment.inputs.update(SolverExperiment.inputs)
 102         GMULExperiment.outputs.update(SolverExperiment.outputs)
 103         super(GMULExperiment, self).__init__()
 104
 105
 106     def build_solver(self):
 107         with self.inputs.gmul as path:
 108             shell("make")
 109
 110
 111     def run_solver(self, formula):
 112         with self.inputs.gmul as path:
 113             shell("timeout 1001 ./ctl tr --verbose < %s" % formula)
 114
 115
 116 class ComparisonExperiment(Experiment):
 117     outputs = { 'cool_data' : CSV_File('cool.csv'),
 118                 'treetab_data' : CSV_File('treetab.csv'),
 119                 'gmul_data' : CSV_File('gmul.csv'),
 120                 'graphs' : Directory('graphs')
 121               }
 122     inputs = { 'cool' : CoolExperiment(),
 123                'treetab' : TreeTabExperiment(),
 124                'gmul' : GMULExperiment()
 125              }
 126
 127     def folder_to_csv(self, folder, csv):
 128         timings = sorted(glob.glob(os.path.join(folder, "shell_*_time")), key=natural_key)
 129         for timing in timings:
 130             with open(timing) as fd:
 131                 lines = fd.readlines()
 132                 command = list(filter(lambda x: "Command being timed" in x, lines))[0]
 133                 timeline = list(filter(lambda x: "Elapsed (wall clock) time" in x, lines))[0]
 134                 memoryline = list(filter(lambda x: "Maximum resident set size" in x, lines))[0]
 135
 136                 command = command.split(": ")[1]
 137                 command = command.split("<")[1].strip().strip('"')
 138                 formula = os.path.basename(command)
 139                 time = parse_timedelta(timeline.split(": ")[1].strip())
 140                 time = time if time > 0 else 0.001
 141                 memory = memoryline.split(": ")[1].strip()
 142                 csv.append([formula, time, memory])
 143         csv.flush()
 144
 145
 146     def run(self):
 147         self.folder_to_csv(self.inputs.cool.timing.path, self.outputs.cool_data)
 148         self.folder_to_csv(self.inputs.treetab.timing.path, self.outputs.treetab_data)
 149         self.folder_to_csv(self.inputs.gmul.timing.path, self.outputs.gmul_data)
 150
 151         with self.outputs.graphs as path:
 152             samplecount = len(self.outputs.cool_data.value)
 153             # Time
 154             plt.title("Time spent: %s" %
 155                       os.path.basename(self.inputs.treetab.metadata['formulas']))
 156             plt.yscale('log')
 157             plt.ylabel('time / s')
 158             plt.ylim(0.001, 10000)
 159             plt.xlabel('problem size')
 160             plt.plot([x[0].split('.')[1] for x in self.outputs.cool_data.value],
 161                      [x[1] for x in self.outputs.cool_data.value],
 162                      'bo', label="cool")
 163             plt.plot([x[0].split('.')[1] for x in self.outputs.treetab_data.value],
 164                      [x[1] for x in self.outputs.treetab_data.value],
 165                      'gv', label="TreeTab")
 166             plt.plot([x[0].split('.')[1] for x in self.outputs.gmul_data.value],
 167                      [x[1] for x in self.outputs.gmul_data.value],
 168                      'r*', label="GMUL")
 169
 170             plt.legend(loc=2)
 171             plt.savefig('time.svg', format='svg')
 172             plt.close()
 173
 174             # Memory
 175             plt.title("Memory usage: %s" %
 176                       os.path.basename(self.inputs.treetab.metadata['formulas']))
 177             plt.yscale('log')
 178             plt.ylabel('memory / kB')
 179             plt.xlabel('problem size')
 180             plt.plot([x[0].split('.')[1] for x in self.outputs.cool_data.value],
 181                      [x[2] for x in self.outputs.cool_data.value],
 182                      'bo', label="cool")
 183             plt.plot([x[0].split('.')[1] for x in self.outputs.treetab_data.value],
 184                      [x[2] for x in self.outputs.treetab_data.value],
 185                      'gv', label="TreeTab")
 186             plt.plot([x[0].split('.')[1] for x in self.outputs.gmul_data.value],
 187                      [x[2] for x in self.outputs.gmul_data.value],
 188                      'r*', label="GMUL")
 189
 190             plt.legend(loc=2)
 191             plt.savefig('memory.svg', format='svg')
 192
 193
 194 if __name__ == "__main__":
 195     parser = argparse.ArgumentParser(description="CTL Experiment runnter", add_help=False)
 196     parser.add_argument("experiment", choices=['cool', 'treetab', 'gmul', 'comparison'])
 197
 198     local, unknown = parser.parse_known_args()
 199
 200     if local.experiment == 'cool':
 201         experiment = CoolExperiment()
 202
 203     elif local.experiment == 'treetab':
 204         experiment = TreeTabExperiment()
 205
 206     elif local.experiment == 'gmul':
 207         experiment = GMULExperiment()
 208
 209     elif local.experiment == 'comparison':
 210         experiment = ComparisonExperiment()
 211
 212     dirname = experiment(unknown)
 213     print(dirname)