cool.py

   1 #!/usr/bin/env python3
   2
   3 from versuchung.experiment import Experiment
   4 from versuchung.archives import TarArchive, GitArchive
   5 from versuchung.files import Directory
   6 from versuchung.execute import shell, CommandFailed
   7
   8 import re
   9 import os
  10 import argparse
  11
  12 def natural_key(string_):
  13     return [int(s) if s.isdigit() else s for s in re.split(r'(\d+)', string_)]
  14
  15
  16 class SolverExperiment(Experiment):
  17     inputs = { 'formulas' : TarArchive() }
  18     outputs = { 'timing' : Directory() }
  19
  20
  21     def build_solver(self):
  22         pass
  23
  24
  25     def run_solver(self, formula):
  26         pass
  27
  28
  29     def run(self):
  30         print("Building Solver ...")
  31         self.build_solver()
  32         formulas = sorted(os.listdir(self.inputs.formulas.path), key=natural_key)
  33         shell.track(self.outputs.timing.path)
  34         for formula in formulas:
  35             print("Running for %s ..." % formula)
  36             try:
  37                 self.run_solver(os.path.join(self.inputs.formulas.path, formula))
  38             except CommandFailed:
  39                 break
  40
  41
  42
  43 class CoolExperiment(SolverExperiment):
  44     inputs = { 'cool' : GitArchive() }
  45     outputs = {}
  46
  47
  48     def __init__(self):
  49         CoolExperiment.inputs.update(SolverExperiment.inputs)
  50         CoolExperiment.outputs.update(SolverExperiment.outputs)
  51         super(CoolExperiment, self).__init__()
  52
  53
  54     def build_solver(self):
  55         with self.inputs.cool as path:
  56             shell("make")
  57
  58
  59     def run_solver(self, formula):
  60         with self.inputs.cool as path:
  61             shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula)
  62
  63
  64
  65 class TreeTabExperiment(SolverExperiment):
  66     inputs = { 'treetab' : TarArchive('ctlProver_r1368.tar') }
  67     outputs = {}
  68
  69
  70     def __init__(self):
  71         TreeTabExperiment.inputs.update(SolverExperiment.inputs)
  72         TreeTabExperiment.outputs.update(SolverExperiment.outputs)
  73         super(TreeTabExperiment, self).__init__()
  74
  75
  76     def build_solver(self):
  77         with self.inputs.treetab as path:
  78             shell("make")
  79
  80
  81     def run_solver(self, formula):
  82         with self.inputs.treetab as path:
  83             shell("timeout 1001 ./ctl tree --verbose < %s" % formula)
  84
  85
  86 class GMULExperiment(SolverExperiment):
  87     inputs = { 'gmul' : TarArchive('ctlgraph.tar') }
  88     outputs = {}
  89
  90
  91     def __init__(self):
  92         GMULExperiment.inputs.update(SolverExperiment.inputs)
  93         GMULExperiment.outputs.update(SolverExperiment.outputs)
  94         super(GMULExperiment, self).__init__()
  95
  96
  97     def build_solver(self):
  98         with self.inputs.gmul as path:
  99             shell("make")
 100
 101
 102     def run_solver(self, formula):
 103         with self.inputs.gmul as path:
 104             shell("timeout 1001 ./ctl tr --verbose < %s" % formula)
 105
 106
 107 if __name__ == "__main__":
 108     parser = argparse.ArgumentParser(description="CTL Experiment runnter", add_help=False)
 109     parser.add_argument("experiment", choices=['cool', 'treetab', 'gmul', 'comparison'])
 110
 111     local, unknown = parser.parse_known_args()
 112
 113     if local.experiment == 'cool':
 114         experiment = CoolExperiment()
 115
 116     elif local.experiment == 'treetab':
 117         experiment = TreeTabExperiment()
 118
 119     elif local.experiment == 'gmul':
 120         experiment = GMULExperiment()
 121
 122     dirname = experiment(unknown)
 123     print(dirname)