X-Git-Url: https://git.siccegge.de//index.cgi?p=master%2Fcool-versuchung.git;a=blobdiff_plain;f=cool.py;h=bab84825db737af92c6e92edb98af3f5fb865b6b;hp=0bfdc15b8beb3e8f7ecc92bab77ce409d7acf4ae;hb=a94ca5b2cb1a6ec23247e81083ad3ed03ade10b6;hpb=7e366195bd15c04e9051659582222dd2c21c50c3 diff --git a/cool.py b/cool.py index 0bfdc15..bab8482 100755 --- a/cool.py +++ b/cool.py @@ -7,6 +7,7 @@ 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_)] @@ -82,9 +83,41 @@ class TreeTabExperiment(SolverExperiment): 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)