X-Git-Url: https://git.siccegge.de//index.cgi?p=master%2Fcool-versuchung.git;a=blobdiff_plain;f=cool.py;h=bab84825db737af92c6e92edb98af3f5fb865b6b;hp=1b9635262d3f451e8afee21c9525ab28bc7b4202;hb=a94ca5b2cb1a6ec23247e81083ad3ed03ade10b6;hpb=904011dd5f3b054052c745fb157aeaa752d7fa1f

diff --git a/cool.py b/cool.py
old mode 100644
new mode 100755
index 1b96352..bab8482
--- a/cool.py
+++ b/cool.py
@@ -7,20 +7,25 @@ from versuchung.execute import shell, CommandFailed
 
 import re
 import os
+import argparse
 
 def natural_key(string_):
     return [int(s) if s.isdigit() else s for s in re.split(r'(\d+)', string_)]
 
+
 class SolverExperiment(Experiment):
     inputs = { 'formulas' : TarArchive() }
     outputs = { 'timing' : Directory() }
 
+
     def build_solver(self):
         pass
 
+
     def run_solver(self, formula):
         pass
-    
+
+
     def run(self):
         print("Building Solver ...")
         self.build_solver()
@@ -34,28 +39,85 @@ class SolverExperiment(Experiment):
                 break
 
 
+
 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 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)
-            
-                
-            
+
+
+
+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)
+
+
 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()
 
+    dirname = experiment(unknown)
     print(dirname)