FA-75076 / CRDT convergence / Open access
Two-phase graph: merge does not carry edge removals · case 01
An edge removed on one replica remains visible on the others.
ROOT CAUSE
Merge unions vertex sets and added edges but omits the removed-edge set.
VERIFIED REPAIR
Union the removed-edge set into the destination during merge.
Unsuccessful approach: Intersecting removed-edge sets forgets removals that only one replica has seen.
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 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]
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'], [['p', 'q']]], [['n0', 'p', 'q'], []]], 'rejected': []} | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | Failed |
SHA-256 / 55c0047abff2eb25f4cc80a949dbe15b837527c0b1869e875e8960da25a0b5f7
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 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'], [['p', 'q']]], [['n0', 'p', 'q'], []]], 'rejected': []} | {'graphs': [[['p', 'q'], []], [['n0', 'p', 'q'], []]], 'rejected': []} | Failed |
SHA-256 / 86a67496161af2719786626738cd2c961190ee0e07ff5e75c926d5cdbc9ebce5
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.843563+00:00.
Case digest / a61dea8b109f29c8c8428def59c8db5b381d42fbc070f9a3f1993824bb1bf532