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