diff --git a/src/consensus/aft/test/driver.h b/src/consensus/aft/test/driver.h index 19f006832536..c5e23e833312 100644 --- a/src/consensus/aft/test/driver.h +++ b/src/consensus/aft/test/driver.h @@ -279,9 +279,7 @@ class RaftDriver if (_nodes.find(node_id) == _nodes.end()) { - throw std::runtime_error(fmt::format( - "Node {} does not exist yet. Use \"create_new_node, \"", - node_id)); + create_new_node(node_id_s); } configuration.try_emplace(node_id); @@ -1053,7 +1051,8 @@ class RaftDriver idx) << std::endl; throw std::runtime_error(fmt::format( - "Node not at expected commit idx ({}) on line {} : {}", + "Node {} not at expected commit idx ({}) on line {} : {}", + node_id, idx, std::to_string((int)lineno), _nodes.at(node_id).raft->get_committed_seqno())); diff --git a/tla/trace2scen.py b/tla/trace2scen.py new file mode 100644 index 000000000000..d67f85fc36d9 --- /dev/null +++ b/tla/trace2scen.py @@ -0,0 +1,73 @@ +# Copyright (c) Microsoft Corporation. All rights reserved. +# Licensed under the Apache 2.0 License. + +import sys +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']]) + +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"], + "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"]], + "AdvanceCommitIndex": noop, + "HandleRequestVoteRequest": lambda _, __, ___: ["dispatch_all"], + "HandleRequestVoteResponse": noop, + "RejectAppendEntriesRequest": noop, + "ReturnToFollowerState": noop, + "AppendEntriesAlreadyDone": noop, + "RcvDropIgnoredMessage": noop, + "RcvUpdateTerm": noop, + "RcvRequestVoteRequest": noop, + "RcvRequestVoteResponse": noop, +} + +def post_commit(post): + 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(): + if state == "Leader": + entries.append(["assert_is_primary", node]) + elif state == "Follower": + entries.append(["assert_is_backup", node]) + elif state == "Candidate": + entries.append(["assert_is_candidate", node]) + 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]))]) + +def asserts(pre_state, action, post_state, assert_gen): + 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] + 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)) \ No newline at end of file