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()
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)