FA-75071 / CRDT convergence / Open access
Two-phase graph: edges may be added to removed vertices · case 01
An edge to a vertex that was removed is accepted instead of rejected.
ROOT CAUSE
The add-edge precondition checks only that the endpoints were ever added.
VERIFIED REPAIR
Require both endpoints to be live (added and not removed) at the origin.
Unsuccessful approach: Checking liveness only for the source still admits edges into removed targets.
Case contract
Vertices and edges each have grow-only add and remove sets. A vertex is live when added and not removed; an edge is visible when added, not removed, and both endpoints are live. At the origin replica, adding an edge requires both endpoints live, removing a vertex requires no visible edge touching it in either direction, and removing an edge requires it visible; failed preconditions record the op index. ["merge", s, d] unions all four sets into d. Return sorted live vertices and visible edges per replica plus rejections.
Why this case matters
Graph CRDTs must keep edges consistent with vertex removals that happen concurrently on other replicas.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
VA = {r: set() for r in replicas}
VR = {r: set() for r in replicas}
EA = {r: set() for r in replicas}
ER = {r: set() for r in replicas}
rejected = []
def vlive(r, v):
return v in VA[r] and v not in VR[r]
def evis(r, e):
return e in EA[r] and e not in ER[r] and vlive(r, e[0]) and vlive(r, e[1])
for i, op in enumerate(ops):
kind, r = op[0], op[1]
if kind == 'addv':
VA[r].add(op[2])
elif kind == 'remv':
v = op[2]
if not vlive(r, v) or any(evis(r, e) and v in e for e in EA[r]):
rejected.append(i)
else:
VR[r].add(v)
elif kind == 'adde':
e = (op[2], op[3])
if e[0] in VA[r] and e[1] in VA[r]:
EA[r].add(e)
else:
rejected.append(i)
elif kind == 'reme':
e = (op[2], op[3])
if evis(r, e):
ER[r].add(e)
else:
rejected.append(i)
else:
d = op[2]
VA[d] |= VA[r]
VR[d] |= VR[r]
EA[d] |= EA[r]
ER[d] |= ER[r]
out = []
for r in replicas:
out.append([sorted(v for v in VA[r] if vlive(r, v)), sorted(list(e) for e in EA[r] if evis(r, e))])
return {'graphs': out, 'rejected': rejected}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w1'], ['adde', 'a', 'w1', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []})],
2: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w2'], ['adde', 'a', 'w2', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'p', 'q'], []]], 'rejected': []})],
3: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w3'], ['adde', 'a', 'w3', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'p', 'q'], []]], 'rejected': []})],
4: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w4'], ['adde', 'a', 'w4', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2'], ['addv', 'b', 'n3']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'n3', 'p', 'q'], []]], 'rejected': []})],
5: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w5'], ['adde', 'a', 'w5', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2'], ['addv', 'b', 'n3'], ['addv', 'b', 'n4']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'n3', 'n4', 'p', 'q'], []]], 'rejected': []})],
}[N]
for label, args, expected in cases:
check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| edge between live vertices | {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []} | {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []} | Passed |
| edge to a missing vertex is rejected | {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]} | {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]} | Passed |
| edge to a removed vertex is rejected | {'graphs': [[['u'], []], [[], []]], 'rejected': []} | {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]} | Failed |
| vertex with incoming edge cannot be removed | {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]} | {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]} | Passed |
| vertex removable after its edge is removed | {'graphs': [[['u'], []], [[], []]], 'rejected': []} | {'graphs': [[['u'], []], [[], []]], 'rejected': []} | Passed |
| concurrent vertex removal hides dangling edge | {'graphs': [[['u'], []], [['u'], []]], 'rejected': []} | {'graphs': [[['u'], []], [['u'], []]], 'rejected': []} | Passed |
| concurrent removal of the source vertex hides the edge | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | Passed |
| edge removal propagates | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | Passed |
SHA-256 / 0229022a8df02e1ea72ce90502d0d84d83b4a0e15f0aed4a3fad0fd9105c8a31
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
VA = {r: set() for r in replicas}
VR = {r: set() for r in replicas}
EA = {r: set() for r in replicas}
ER = {r: set() for r in replicas}
rejected = []
def vlive(r, v):
return v in VA[r] and v not in VR[r]
def evis(r, e):
return e in EA[r] and e not in ER[r] and vlive(r, e[0]) and vlive(r, e[1])
for i, op in enumerate(ops):
kind, r = op[0], op[1]
if kind == 'addv':
VA[r].add(op[2])
elif kind == 'remv':
v = op[2]
if not vlive(r, v) or any(evis(r, e) and v in e for e in EA[r]):
rejected.append(i)
else:
VR[r].add(v)
elif kind == 'adde':
e = (op[2], op[3])
if vlive(r, e[0]) and e[1] in VA[r]:
EA[r].add(e)
else:
rejected.append(i)
elif kind == 'reme':
e = (op[2], op[3])
if evis(r, e):
ER[r].add(e)
else:
rejected.append(i)
else:
d = op[2]
VA[d] |= VA[r]
VR[d] |= VR[r]
EA[d] |= EA[r]
ER[d] |= ER[r]
out = []
for r in replicas:
out.append([sorted(v for v in VA[r] if vlive(r, v)), sorted(list(e) for e in EA[r] if evis(r, e))])
return {'graphs': out, 'rejected': rejected}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w1'], ['adde', 'a', 'w1', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []})],
2: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w2'], ['adde', 'a', 'w2', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'p', 'q'], []]], 'rejected': []})],
3: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w3'], ['adde', 'a', 'w3', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'p', 'q'], []]], 'rejected': []})],
4: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w4'], ['adde', 'a', 'w4', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2'], ['addv', 'b', 'n3']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'n3', 'p', 'q'], []]], 'rejected': []})],
5: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w5'], ['adde', 'a', 'w5', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2'], ['addv', 'b', 'n3'], ['addv', 'b', 'n4']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'n3', 'n4', 'p', 'q'], []]], 'rejected': []})],
}[N]
for label, args, expected in cases:
check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| edge between live vertices | {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []} | {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []} | Passed |
| edge to a missing vertex is rejected | {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]} | {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]} | Passed |
| edge to a removed vertex is rejected | {'graphs': [[['u'], []], [[], []]], 'rejected': [4]} | {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]} | Failed |
| vertex with incoming edge cannot be removed | {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]} | {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]} | Passed |
| vertex removable after its edge is removed | {'graphs': [[['u'], []], [[], []]], 'rejected': []} | {'graphs': [[['u'], []], [[], []]], 'rejected': []} | Passed |
| concurrent vertex removal hides dangling edge | {'graphs': [[['u'], []], [['u'], []]], 'rejected': []} | {'graphs': [[['u'], []], [['u'], []]], 'rejected': []} | Passed |
| concurrent removal of the source vertex hides the edge | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | Passed |
| edge removal propagates | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | Passed |
SHA-256 / 6e49e029101a02c81b054277e112ca3d5ab75c6c630d152b1a0bbd446c3801b8
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
VA = {r: set() for r in replicas}
VR = {r: set() for r in replicas}
EA = {r: set() for r in replicas}
ER = {r: set() for r in replicas}
rejected = []
def vlive(r, v):
return v in VA[r] and v not in VR[r]
def evis(r, e):
return e in EA[r] and e not in ER[r] and vlive(r, e[0]) and vlive(r, e[1])
for i, op in enumerate(ops):
kind, r = op[0], op[1]
if kind == 'addv':
VA[r].add(op[2])
elif kind == 'remv':
v = op[2]
if not vlive(r, v) or any(evis(r, e) and v in e for e in EA[r]):
rejected.append(i)
else:
VR[r].add(v)
elif kind == 'adde':
e = (op[2], op[3])
if vlive(r, e[0]) and vlive(r, e[1]):
EA[r].add(e)
else:
rejected.append(i)
elif kind == 'reme':
e = (op[2], op[3])
if evis(r, e):
ER[r].add(e)
else:
rejected.append(i)
else:
d = op[2]
VA[d] |= VA[r]
VR[d] |= VR[r]
EA[d] |= EA[r]
ER[d] |= ER[r]
out = []
for r in replicas:
out.append([sorted(v for v in VA[r] if vlive(r, v)), sorted(list(e) for e in EA[r] if evis(r, e))])
return {'graphs': out, 'rejected': rejected}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w1'], ['adde', 'a', 'w1', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []})],
2: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w2'], ['adde', 'a', 'w2', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'p', 'q'], []]], 'rejected': []})],
3: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w3'], ['adde', 'a', 'w3', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'p', 'q'], []]], 'rejected': []})],
4: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w4'], ['adde', 'a', 'w4', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2'], ['addv', 'b', 'n3']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'n3', 'p', 'q'], []]], 'rejected': []})],
5: [('edge between live vertices', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []}), ('edge to a missing vertex is rejected', [[['addv', 'a', 'u'], ['adde', 'a', 'u', 'w5'], ['adde', 'a', 'w5', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]}), ('edge to a removed vertex is rejected', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['remv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['adde', 'a', 'v', 'u']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]}), ('vertex with incoming edge cannot be removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['remv', 'a', 'v'], ['remv', 'a', 'u']], ['a', 'b']], {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]}), ('vertex removable after its edge is removed', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['adde', 'a', 'u', 'v'], ['reme', 'a', 'u', 'v'], ['remv', 'a', 'v']], ['a', 'b']], {'graphs': [[['u'], []], [[], []]], 'rejected': []}), ('concurrent vertex removal hides dangling edge', [[['addv', 'a', 'u'], ['addv', 'a', 'v'], ['merge', 'a', 'b'], ['adde', 'a', 'u', 'v'], ['remv', 'b', 'v'], ['merge', 'b', 'a'], ['merge', 'a', 'b']], ['a', 'b']], {'graphs': [[['u'], []], [['u'], []]], 'rejected': []}), ('concurrent removal of the source vertex hides the edge', [[['addv', 'a', 'x'], ['addv', 'a', 'y'], ['merge', 'a', 'b'], ['adde', 'a', 'x', 'y'], ['remv', 'b', 'x'], ['merge', 'b', 'a']], ['a', 'b']], {'graphs': [[['y'], []], [['y'], []]], 'rejected': []}), ('edge removal propagates', [[['addv', 'a', 'p'], ['addv', 'a', 'q'], ['adde', 'a', 'p', 'q'], ['merge', 'a', 'b'], ['reme', 'b', 'p', 'q'], ['merge', 'b', 'a'], ['addv', 'b', 'n0'], ['addv', 'b', 'n1'], ['addv', 'b', 'n2'], ['addv', 'b', 'n3'], ['addv', 'b', 'n4']], ['a', 'b']], {'graphs': [[['p', 'q'], []], [['n0', 'n1', 'n2', 'n3', 'n4', 'p', 'q'], []]], 'rejected': []})],
}[N]
for label, args, expected in cases:
check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| edge between live vertices | {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []} | {'graphs': [[['u', 'v'], [['u', 'v']]], [['u', 'v'], [['u', 'v']]]], 'rejected': []} | Passed |
| edge to a missing vertex is rejected | {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]} | {'graphs': [[['u'], []], [[], []]], 'rejected': [1, 2]} | Passed |
| edge to a removed vertex is rejected | {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]} | {'graphs': [[['u'], []], [[], []]], 'rejected': [3, 4]} | Passed |
| vertex with incoming edge cannot be removed | {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]} | {'graphs': [[['u', 'v'], [['u', 'v']]], [[], []]], 'rejected': [3, 4]} | Passed |
| vertex removable after its edge is removed | {'graphs': [[['u'], []], [[], []]], 'rejected': []} | {'graphs': [[['u'], []], [[], []]], 'rejected': []} | Passed |
| concurrent vertex removal hides dangling edge | {'graphs': [[['u'], []], [['u'], []]], 'rejected': []} | {'graphs': [[['u'], []], [['u'], []]], 'rejected': []} | Passed |
| concurrent removal of the source vertex hides the edge | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | Passed |
| edge removal propagates | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | Passed |
SHA-256 / ee616f41ed40913648bb507ba5c16e92f7405514bb81255c774778f1e9752c7a
Verification & scope
A deterministic, bounded teaching model of one replicated data type with stipulated operation and merge rules; it is not a production CRDT library and makes no claim of conformance to any specific published design. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.
Observations recorded using Python 3.12.14 at 2026-09-29T14:49:02.706296+00:00.
Case digest / aa31f1fadb0e6df05ce6c4f785a00cad8747416b041df90c39da56b74198a100