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 seconds + 60 * 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                 'graphs' : Directory('graphs')
 120               }
 121     inputs = { 'cool' : CoolExperiment(),
 122                'treetab' : TreeTabExperiment()
 123              }
 124
 125     def folder_to_csv(self, folder, csv):
 126         timings = sorted(glob.glob(os.path.join(folder, "shell_*_time")), key=natural_key)
 127         for timing in timings:
 128             with open(timing) as fd:
 129                 lines = fd.readlines()
 130                 command = list(filter(lambda x: "Command being timed" in x, lines))[0]
 131                 timeline = list(filter(lambda x: "Elapsed (wall clock) time" in x, lines))[0]
 132                 memoryline = list(filter(lambda x: "Maximum resident set size" in x, lines))[0]
 133
 134                 command = command.split(": ")[1]
 135                 command = command.split("<")[1].strip().strip('"')
 136                 formula = os.path.basename(command)
 137                 time = parse_timedelta(timeline.split(": ")[1].strip())
 138                 memory = memoryline.split(": ")[1].strip()
 139                 csv.append([formula, time, memory])
 140         csv.flush()
 141
 142
 143     def run(self):
 144         self.folder_to_csv(self.inputs.cool.timing.path, self.outputs.cool_data)
 145         self.folder_to_csv(self.inputs.treetab.timing.path, self.outputs.treetab_data)
 146
 147         with self.outputs.graphs as path:
 148             # Time
 149             plt.title("Time spent: %s" %
 150                       os.path.basename(self.inputs.treetab.metadata['formulas']))
 151             plt.yscale('log')
 152             plt.ylabel('time / s')
 153             plt.xlabel('problem size')
 154             plt.plot(range(1,21),
 155                      [x[1] for x in self.outputs.cool_data.value],
 156                      'bo', label="cool")
 157             plt.plot(range(1,21),
 158                      [x[1] for x in self.outputs.treetab_data.value],
 159                      'gv', label="TreeTab")
 160             plt.legend()
 161             plt.savefig('time.svg', format='svg')
 162             plt.close()
 163
 164             # Memory
 165             plt.title("Memory usage: %s" %
 166                       os.path.basename(self.inputs.treetab.metadata['formulas']))
 167             plt.yscale('log')
 168             plt.ylabel('memory / kB')
 169             plt.xlabel('problem size')
 170             plt.plot(range(1,21),
 171                      [x[2] for x in self.outputs.cool_data.value],
 172                      'bo', label="cool")
 173             plt.plot(range(1,21),
 174                      [x[2] for x in self.outputs.treetab_data.value],
 175                      'gv', label="TreeTab")
 176             plt.legend()
 177             plt.savefig('memory.svg', format='svg')
 178
 179
 180 if __name__ == "__main__":
 181     parser = argparse.ArgumentParser(description="CTL Experiment runnter", add_help=False)
 182     parser.add_argument("experiment", choices=['cool', 'treetab', 'gmul', 'comparison'])
 183
 184     local, unknown = parser.parse_known_args()
 185
 186     if local.experiment == 'cool':
 187         experiment = CoolExperiment()
 188
 189     elif local.experiment == 'treetab':
 190         experiment = TreeTabExperiment()
 191
 192     elif local.experiment == 'gmul':
 193         experiment = GMULExperiment()
 194
 195     elif local.experiment == 'comparison':
 196         experiment = ComparisonExperiment()
 197
 198     dirname = experiment(unknown)
 199     print(dirname)