Skip to content

Commit 61105c6

Browse files
marshtompsxdmarshtompsxd
committed
Validate counting information (#5)
Signed-off-by: Xudong Sun <[email protected]>
1 parent de905b3 commit 61105c6

File tree

1 file changed

+85
-107
lines changed

1 file changed

+85
-107
lines changed

‎tools/gen-t1-t2-lines.py

+85-107
Original file line numberDiff line numberDiff line change
@@ -2,156 +2,134 @@
22
import json
33

44

5-
def main():
6-
os.system(
7-
"python3 count-lines.py $VERUS_DIR/source/tools/line_count/zookeeper_table zookeeper"
8-
)
9-
os.system(
10-
"python3 count-lines.py $VERUS_DIR/source/tools/line_count/rabbitmq_table rabbitmq"
11-
)
12-
os.system(
13-
"python3 count-lines.py $VERUS_DIR/source/tools/line_count/fluent_table fluent"
14-
)
5+
def count_total_lines(data):
6+
lines = 0
7+
for key in data:
8+
for inner_key in data[key]:
9+
lines += data[key][inner_key]
10+
return lines
11+
12+
13+
def gen_for_controller(controller):
1514
os.system(
16-
"python3 count-anvil-lines.py $VERUS_DIR/source/tools/line_count/lib_table"
17-
)
18-
zk_data = json.load(open("zookeeper-lines.json"))
19-
rmq_data = json.load(open("rabbitmq-lines.json"))
20-
fb_data = json.load(open("fluent-lines.json"))
21-
anvil_data = json.load(open("anvil-lines.json"))
22-
print("ZooKeeper:")
23-
print(
24-
"Liveness & {} & -- & {}".format(
25-
zk_data["liveness_theorem"]["Trusted"],
26-
zk_data["liveness_proof"]["Proof"],
27-
)
28-
)
29-
print(
30-
"Conformance & 5 & -- & {}".format(
31-
zk_data["reconcile_impl"]["Proof"] - 5,
32-
)
33-
)
34-
print(
35-
"Controller model & -- & -- & {}".format(
36-
zk_data["reconcile_model"]["Proof"],
37-
)
38-
)
39-
print(
40-
"Controller impl & -- & {} & --".format(
41-
zk_data["reconcile_model"]["Exec"] + zk_data["reconcile_impl"]["Exec"],
42-
)
43-
)
44-
print(
45-
"Trusted wrapper & {} & -- & --".format(
46-
zk_data["wrapper"]["Trusted"],
47-
)
48-
)
49-
print(
50-
"Trusted ZooKeeper API & {} & -- & --".format(
51-
zk_data["external_model"]["Trusted"],
52-
)
53-
)
54-
print(
55-
"Trusted entry point & {} & -- & --".format(
56-
zk_data["entry"]["Trusted"],
15+
"python3 count-lines.py $VERUS_DIR/source/tools/line_count/{}_table {}".format(
16+
controller, controller
5717
)
5818
)
19+
data = json.load(open("{}-lines.json".format(controller)))
20+
21+
total_lines = count_total_lines(data)
22+
total_lines -= data["liveness_inv"]["Proof"]
5923

60-
print("RabbitMQ:")
24+
print("{}:".format(controller))
6125
print(
6226
"Liveness & {} & -- & {}".format(
63-
rmq_data["liveness_theorem"]["Trusted"],
64-
rmq_data["liveness_proof"]["Proof"],
27+
data["liveness_theorem"]["Trusted"],
28+
data["liveness_proof"]["Proof"],
6529
)
6630
)
67-
print(
68-
"Safety & {} & -- & {}".format(
69-
rmq_data["safety_theorem"]["Trusted"],
70-
rmq_data["safety_proof"]["Proof"],
31+
total_lines -= data["liveness_theorem"]["Trusted"]
32+
total_lines -= data["liveness_proof"]["Proof"]
33+
34+
if controller == "rabbitmq":
35+
print(
36+
"Safety & {} & -- & {}".format(
37+
data["safety_theorem"]["Trusted"],
38+
data["safety_proof"]["Proof"],
39+
)
40+
)
41+
total_lines -= data["safety_theorem"]["Trusted"]
42+
total_lines -= data["safety_proof"]["Proof"]
43+
44+
if controller == "fluent":
45+
print(
46+
"Conformance & 10 & -- & {}".format(
47+
data["reconcile_impl"]["Proof"] - 10,
48+
)
7149
)
72-
)
73-
print(
74-
"Conformance & 5 & -- & {}".format(
75-
rmq_data["reconcile_impl"]["Proof"] - 5,
50+
else:
51+
print(
52+
"Conformance & 5 & -- & {}".format(
53+
data["reconcile_impl"]["Proof"] - 5,
54+
)
7655
)
77-
)
56+
total_lines -= data["reconcile_impl"]["Proof"]
7857
print(
7958
"Controller model & -- & -- & {}".format(
80-
rmq_data["reconcile_model"]["Proof"],
59+
data["reconcile_model"]["Proof"],
8160
)
8261
)
62+
total_lines -= data["reconcile_model"]["Proof"]
8363
print(
8464
"Controller impl & -- & {} & --".format(
85-
rmq_data["reconcile_model"]["Exec"] + rmq_data["reconcile_impl"]["Exec"],
65+
data["reconcile_model"]["Exec"] + data["reconcile_impl"]["Exec"],
8666
)
8767
)
68+
total_lines -= data["reconcile_model"]["Exec"] + data["reconcile_impl"]["Exec"]
8869
print(
8970
"Trusted wrapper & {} & -- & --".format(
90-
rmq_data["wrapper"]["Trusted"],
71+
data["wrapper"]["Trusted"],
9172
)
9273
)
74+
total_lines -= data["wrapper"]["Trusted"]
75+
if controller == "zookeeper":
76+
print(
77+
"Trusted ZooKeeper API & {} & -- & --".format(
78+
data["external_model"]["Trusted"],
79+
)
80+
)
81+
total_lines -= data["external_model"]["Trusted"]
9382
print(
9483
"Trusted entry point & {} & -- & --".format(
95-
rmq_data["entry"]["Trusted"],
84+
data["entry"]["Trusted"],
9685
)
9786
)
87+
total_lines -= data["entry"]["Trusted"]
88+
print("{} lines are not included".format(total_lines))
9889

99-
print("Fluent:")
100-
print(
101-
"Liveness & {} & -- & {}".format(
102-
fb_data["liveness_theorem"]["Trusted"],
103-
fb_data["liveness_proof"]["Proof"],
104-
)
105-
)
106-
print(
107-
"Conformance & 10 & -- & {}".format(
108-
fb_data["reconcile_impl"]["Proof"] - 10,
109-
)
110-
)
111-
print(
112-
"Controller model & -- & -- & {}".format(
113-
fb_data["reconcile_model"]["Proof"],
114-
)
115-
)
116-
print(
117-
"Controller impl & -- & {} & --".format(
118-
fb_data["reconcile_model"]["Exec"] + fb_data["reconcile_impl"]["Exec"],
119-
)
90+
91+
def main():
92+
gen_for_controller("zookeeper")
93+
gen_for_controller("rabbitmq")
94+
gen_for_controller("fluent")
95+
96+
os.system(
97+
"python3 count-anvil-lines.py $VERUS_DIR/source/tools/line_count/lib_table"
12098
)
99+
anvil_data = json.load(open("anvil-lines.json"))
100+
total_lines = count_total_lines(anvil_data)
101+
total_lines -= anvil_data["test_lines"]["Exec"]
102+
print("Anvil:")
121103
print(
122-
"Trusted wrapper & {} & -- & --".format(
123-
fb_data["wrapper"]["Trusted"],
104+
"Lemmas & -- & -- & {}".format(
105+
anvil_data["k8s_lemma_lines"]["Proof"]
106+
+ anvil_data["tla_lemma_lines"]["Proof"]
124107
)
125108
)
126-
print(
127-
"Trusted entry point & {} & -- & --".format(
128-
fb_data["entry"]["Trusted"],
129-
)
109+
total_lines -= (
110+
anvil_data["k8s_lemma_lines"]["Proof"] + anvil_data["tla_lemma_lines"]["Proof"]
130111
)
131-
print("Anvil:")
132112
print(
133113
"TLA embedding & {} & -- & --".format(
134114
anvil_data["tla_embedding_lines"]["Trusted"]
135115
)
136116
)
117+
total_lines -= anvil_data["tla_embedding_lines"]["Trusted"]
118+
print("Model & {} & -- & --".format(anvil_data["other_lines"]["Trusted"]))
119+
total_lines -= anvil_data["other_lines"]["Trusted"]
137120
print(
138-
"Model & {} & -- & --".format(
139-
anvil_data["other_lines"]["Trusted"]
140-
+ anvil_data["object_model_lines"]["Trusted"]
141-
)
142-
)
143-
print(
144-
"Lemmas & -- & -- & {}".format(
145-
anvil_data["k8s_lemma_lines"]["Proof"]
146-
+ anvil_data["tla_lemma_lines"]["Proof"]
147-
)
121+
"Object view & {} & -- & --".format(anvil_data["object_model_lines"]["Trusted"])
148122
)
123+
total_lines -= anvil_data["object_model_lines"]["Trusted"]
149124
print(
150-
"Shim layer & {} & -- & --".format(
125+
"Object wrapper & {} & -- & --".format(
151126
anvil_data["object_wrapper_lines"]["Trusted"]
152-
+ anvil_data["other_lines"]["Exec"]
153127
)
154128
)
129+
total_lines -= anvil_data["object_wrapper_lines"]["Trusted"]
130+
print("Shim layer & {} & -- & --".format(anvil_data["other_lines"]["Exec"]))
131+
total_lines -= anvil_data["other_lines"]["Exec"]
132+
print("{} lines are not included".format(total_lines))
155133

156134

157135
if __name__ == "__main__":

0 commit comments

Comments
 (0)