]>
git.siccegge.de Git - master/cool-versuchung.git/blob - cool.py
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
12 def natural_key(string_
):
13 return [int(s
) if s
.isdigit() else s
for s
in re
.split(r
'(\d+)', string_
)]
16 class SolverExperiment(Experiment
):
17 inputs
= { 'formulas' : TarArchive() }
18 outputs
= { 'timing' : Directory() }
21 def build_solver(self
):
25 def run_solver(self
, formula
):
30 print("Building 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
)
37 self
.run_solver(os
.path
.join(self
.inputs
.formulas
.path
, formula
))
43 class CoolExperiment(SolverExperiment
):
44 inputs
= { 'cool' : GitArchive() }
49 CoolExperiment
.inputs
.update(SolverExperiment
.inputs
)
50 CoolExperiment
.outputs
.update(SolverExperiment
.outputs
)
51 super(CoolExperiment
, self
).__init
__()
54 def build_solver(self
):
55 with self
.inputs
.cool
as path
:
59 def run_solver(self
, formula
):
60 with self
.inputs
.cool
as path
:
61 shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula
)
65 class TreeTabExperiment(SolverExperiment
):
66 inputs
= { 'treetab' : TarArchive('ctlProver_r1368.tar') }
71 TreeTabExperiment
.inputs
.update(SolverExperiment
.inputs
)
72 TreeTabExperiment
.outputs
.update(SolverExperiment
.outputs
)
73 super(TreeTabExperiment
, self
).__init
__()
76 def build_solver(self
):
77 with self
.inputs
.treetab
as path
:
81 def run_solver(self
, formula
):
82 with self
.inputs
.treetab
as path
:
83 shell("timeout 1001 ./ctl tree --verbose < %s" % formula
)
86 class GMULExperiment(SolverExperiment
):
87 inputs
= { 'gmul' : TarArchive('ctlgraph.tar') }
92 GMULExperiment
.inputs
.update(SolverExperiment
.inputs
)
93 GMULExperiment
.outputs
.update(SolverExperiment
.outputs
)
94 super(GMULExperiment
, self
).__init
__()
97 def build_solver(self
):
98 with self
.inputs
.gmul
as path
:
102 def run_solver(self
, formula
):
103 with self
.inputs
.gmul
as path
:
104 shell("timeout 1001 ./ctl tr --verbose < %s" % formula
)
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'])
111 local
, unknown
= parser
.parse_known_args()
113 if local
.experiment
== 'cool':
114 experiment
= CoolExperiment()
116 elif local
.experiment
== 'treetab':
117 experiment
= TreeTabExperiment()
119 elif local
.experiment
== 'gmul':
120 experiment
= GMULExperiment()
122 dirname
= experiment(unknown
)