Remove unused variable

[master/cool-versuchung.git] / cool.py

diff --git a/cool.py b/cool.py
old mode 100644 (file)
new mode 100755 (executable)
index 1b96352..63e364d
--- a/cool.py
+++ b/cool.py
@@ -4,58 +4,238 @@ from versuchung.experiment import Experiment
 from versuchung.archives import TarArchive, GitArchive
 from versuchung.files import Directory
 from versuchung.execute import shell, CommandFailed
 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 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 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() }
 class SolverExperiment(Experiment):
     inputs = { 'formulas' : TarArchive() }

-    outputs = { 'timing' : Directory() }
+    outputs = { 'output' : Directory('output'),
+                'timing' : CSV_File('timing.csv') }
+

 
     def build_solver(self):
         pass
 
 
     def build_solver(self):
         pass
 

+

     def run_solver(self, formula):
         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()
     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 = {}
 
 
 
 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 __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 build_solver(self):
         with self.inputs.cool as path:
             shell("make")
 

+

     def run_solver(self, formula):
         with self.inputs.cool as path:
     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__":
 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)
     print(dirname)