add GMUL to ComparisonExperiment

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

diff --git a/cool.py b/cool.py
old mode 100644 (file)
new mode 100755 (executable)
index 1b96352..18ed21d
--- a/cool.py
+++ b/cool.py
@@ -4,23 +4,37 @@ 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

 
 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 seconds + 60 * minutes
+
+

 class SolverExperiment(Experiment):
     inputs = { 'formulas' : TarArchive() }
     outputs = { 'timing' : Directory() }
 
 class SolverExperiment(Experiment):
     inputs = { 'formulas' : TarArchive() }
     outputs = { 'timing' : Directory() }
 

+

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

+

     def run_solver(self, formula):
         pass
     def run_solver(self, formula):
         pass

-    
+
+

     def run(self):
         print("Building Solver ...")
         self.build_solver()
     def run(self):
         print("Building Solver ...")
         self.build_solver()


@@ -34,28 +48,164 @@ class SolverExperiment(Experiment):
                 break
 
 
                 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:
             shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula)
     def run_solver(self, formula):
         with self.inputs.cool as path:
             shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula)

-            
-                
-            
+
+
+
+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:
+            shell("timeout 1001 ./ctl tree --verbose < %s" % formula)
+
+
+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:
+            shell("timeout 1001 ./ctl tr --verbose < %s" % formula)
+
+
+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())
+                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:
+            samplecount = len(self.outputs.cool_data.value)
+            # Time
+            plt.title("Time spent: %s" %
+                      os.path.basename(self.inputs.treetab.metadata['formulas']))
+            plt.yscale('log')
+            plt.ylabel('time / s')
+            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.legend()
+            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.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.legend()
+            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.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)