]>
git.siccegge.de Git - master/cool-versuchung.git/blob - cool.py
18ed21d850bbddce0139ca8ab8276f2d253ffc67
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 'gmul_data' : CSV_File('gmul.csv'),
120 'graphs' : Directory('graphs')
122 inputs
= { 'cool' : CoolExperiment(),
123 'treetab' : TreeTabExperiment(),
124 'gmul' : GMULExperiment()
127 def folder_to_csv(self
, folder
, csv
):
128 timings
= sorted(glob
.glob(os
.path
.join(folder
, "shell_*_time")), key
=natural_key
)
129 for timing
in timings
:
130 with
open(timing
) as fd
:
131 lines
= fd
.readlines()
132 command
= list(filter(lambda x
: "Command being timed" in x
, lines
))[0]
133 timeline
= list(filter(lambda x
: "Elapsed (wall clock) time" in x
, lines
))[0]
134 memoryline
= list(filter(lambda x
: "Maximum resident set size" in x
, lines
))[0]
136 command
= command
.split(": ")[1]
137 command
= command
.split("<")[1].strip().strip('"')
138 formula
= os
.path
.basename(command
)
139 time
= parse_timedelta(timeline
.split(": ")[1].strip())
140 memory
= memoryline
.split(": ")[1].strip()
141 csv
.append([formula
, time
, memory
])
146 self
.folder_to_csv(self
.inputs
.cool
.timing
.path
, self
.outputs
.cool_data
)
147 self
.folder_to_csv(self
.inputs
.treetab
.timing
.path
, self
.outputs
.treetab_data
)
148 self
.folder_to_csv(self
.inputs
.gmul
.timing
.path
, self
.outputs
.gmul_data
)
150 with self
.outputs
.graphs
as path
:
151 samplecount
= len(self
.outputs
.cool_data
.value
)
153 plt
.title("Time spent: %s" %
154 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
156 plt
.ylabel('time / s')
157 plt
.xlabel('problem size')
158 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.cool_data
.value
],
159 [x
[1] for x
in self
.outputs
.cool_data
.value
],
161 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.treetab_data
.value
],
162 [x
[1] for x
in self
.outputs
.treetab_data
.value
],
163 'gv', label
="TreeTab")
165 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.gmul_data
.value
],
166 [x
[1] for x
in self
.outputs
.gmul_data
.value
],
169 plt
.savefig('time.svg', format
='svg')
173 plt
.title("Memory usage: %s" %
174 os
.path
.basename(self
.inputs
.treetab
.metadata
['formulas']))
176 plt
.ylabel('memory / kB')
177 plt
.xlabel('problem size')
178 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.cool_data
.value
],
179 [x
[2] for x
in self
.outputs
.cool_data
.value
],
181 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.treetab_data
.value
],
182 [x
[2] for x
in self
.outputs
.treetab_data
.value
],
183 'gv', label
="TreeTab")
185 plt
.plot([x
[0].split('.')[1] for x
in self
.outputs
.gmul_data
.value
],
186 [x
[2] for x
in self
.outputs
.gmul_data
.value
],
189 plt
.savefig('memory.svg', format
='svg')
192 if __name__
== "__main__":
193 parser
= argparse
.ArgumentParser(description
="CTL Experiment runnter", add_help
=False)
194 parser
.add_argument("experiment", choices
=['cool', 'treetab', 'gmul', 'comparison'])
196 local
, unknown
= parser
.parse_known_args()
198 if local
.experiment
== 'cool':
199 experiment
= CoolExperiment()
201 elif local
.experiment
== 'treetab':
202 experiment
= TreeTabExperiment()
204 elif local
.experiment
== 'gmul':
205 experiment
= GMULExperiment()
207 elif local
.experiment
== 'comparison':
208 experiment
= ComparisonExperiment()
210 dirname
= experiment(unknown
)