FAILURE MAP
← Case archive

FA-11531 / Static analysis soundness / Open access

A single dataflow sweep misses facts across backward edges · case 01

A single dataflow sweep misses facts across backward edges.

Verified by executionVariant 1 · 6 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

Nodes are visited only once even after a successor receives new information.

VERIFIED REPAIR

Repeat monotone union propagation until no node changes.

Unsuccessful approach: A second fixed sweep handles short paths but still misses longer reverse-ordered chains.

Case contract

Given node count, directed edges, and per-node seed labels, return the sorted labels reachable at each node, including seeds; compute the least union fixed point.

Why this case matters

A deterministic offline analysis model exposing a specific soundness or precision boundary; it does not implement a complete language analyzer.

1 / The failure

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(count, edges, seeds):
    facts=[set(x) for x in seeds]
    for a,b in edges: facts[b]|=facts[a]
    return [sorted(x) for x in facts]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='d'+str(N)
check('three reverse dependencies',solve(4,[(2,3),(1,2),(0,1)],[[x],[],[],[]]),[[x],[x],[x],[x]])
check('cycle converges',solve(3,[(1,2),(2,0),(0,1)],[[x],[],[]]),[[x],[x],[x]])
check('isolated nodes',solve(2,[],[[x],[]]),[[x],[]])
check('self edge',solve(1,[(0,0)],[[x]]),[[x]])
check('no nodes',solve(0,[],[]),[])
check('union incoming',solve(3,[(0,2),(1,2)],[[x],['a'],[]]),[[x],['a'],['a',x]])
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 fixtureActualExpectedOutcome
three reverse dependencies[['d1'], ['d1'], [], []][['d1'], ['d1'], ['d1'], ['d1']]Failed
cycle converges[['d1'], ['d1'], []][['d1'], ['d1'], ['d1']]Failed
isolated nodes[['d1'], []][['d1'], []]Passed
self edge[['d1']][['d1']]Passed
no nodes[][]Passed
union incoming[['d1'], ['a'], ['a', 'd1']][['d1'], ['a'], ['a', 'd1']]Passed

SHA-256 / fd6e3fd8eb8be1d63c430305f83d3c82271426400aa1bc8d8639ab1d8f53982a

2 / The unsuccessful fix

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(count, edges, seeds):
    facts=[set(x) for x in seeds]
    for _ in range(2):
        for a,b in edges: facts[b]|=facts[a]
    return [sorted(x) for x in facts]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='d'+str(N)
check('three reverse dependencies',solve(4,[(2,3),(1,2),(0,1)],[[x],[],[],[]]),[[x],[x],[x],[x]])
check('cycle converges',solve(3,[(1,2),(2,0),(0,1)],[[x],[],[]]),[[x],[x],[x]])
check('isolated nodes',solve(2,[],[[x],[]]),[[x],[]])
check('self edge',solve(1,[(0,0)],[[x]]),[[x]])
check('no nodes',solve(0,[],[]),[])
check('union incoming',solve(3,[(0,2),(1,2)],[[x],['a'],[]]),[[x],['a'],['a',x]])
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 fixtureActualExpectedOutcome
three reverse dependencies[['d1'], ['d1'], ['d1'], []][['d1'], ['d1'], ['d1'], ['d1']]Failed
cycle converges[['d1'], ['d1'], ['d1']][['d1'], ['d1'], ['d1']]Passed
isolated nodes[['d1'], []][['d1'], []]Passed
self edge[['d1']][['d1']]Passed
no nodes[][]Passed
union incoming[['d1'], ['a'], ['a', 'd1']][['d1'], ['a'], ['a', 'd1']]Passed

SHA-256 / ab3fd4ff0c159490a610291dd77e4b0729b828023968d0d7700e623036d08448

3 / The verified repair

Exit 0
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(count, edges, seeds):
    facts=[set(x) for x in seeds]
    changed=True
    while changed:
        changed=False
        for a,b in edges:
            old=len(facts[b]); facts[b]|=facts[a]
            changed |= len(facts[b])!=old
    return [sorted(x) for x in facts]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='d'+str(N)
check('three reverse dependencies',solve(4,[(2,3),(1,2),(0,1)],[[x],[],[],[]]),[[x],[x],[x],[x]])
check('cycle converges',solve(3,[(1,2),(2,0),(0,1)],[[x],[],[]]),[[x],[x],[x]])
check('isolated nodes',solve(2,[],[[x],[]]),[[x],[]])
check('self edge',solve(1,[(0,0)],[[x]]),[[x]])
check('no nodes',solve(0,[],[]),[])
check('union incoming',solve(3,[(0,2),(1,2)],[[x],['a'],[]]),[[x],['a'],['a',x]])
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 fixtureActualExpectedOutcome
three reverse dependencies[['d1'], ['d1'], ['d1'], ['d1']][['d1'], ['d1'], ['d1'], ['d1']]Passed
cycle converges[['d1'], ['d1'], ['d1']][['d1'], ['d1'], ['d1']]Passed
isolated nodes[['d1'], []][['d1'], []]Passed
self edge[['d1']][['d1']]Passed
no nodes[][]Passed
union incoming[['d1'], ['a'], ['a', 'd1']][['d1'], ['a'], ['a', 'd1']]Passed

SHA-256 / 230f80a19dd3ab80b0cc69e3808c1a5a374f28e7fc676aa31aa58afe656a0e8e

Verification & scope

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:38:48.685003+00:00.

Case digest / a85cb1de95a5dac8bc6f3ad55ab796f1b5d56d9904150947e3d17850e5c8374d