]>
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
18 def natural_key(string_
):
19 return [int(s
) if s
.isdigit() else s
for s
in re
.split(r
'(\d+)', string_
)]
21 def parse_timedelta(strrep
):
22 minutes
, seconds
= strrep
.split(":")
23 return float(seconds
) + 60 * float(minutes
)
26 class SolverExperiment(Experiment
):
27 inputs
= { 'formulas' : TarArchive() }
28 outputs
= { 'output' : Directory('output'),
29 'timing' : CSV_File('timing.csv') }
32 def build_solver(self
):
36 def run_solver(self
, formula
):
40 def execute_timed(self
, formula
, command
, **kwargs
):
41 with self
.outputs
.output
as directory
:
42 with
open(os
.path
.join(directory
, '%s_stdout' % formula
), 'w') as stdoutfd
:
43 with
open(os
.path
.join(directory
, '%s_stderr' % formula
), 'w') as stderrfd
:
44 p
= subprocess
.Popen(command
, stdout
=stdoutfd
, stderr
=stderrfd
, **kwargs
)
45 _pid
, ret
, ru
= os
.wait4(p
.pid
, 0)
49 raise CommandFailed(command
, ret
)
51 self
.outputs
.timing
.append([formula
, ru
.ru_utime
, ru
.ru_maxrss
])
56 print("Building Solver ...")
58 with self
.inputs
.formulas
as path
:
59 formulas
= sorted(os
.listdir(path
), key
=natural_key
)
61 for formula
in formulas
:
62 print("Running for %s ..." % formula
)
64 self
.run_solver(os
.path
.join(path
, formula
))
70 class CoolExperiment(SolverExperiment
):
71 inputs
= { 'cool' : GitArchive() }
76 CoolExperiment
.inputs
.update(SolverExperiment
.inputs
)
77 CoolExperiment
.outputs
.update(SolverExperiment
.outputs
)
78 super(CoolExperiment
, self
).__init
__()
81 def build_solver(self
):
82 with self
.inputs
.cool
as path
:
86 def run_solver(self
, formula
):
87 with self
.inputs
.cool
as path
:
88 executable
= os
.path
.join(path
, 'coalg.native')
89 self
.execute_timed(os
.path
.basename(formula
),
90 "timeout 1000 %s sat KD --verbose < %s"
91 % (executable
, formula
),
95 class TreeTabExperiment(SolverExperiment
):
96 inputs
= { 'treetab' : TarArchive('ctlProver_r1368.tar') }
101 TreeTabExperiment
.inputs
.update(SolverExperiment
.inputs
)
102 TreeTabExperiment
.outputs
.update(SolverExperiment
.outputs
)
103 super(TreeTabExperiment
, self
).__init
__()
106 def build_solver(self
):
107 with self
.inputs
.treetab
as path
:
111 def run_solver(self
, formula
):
112 with self
.inputs
.treetab
as path
:
113 executable
= os
.path
.join(path
, 'ctl')
114 self
.execute_timed(os
.path
.basename(formula
),
115 "timeout 1001 %s tree --verbose < %s"
116 % (executable
, formula
),
120 class GMULExperiment(SolverExperiment
):
121 inputs
= { 'gmul' : TarArchive('ctlgraph.tar') }
126 GMULExperiment
.inputs
.update(SolverExperiment
.inputs
)
127 GMULExperiment
.outputs
.update(SolverExperiment
.outputs
)
128 super(GMULExperiment
, self
).__init
__()
131 def build_solver(self
):
132 with self
.inputs
.gmul
as path
:
136 def run_solver(self
, formula
):
137 with self
.inputs
.gmul
as path
:
138 executable
= os
.path
.join(path
, 'ctl')
139 self
.execute_timed(os
.path
.basename(formula
),
140 "timeout 1001 %s tr --verbose < %s"
141 % (executable
, formula
),
145 class ComparisonExperiment(Experiment
):
146 outputs
= { 'cool_data' : CSV_File('cool.csv'),
147 'treetab_data' : CSV_File('treetab.csv'),
148 'gmul_data' : CSV_File('gmul.csv'),
149 'graphs' : Directory('graphs')
151 inputs
= { 'cool' : CoolExperiment(),
152 'treetab' : TreeTabExperiment(),
153 'gmul' : GMULExperiment()
156 def folder_to_csv(self
, folder
, csv
):
157 timings
= sorted(glob
.glob(os
.path
.join(folder
, "shell_*_time")), key
=natural_key
)
158 for timing
in timings
:
159 with
open(timing
) as fd
:
160 lines
= fd
.readlines()
161 command
= list(filter(lambda x
: "Command being timed" in x
, lines
))[0]
162 timeline
= list(filter(lambda x
: "Elapsed (wall clock) time" in x
, lines
))[0]
163 memoryline
= list(filter(lambda x
: "Maximum resident set size" in x
, lines
))[0]
165 command
= command
.split(": ")[1]
166 command
= command
.split("<")[1].strip().strip('"')
167 formula
= os
.path
.basename(command
)
168 time
= parse_timedelta(timeline
.split(": ")[1].strip())
169 time
= time
if time
> 0 else 0.001
170 memory
= memoryline
.split(": ")[1].strip()
171 csv
.append([formula
, time
, memory
])
176 self
.folder_to_csv(self
.inputs
.cool
.timing
.path
, self
.outputs
.cool_data
)
177 self
.folder_to_csv(self
.inputs
.treetab
.timing
.path
, self
.outputs
.treetab_data
)
178 self
.folder_to_csv(self
.inputs
.gmul
.timing
.path
, self
.outputs
.gmul_data
)
180 with self
.outputs
.graphs
as path
:
181 samplecount
= len(self
.outputs
.cool_data
.value
)
183 plt
.title("Time spent: %s" %
184 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
186 plt
.ylabel('time / s')
187 plt
.ylim(0.001, 10000)
188 plt
.xlabel('problem size')
189 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.cool_data
.value
],
190 [x
[1] for x
in self
.outputs
.cool_data
.value
],
192 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.treetab_data
.value
],
193 [x
[1] for x
in self
.outputs
.treetab_data
.value
],
194 'gv', label
="TreeTab")
195 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.gmul_data
.value
],
196 [x
[1] for x
in self
.outputs
.gmul_data
.value
],
200 plt
.savefig('time.svg', format
='svg')
204 plt
.title("Memory usage: %s" %
205 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
207 plt
.ylabel('memory / kB')
208 plt
.xlabel('problem size')
209 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.cool_data
.value
],
210 [x
[2] for x
in self
.outputs
.cool_data
.value
],
212 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.treetab_data
.value
],
213 [x
[2] for x
in self
.outputs
.treetab_data
.value
],
214 'gv', label
="TreeTab")
215 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.gmul_data
.value
],
216 [x
[2] for x
in self
.outputs
.gmul_data
.value
],
220 plt
.savefig('memory.svg', format
='svg')
223 if __name__
== "__main__":
224 parser
= argparse
.ArgumentParser(description
="CTL Experiment runnter", add_help
=False)
225 parser
.add_argument("experiment", choices
=['cool', 'treetab', 'gmul', 'comparison'])
227 local
, unknown
= parser
.parse_known_args()
229 if local
.experiment
== 'cool':
230 experiment
= CoolExperiment()
232 elif local
.experiment
== 'treetab':
233 experiment
= TreeTabExperiment()
235 elif local
.experiment
== 'gmul':
236 experiment
= GMULExperiment()
238 elif local
.experiment
== 'comparison':
239 experiment
= ComparisonExperiment()
241 dirname
= experiment(unknown
)