]>
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 float(seconds
) + 60 * float(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 with self
.inputs
.formulas
as path
:
42 formulas
= sorted(os
.listdir(path
), key
=natural_key
)
43 shell
.track(self
.outputs
.timing
.path
)
45 for formula
in formulas
:
46 print("Running for %s ..." % formula
)
49 self
.run_solver(os
.path
.join(path
, formula
))
55 class CoolExperiment(SolverExperiment
):
56 inputs
= { 'cool' : GitArchive() }
61 CoolExperiment
.inputs
.update(SolverExperiment
.inputs
)
62 CoolExperiment
.outputs
.update(SolverExperiment
.outputs
)
63 super(CoolExperiment
, self
).__init
__()
66 def build_solver(self
):
67 with self
.inputs
.cool
as path
:
71 def run_solver(self
, formula
):
72 with self
.inputs
.cool
as path
:
73 shell("timeout 1001 ./coalg.native sat KD --verbose < %s" % formula
)
77 class TreeTabExperiment(SolverExperiment
):
78 inputs
= { 'treetab' : TarArchive('ctlProver_r1368.tar') }
83 TreeTabExperiment
.inputs
.update(SolverExperiment
.inputs
)
84 TreeTabExperiment
.outputs
.update(SolverExperiment
.outputs
)
85 super(TreeTabExperiment
, self
).__init
__()
88 def build_solver(self
):
89 with self
.inputs
.treetab
as path
:
93 def run_solver(self
, formula
):
94 with self
.inputs
.treetab
as path
:
95 shell("timeout 1001 ./ctl tree --verbose < %s" % formula
)
98 class GMULExperiment(SolverExperiment
):
99 inputs
= { 'gmul' : TarArchive('ctlgraph.tar') }
104 GMULExperiment
.inputs
.update(SolverExperiment
.inputs
)
105 GMULExperiment
.outputs
.update(SolverExperiment
.outputs
)
106 super(GMULExperiment
, self
).__init
__()
109 def build_solver(self
):
110 with self
.inputs
.gmul
as path
:
114 def run_solver(self
, formula
):
115 with self
.inputs
.gmul
as path
:
116 shell("timeout 1001 ./ctl tr --verbose < %s" % formula
)
119 class ComparisonExperiment(Experiment
):
120 outputs
= { 'cool_data' : CSV_File('cool.csv'),
121 'treetab_data' : CSV_File('treetab.csv'),
122 'gmul_data' : CSV_File('gmul.csv'),
123 'graphs' : Directory('graphs')
125 inputs
= { 'cool' : CoolExperiment(),
126 'treetab' : TreeTabExperiment(),
127 'gmul' : GMULExperiment()
130 def folder_to_csv(self
, folder
, csv
):
131 timings
= sorted(glob
.glob(os
.path
.join(folder
, "shell_*_time")), key
=natural_key
)
132 for timing
in timings
:
133 with
open(timing
) as fd
:
134 lines
= fd
.readlines()
135 command
= list(filter(lambda x
: "Command being timed" in x
, lines
))[0]
136 timeline
= list(filter(lambda x
: "Elapsed (wall clock) time" in x
, lines
))[0]
137 memoryline
= list(filter(lambda x
: "Maximum resident set size" in x
, lines
))[0]
139 command
= command
.split(": ")[1]
140 command
= command
.split("<")[1].strip().strip('"')
141 formula
= os
.path
.basename(command
)
142 time
= parse_timedelta(timeline
.split(": ")[1].strip())
143 time
= time
if time
> 0 else 0.001
144 memory
= memoryline
.split(": ")[1].strip()
145 csv
.append([formula
, time
, memory
])
150 self
.folder_to_csv(self
.inputs
.cool
.timing
.path
, self
.outputs
.cool_data
)
151 self
.folder_to_csv(self
.inputs
.treetab
.timing
.path
, self
.outputs
.treetab_data
)
152 self
.folder_to_csv(self
.inputs
.gmul
.timing
.path
, self
.outputs
.gmul_data
)
154 with self
.outputs
.graphs
as path
:
155 samplecount
= len(self
.outputs
.cool_data
.value
)
157 plt
.title("Time spent: %s" %
158 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
160 plt
.ylabel('time / s')
161 plt
.ylim(0.001, 10000)
162 plt
.xlabel('problem size')
163 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.cool_data
.value
],
164 [x
[1] for x
in self
.outputs
.cool_data
.value
],
166 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.treetab_data
.value
],
167 [x
[1] for x
in self
.outputs
.treetab_data
.value
],
168 'gv', label
="TreeTab")
169 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.gmul_data
.value
],
170 [x
[1] for x
in self
.outputs
.gmul_data
.value
],
174 plt
.savefig('time.svg', format
='svg')
178 plt
.title("Memory usage: %s" %
179 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
181 plt
.ylabel('memory / kB')
182 plt
.xlabel('problem size')
183 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.cool_data
.value
],
184 [x
[2] for x
in self
.outputs
.cool_data
.value
],
186 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.treetab_data
.value
],
187 [x
[2] for x
in self
.outputs
.treetab_data
.value
],
188 'gv', label
="TreeTab")
189 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.gmul_data
.value
],
190 [x
[2] for x
in self
.outputs
.gmul_data
.value
],
194 plt
.savefig('memory.svg', format
='svg')
197 if __name__
== "__main__":
198 parser
= argparse
.ArgumentParser(description
="CTL Experiment runnter", add_help
=False)
199 parser
.add_argument("experiment", choices
=['cool', 'treetab', 'gmul', 'comparison'])
201 local
, unknown
= parser
.parse_known_args()
203 if local
.experiment
== 'cool':
204 experiment
= CoolExperiment()
206 elif local
.experiment
== 'treetab':
207 experiment
= TreeTabExperiment()
209 elif local
.experiment
== 'gmul':
210 experiment
= GMULExperiment()
212 elif local
.experiment
== 'comparison':
213 experiment
= ComparisonExperiment()
215 dirname
= experiment(unknown
)