From 5aaf901f1796cf4d994dd03313a16c4a41a263d4 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Mon, 4 Dec 2023 20:51:11 -0600 Subject: [PATCH 1/2] Push-button and then get table Signed-off-by: Xudong Sun --- tools/{gen-table2.py => gen-t1-t2-lines.py} | 0 tools/gen-t1-t2-time.py | 45 +++++++++++++++++++++ 2 files changed, 45 insertions(+) rename tools/{gen-table2.py => gen-t1-t2-lines.py} (100%) create mode 100644 tools/gen-t1-t2-time.py diff --git a/tools/gen-table2.py b/tools/gen-t1-t2-lines.py similarity index 100% rename from tools/gen-table2.py rename to tools/gen-t1-t2-lines.py diff --git a/tools/gen-t1-t2-time.py b/tools/gen-t1-t2-time.py new file mode 100644 index 000000000..201482f4f --- /dev/null +++ b/tools/gen-t1-t2-time.py @@ -0,0 +1,45 @@ +import os +import json + + +def main(): + os.system("python3 count-time.py zookeeper.json zookeeper") + os.system("python3 count-time.py rabbitmq.json rabbitmq") + os.system("python3 count-time.py fluent.json fluent") + zk_data = json.load(open("zookeeper-time.json")) + rmq_data = json.load(open("rabbitmq-time.json")) + fb_data = json.load(open("fluent-time.json")) + zk_raw_data = json.load(open("zookeeper.json")) + rmq_raw_data = json.load(open("rabbitmq.json")) + fb_raw_data = json.load(open("fluent.json")) + print("ZooKeeper:") + print("Liveness & {}".format(zk_data["Liveness"] / 1000)) + print("Safety & {}".format(zk_data["Safety"] / 1000)) + print("Conformance & {}".format(zk_data["Impl"] / 1000)) + print( + "Total & {} ({})".format( + zk_data["Total"] / 1000, zk_raw_data["times-ms"]["total"] / 1000 + ) + ) + print("RabbitMQ:") + print("Liveness & {}".format(rmq_data["Liveness"] / 1000)) + print("Safety & {}".format(rmq_data["Safety"] / 1000)) + print("Conformance & {}".format(rmq_data["Impl"] / 1000)) + print( + "Total & {} ({})".format( + rmq_data["Total"] / 1000, rmq_raw_data["times-ms"]["total"] / 1000 + ) + ) + print("Fluent:") + print("Liveness & {}".format(fb_data["Liveness"] / 1000)) + print("Safety & {}".format(fb_data["Safety"] / 1000)) + print("Conformance & {}".format(fb_data["Impl"] / 1000)) + print( + "Total & {} ({})".format( + fb_data["Total"] / 1000, fb_raw_data["times-ms"]["total"] / 1000 + ) + ) + + +if __name__ == "__main__": + main() From 07ba99393402734c584905b455a4f299ea44105f Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Mon, 4 Dec 2023 20:56:09 -0600 Subject: [PATCH 2/2] more Signed-off-by: Xudong Sun --- tools/gen-t1-t2-time.py | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tools/gen-t1-t2-time.py b/tools/gen-t1-t2-time.py index 201482f4f..63d066fb3 100644 --- a/tools/gen-t1-t2-time.py +++ b/tools/gen-t1-t2-time.py @@ -12,6 +12,7 @@ def main(): zk_raw_data = json.load(open("zookeeper.json")) rmq_raw_data = json.load(open("rabbitmq.json")) fb_raw_data = json.load(open("fluent.json")) + anvil_raw_data = json.load(open("lib.json")) print("ZooKeeper:") print("Liveness & {}".format(zk_data["Liveness"] / 1000)) print("Safety & {}".format(zk_data["Safety"] / 1000)) @@ -39,6 +40,13 @@ def main(): fb_data["Total"] / 1000, fb_raw_data["times-ms"]["total"] / 1000 ) ) + print("Anvil:") + print( + "Reusable lemmas & {} ({})".format( + anvil_raw_data["times-ms"]["total-verify"] / 1000, + anvil_raw_data["times-ms"]["total"] / 1000, + ) + ) if __name__ == "__main__":