Format Python under tla/ (#6515)

microsoft · Oct 1, 2024 · df6d004 · df6d004
1 parent 0182242
commit df6d004
Show file tree

Hide file tree

Showing 5 changed files with 68 additions and 24 deletions.
diff --git a/scripts/ci-checks.sh b/scripts/ci-checks.sh
@@ -109,9 +109,9 @@ endgroup
 
 group "Python format"
 if [ $FIX -ne 0 ]; then
-  git ls-files tests/ python/ scripts/ .cmake-format.py | grep -e '\.py$' | xargs black
+  git ls-files tests/ python/ scripts/ tla/ .cmake-format.py | grep -e '\.py$' | xargs black
 else
-  git ls-files tests/ python/ scripts/ .cmake-format.py | grep -e '\.py$' | xargs black --check
+  git ls-files tests/ python/ scripts/ tla/ .cmake-format.py | grep -e '\.py$' | xargs black --check
 fi
 endgroup
 

diff --git a/tla/actions.py b/tla/actions.py
@@ -21,7 +21,7 @@
 
 """
 
-TOP=5
+TOP = 5
 
 if __name__ == "__main__":
     ts = defaultdict(list)
@@ -40,8 +40,10 @@
     top_TOP = [x[0] for x in col_max[-TOP:]]
     df_TOP = df[top_TOP]
     print(df_TOP)
-    plot = df_TOP.plot.line(y=df_TOP.columns, width=1200, height=600, title=f"Top {TOP} distinct actions")
+    plot = df_TOP.plot.line(
+        y=df_TOP.columns, width=1200, height=600, title=f"Top {TOP} distinct actions"
+    )
     if len(sys.argv) > 1:
         hvplot.save(plot, sys.argv[1])
     else:
-        hvplot.show(plot)
+        hvplot.show(plot)
diff --git a/tla/install_deps.py b/tla/install_deps.py
@@ -79,7 +79,9 @@ def _parse_args() -> argparse.Namespace:
 
 def install_tlc():
     java = "java"
-    tlaplus_path = "~/.vscode-remote/extensions/tlaplus.vscode-ide-*/tools/tla2tools.jar"
+    tlaplus_path = (
+        "~/.vscode-remote/extensions/tlaplus.vscode-ide-*/tools/tla2tools.jar"
+    )
     copy_tlaplus = f"-cp {tlaplus_path} tlc2.TLC"
 
     set_alias("tlcrepl", f"{java} -cp {tlaplus_path} tlc2.REPL")

diff --git a/tla/loc.py b/tla/loc.py
@@ -4,6 +4,7 @@
 import dataclasses
 import sys
 
+
 @dataclasses.dataclass
 class LOC:
     code: int = 0
@@ -21,9 +22,10 @@ def __add__(self, other):
         return LOC(
             self.code + other.code,
             self.comment + other.comment,
-            self.blank + other.blank
+            self.blank + other.blank,
         )
 
+
 def is_comment(line: str) -> bool:
     if line.startswith(r"\*"):
         return True
@@ -33,15 +35,19 @@ def is_comment(line: str) -> bool:
         return True
     return False
 
+
 def is_multiline_comment_start(line: str) -> bool:
     return line.startswith("(*")
 
+
 def is_footer(line: str) -> bool:
     return all(c == "=" for c in line)
 
+
 def is_multiline_comment_end(line: str) -> bool:
     return line.endswith("*)")
 
+
 def count_loc(lines) -> LOC:
     loc = LOC()
     in_comment = False
@@ -68,6 +74,7 @@ def count_loc(lines) -> LOC:
             loc.code += 1
     return loc
 
+
 JUST_CODE = r"""
 ---------- MODULE MCccfraft ----------
 EXTENDS ccfraft, StatsFile, MCAliases
@@ -127,6 +134,7 @@ def count_loc(lines) -> LOC:
     /\ msg.prevLogIndex = logline.msg.packet.prev_idx
 """
 
+
 def test_loc():
     """
     Run with py.test loc.py
@@ -135,7 +143,10 @@ def test_loc():
     assert count_loc(CODE_AND_COMMENTS.splitlines()) == LOC(code=2, comment=2, blank=1)
     assert count_loc(FOOTER.splitlines()) == LOC(code=0, comment=9, blank=1)
     assert count_loc(MULTILINE_COMMENT.splitlines()) == LOC(code=2, comment=4, blank=2)
-    assert count_loc(MULTILINE_COMMENT_2.splitlines()) == LOC(code=7, comment=12, blank=1)
+    assert count_loc(MULTILINE_COMMENT_2.splitlines()) == LOC(
+        code=7, comment=12, blank=1
+    )
+
 
 if __name__ == "__main__":
     locs = []
@@ -144,4 +155,4 @@ def test_loc():
             lines = f.readlines()
         locs.append(count_loc(lines))
         print(f"{arg} {locs[-1]}")
-    print(f"Total {sum(locs, LOC())}")
+    print(f"Total {sum(locs, LOC())}")
diff --git a/tla/trace2scen.py b/tla/trace2scen.py
@@ -5,27 +5,41 @@
 import json
 import os
 
+
 def comment(action):
     return f"# {action['name']} {action['location']['module']}:{action['location']['beginLine']}"
 
+
 def term(ctx, pre):
-    return str(pre["currentTerm"][ctx['i']])
+    return str(pre["currentTerm"][ctx["i"]])
+
 
 def noop(ctx, pre, post):
     return ["# Noop"]
 
+
 MAP = {
     "ClientRequest": lambda ctx, pre, post: ["replicate", term(ctx, pre), "42"],
     "MCClientRequest": lambda ctx, pre, post: ["replicate", term(ctx, pre), "42"],
-    "CheckQuorum": lambda ctx, pre, post: ["periodic_one", ctx['i'], "110"],
-    "Timeout": lambda ctx, pre, post: ["periodic_one",  ctx['i'], "110"],
-    "MCTimeout": lambda ctx, pre, post: ["periodic_one",  ctx['i'], "110"],
+    "CheckQuorum": lambda ctx, pre, post: ["periodic_one", ctx["i"], "110"],
+    "Timeout": lambda ctx, pre, post: ["periodic_one", ctx["i"], "110"],
+    "MCTimeout": lambda ctx, pre, post: ["periodic_one", ctx["i"], "110"],
     "RequestVote": noop,
     "AppendEntries": lambda _, __, ___: ["dispatch_all"],
     "BecomeLeader": noop,
-    "SignCommittableMessages": lambda ctx, pre, post: ["emit_signature", term(ctx, pre)],
-    "MCSignCommittableMessages": lambda ctx, pre, post: ["emit_signature", term(ctx, pre)],
-    "ChangeConfigurationInt": lambda ctx, pre, post: ["replicate_new_configuration", term(ctx, pre), *ctx["newConfiguration"]],
+    "SignCommittableMessages": lambda ctx, pre, post: [
+        "emit_signature",
+        term(ctx, pre),
+    ],
+    "MCSignCommittableMessages": lambda ctx, pre, post: [
+        "emit_signature",
+        term(ctx, pre),
+    ],
+    "ChangeConfigurationInt": lambda ctx, pre, post: [
+        "replicate_new_configuration",
+        term(ctx, pre),
+        *ctx["newConfiguration"],
+    ],
     "AdvanceCommitIndex": noop,
     "HandleRequestVoteRequest": lambda _, __, ___: ["dispatch_all"],
     "HandleRequestVoteResponse": noop,
@@ -38,31 +52,46 @@ def noop(ctx, pre, post):
     "RcvRequestVoteResponse": noop,
 }
 
+
 def post_commit(post):
-    return [["assert_commit_idx", node, str(idx)] for node, idx in post["commitIndex"].items()]
+    return [
+        ["assert_commit_idx", node, str(idx)]
+        for node, idx in post["commitIndex"].items()
+    ]
+
 
 def post_state(post):
     entries = []
     for node, state in post["state"].items():
-            entries.append(["assert_detail", "leadership_state", node, state])
+        entries.append(["assert_detail", "leadership_state", node, state])
     return entries
 
+
 def step_to_action(pre_state, action, post_state):
-    return os.linesep.join([
-        comment(action),
-        ','.join(MAP[action['name']](action['context'], pre_state[1], post_state[1]))])
+    return os.linesep.join(
+        [
+            comment(action),
+            ",".join(
+                MAP[action["name"]](action["context"], pre_state[1], post_state[1])
+            ),
+        ]
+    )
+
 
 def asserts(pre_state, action, post_state, assert_gen):
-    return os.linesep.join([','.join(assertion) for assertion in assert_gen(post_state[1])])
+    return os.linesep.join(
+        [",".join(assertion) for assertion in assert_gen(post_state[1])]
+    )
+
 
 if __name__ == "__main__":
     with open(sys.argv[1]) as trace:
         steps = json.load(trace)["action"]
         initial_state = steps[0][0][1]
-        initial_node, = [node for node, log in initial_state["log"].items() if log]
+        (initial_node,) = [node for node, log in initial_state["log"].items() if log]
         print(f"start_node,{initial_node}")
         print(f"emit_signature,2")
         for step in steps:
             print(step_to_action(*step))
             print(asserts(*step, post_state))
-        print(asserts(*steps[-1], post_commit))
+        print(asserts(*steps[-1], post_commit))