]>
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
7 from versuchung
.files
import CSV_File
9 from matplotlib
import pyplot
as plt
17 def natural_key(string_
):
18 return [int(s
) if s
.isdigit() else s
for s
in re
.split(r
'(\d+)', string_
)]
20 def parse_timedelta(strrep
):
21 minutes
, seconds
= strrep
.split(":")
22 return seconds
+ 60 * minutes
25 class SolverExperiment(Experiment
):
26 inputs
= { 'formulas' : TarArchive() }
27 outputs
= { 'timing' : Directory() }
30 def build_solver(self
):
34 def run_solver(self
, formula
):
39 print("Building Solver ...")
41 formulas
= sorted(os
.listdir(self
.inputs
.formulas
.path
), key
=natural_key
)
42 shell
.track(self
.outputs
.timing
.path
)
43 for formula
in formulas
:
44 print("Running for %s ..." % formula
)
46 self
.run_solver(os
.path
.join(self
.inputs
.formulas
.path
, formula
))
52 class CoolExperiment(SolverExperiment
):
53 inputs
= { 'cool' : GitArchive() }
58 CoolExperiment
.inputs
.update(SolverExperiment
.inputs
)
59 CoolExperiment
.outputs
.update(SolverExperiment
.outputs
)
60 super(CoolExperiment
, self
).__init
__()
63 def build_solver(self
):
64 with self
.inputs
.cool
as path
:
68 def run_solver(self
, formula
):
69 with self
.inputs
.cool
as path
:
70 shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula
)
74 class TreeTabExperiment(SolverExperiment
):
75 inputs
= { 'treetab' : TarArchive('ctlProver_r1368.tar') }
80 TreeTabExperiment
.inputs
.update(SolverExperiment
.inputs
)
81 TreeTabExperiment
.outputs
.update(SolverExperiment
.outputs
)
82 super(TreeTabExperiment
, self
).__init
__()
85 def build_solver(self
):
86 with self
.inputs
.treetab
as path
:
90 def run_solver(self
, formula
):
91 with self
.inputs
.treetab
as path
:
92 shell("timeout 1001 ./ctl tree --verbose < %s" % formula
)
95 class GMULExperiment(SolverExperiment
):
96 inputs
= { 'gmul' : TarArchive('ctlgraph.tar') }
101 GMULExperiment
.inputs
.update(SolverExperiment
.inputs
)
102 GMULExperiment
.outputs
.update(SolverExperiment
.outputs
)
103 super(GMULExperiment
, self
).__init
__()
106 def build_solver(self
):
107 with self
.inputs
.gmul
as path
:
111 def run_solver(self
, formula
):
112 with self
.inputs
.gmul
as path
:
113 shell("timeout 1001 ./ctl tr --verbose < %s" % formula
)
116 class ComparisonExperiment(Experiment
):
117 outputs
= { 'cool_data' : CSV_File('cool.csv'),
118 'treetab_data' : CSV_File('treetab.csv'),
119 'graphs' : Directory('graphs')
121 inputs
= { 'cool' : CoolExperiment(),
122 'treetab' : TreeTabExperiment()
125 def folder_to_csv(self
, folder
, csv
):
126 timings
= sorted(glob
.glob(os
.path
.join(folder
, "shell_*_time")), key
=natural_key
)
127 for timing
in timings
:
128 with
open(timing
) as fd
:
129 lines
= fd
.readlines()
130 command
= list(filter(lambda x
: "Command being timed" in x
, lines
))[0]
131 timeline
= list(filter(lambda x
: "Elapsed (wall clock) time" in x
, lines
))[0]
132 memoryline
= list(filter(lambda x
: "Maximum resident set size" in x
, lines
))[0]
134 command
= command
.split(": ")[1]
135 command
= command
.split("<")[1].strip().strip('"')
136 formula
= os
.path
.basename(command
)
137 time
= parse_timedelta(timeline
.split(": ")[1].strip())
138 memory
= memoryline
.split(": ")[1].strip()
139 csv
.append([formula
, time
, memory
])
144 self
.folder_to_csv(self
.inputs
.cool
.timing
.path
, self
.outputs
.cool_data
)
145 self
.folder_to_csv(self
.inputs
.treetab
.timing
.path
, self
.outputs
.treetab_data
)
147 with self
.outputs
.graphs
as path
:
149 plt
.title("Time spent: %s" %
150 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
152 plt
.ylabel('time / s')
153 plt
.xlabel('problem size')
154 plt
.plot(range(1,21),
155 [x
[1] for x
in self
.outputs
.cool_data
.value
],
157 plt
.plot(range(1,21),
158 [x
[1] for x
in self
.outputs
.treetab_data
.value
],
159 'gv', label
="TreeTab")
161 plt
.savefig('time.svg', format
='svg')
165 plt
.title("Memory usage: %s" %
166 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
168 plt
.ylabel('memory / kB')
169 plt
.xlabel('problem size')
170 plt
.plot(range(1,21),
171 [x
[2] for x
in self
.outputs
.cool_data
.value
],
173 plt
.plot(range(1,21),
174 [x
[2] for x
in self
.outputs
.treetab_data
.value
],
175 'gv', label
="TreeTab")
177 plt
.savefig('memory.svg', format
='svg')
180 if __name__
== "__main__":
181 parser
= argparse
.ArgumentParser(description
="CTL Experiment runnter", add_help
=False)
182 parser
.add_argument("experiment", choices
=['cool', 'treetab', 'gmul', 'comparison'])
184 local
, unknown
= parser
.parse_known_args()
186 if local
.experiment
== 'cool':
187 experiment
= CoolExperiment()
189 elif local
.experiment
== 'treetab':
190 experiment
= TreeTabExperiment()
192 elif local
.experiment
== 'gmul':
193 experiment
= GMULExperiment()
195 elif local
.experiment
== 'comparison':
196 experiment
= ComparisonExperiment()
198 dirname
= experiment(unknown
)