-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathjson2tex.py
executable file
·60 lines (52 loc) · 3.73 KB
/
json2tex.py
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
#!/usr/bin/env python3
################################################################################
# json2tex.py #
################################################################################
# #
# Author : Heinz Riener (2016) #
# #
################################################################################
import argparse
import json
import statistics
def slice_log(filename, chunk_size):
data = json.load(open(filename))
num_slices = int((len(data) - 1) / chunk_size)
return [data[i*chunk_size:(i*chunk_size)+chunk_size] for i in range(num_slices)]
def mean(list):
return statistics.mean(list) if len(list) > 0 else 0.0
parser = argparse.ArgumentParser()
parser.add_argument('log', help="Log file in JSON format")
parser.add_argument('-k', help='Maximum k', type=int)
args = parser.parse_args()
data = slice_log(args.log,args.k+1) # max{ k } + 1
num_experiments = len(data)
# for i in range(1,len(data[0])):
# print("===========================================================================")
# print(data[0][0]['command'])
# print('k:',data[0][i]['k'])
# print('#SMT calls: {:8.2f}'.format(mean([data[l][i]['#smt_calls'] for l in range(num_experiments)])))
# print('#restarts: {:8.2f}'.format(mean([data[l][i]['#restarts'] for l in range(num_experiments)])))
# print('#counterexamples: {:8.2f}'.format(mean([data[l][i]['#counterexamples'] for l in range(num_experiments)])))
# print('#parameter candidates: {:8.2f}'.format(mean([data[l][i]['#parameter_candidates'] for l in range(num_experiments)])))
# print('#cex randomizations: {:8.2f}'.format(mean([data[l][i]['#randomizations'] for l in range(num_experiments)])))
#
# print('time[total]: {:8.2f}'.format(mean([data[l][i]['cegis.time'] for l in range(num_experiments)])))
# print('time[param synth]: {:8.2f}'.format(mean([sum(data[l][i]['parameter_synthesis.time']) for l in range(num_experiments)])))
# print('time[correct check]: {:8.2f}'.format(mean([sum(data[l][i]['correctness_check.time']) for l in range(num_experiments)])))
# print('time[cex random]: {:8.2f}'.format(mean([sum(data[l][i]['counterexample_randomization.time']) for l in range(num_experiments)])))
# print('time per param synth: {:8.2f}'.format(mean([mean(data[l][i]['parameter_synthesis.time']) for l in range(num_experiments)])))
# print('time per correct check: {:8.2f}'.format(mean([mean(data[l][i]['correctness_check.time']) for l in range(num_experiments)])))
# print('time per cex random: {:8.2f}'.format(mean([mean(data[l][i]['counterexample_randomization.time']) for l in range(num_experiments)])))
for i in range(1,len(data[0])):
name, ext = data[0][0]['smt'].split('/')[-1:][0].split('.')
num_params = len(data[0][0]['parameter'])
k = data[0][i]['k']
smt_calls = mean([data[l][i]['#smt_calls'] for l in range(num_experiments)])
num_cex = mean([data[l][i]['#counterexamples'] for l in range(num_experiments)])
solution = data[0][i]['solution']
tp = mean([sum(data[l][i]['parameter_synthesis.time']) for l in range(num_experiments)])
tc = mean([sum(data[l][i]['correctness_check.time']) for l in range(num_experiments)])
tr = mean([sum(data[l][i]['counterexample_randomization.time']) for l in range(num_experiments)])
time = mean([data[l][i]['cegis.time'] for l in range(num_experiments)])
print('\\texttt{{{:s}}} & {:d} & {:d} & {:8.2f} & {:8.2f} & {:3s} & {:8.2f} & {:8.2f} & {:8.2f} & {:8.2f}\\\\'.format(name,num_params,k,smt_calls,num_cex,solution,tp,tc,tr,time))