Remove unused variable

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

diff --git a/cool.py b/cool.py
index d6b400cc873677a773ffc733839d44c352edabb8..63e364d18e73506968f2bc8021afaa25ddc42f22 100755 (executable)
--- a/cool.py
+++ b/cool.py
@@ -4,17 +4,29 @@ 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):
 
 
     def build_solver(self):


@@ -25,17 +37,33 @@ class SolverExperiment(Experiment):
         pass
 
 
         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

 
 
 
 
 
 


@@ -57,13 +85,157 @@ class CoolExperiment(SolverExperiment):
 
     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)