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