FA-75061 / CRDT convergence / Open access
Two-phase graph: edges to concurrently removed vertices remain visible · case 01
After merging a concurrent vertex removal, an edge dangles from or into a vertex that no longer exists.
ROOT CAUSE
Edge visibility tests only the edge sets and ignores endpoint liveness.
VERIFIED REPAIR
An edge is visible only while both of its endpoints are live.
Unsuccessful approach: Checking only the target endpoint still shows edges whose source vertex was removed.
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]
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', 'v']]], [['u'], [['u', 'v']]]], 'rejected': []} | {'graphs': [[['u'], []], [['u'], []]], 'rejected': []} | Failed |
| concurrent removal of the source vertex hides the edge | {'graphs': [[['y'], [['x', 'y']]], [['y'], []]], 'rejected': []} | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | Failed |
| edge removal propagates | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | Passed |
SHA-256 / 8f4a441dc4300e85027e8af0d3a978b17d0e3cbf013480ba709e3d72312c131c
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[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'], [['x', 'y']]], [['y'], []]], 'rejected': []} | {'graphs': [[['y'], []], [['y'], []]], 'rejected': []} | Failed |
| edge removal propagates | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | Passed |
SHA-256 / 82a6d0866d400bb41df913f73e20139e0d65039d48e0bbfd7a2096c53cadc442
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.521768+00:00.
Case digest / 1f0662b49e4d3c9b5fc59fd2a64d2f0e6963a67bf6eb10da31c210ddd0b817d2