{"abstract":"A single dataflow sweep misses facts across backward edges.","category":"Static analysis soundness","checks":6,"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.","evaluation_group":"model-846a39dd5041e56b","failed_approach":"A second fixed sweep handles short paths but still misses longer reverse-ordered chains.","family":"z-static_analysis-propagation-fixpoint","id":"FA-11531","implementations":{"attempt":{"sha256":"ab3fd4ff0c159490a610291dd77e4b0729b828023968d0d7700e623036d08448","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(count, edges, seeds):\n    facts=[set(x) for x in seeds]\n    for _ in range(2):\n        for a,b in edges: facts[b]|=facts[a]\n    return [sorted(x) for x in facts]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='d'+str(N)\ncheck('three reverse dependencies',solve(4,[(2,3),(1,2),(0,1)],[[x],[],[],[]]),[[x],[x],[x],[x]])\ncheck('cycle converges',solve(3,[(1,2),(2,0),(0,1)],[[x],[],[]]),[[x],[x],[x]])\ncheck('isolated nodes',solve(2,[],[[x],[]]),[[x],[]])\ncheck('self edge',solve(1,[(0,0)],[[x]]),[[x]])\ncheck('no nodes',solve(0,[],[]),[])\ncheck('union incoming',solve(3,[(0,2),(1,2)],[[x],['a'],[]]),[[x],['a'],['a',x]])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"fd6e3fd8eb8be1d63c430305f83d3c82271426400aa1bc8d8639ab1d8f53982a","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(count, edges, seeds):\n    facts=[set(x) for x in seeds]\n    for a,b in edges: facts[b]|=facts[a]\n    return [sorted(x) for x in facts]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='d'+str(N)\ncheck('three reverse dependencies',solve(4,[(2,3),(1,2),(0,1)],[[x],[],[],[]]),[[x],[x],[x],[x]])\ncheck('cycle converges',solve(3,[(1,2),(2,0),(0,1)],[[x],[],[]]),[[x],[x],[x]])\ncheck('isolated nodes',solve(2,[],[[x],[]]),[[x],[]])\ncheck('self edge',solve(1,[(0,0)],[[x]]),[[x]])\ncheck('no nodes',solve(0,[],[]),[])\ncheck('union incoming',solve(3,[(0,2),(1,2)],[[x],['a'],[]]),[[x],['a'],['a',x]])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"230f80a19dd3ab80b0cc69e3808c1a5a374f28e7fc676aa31aa58afe656a0e8e","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(count, edges, seeds):\n    facts=[set(x) for x in seeds]\n    changed=True\n    while changed:\n        changed=False\n        for a,b in edges:\n            old=len(facts[b]); facts[b]|=facts[a]\n            changed |= len(facts[b])!=old\n    return [sorted(x) for x in facts]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='d'+str(N)\ncheck('three reverse dependencies',solve(4,[(2,3),(1,2),(0,1)],[[x],[],[],[]]),[[x],[x],[x],[x]])\ncheck('cycle converges',solve(3,[(1,2),(2,0),(0,1)],[[x],[],[]]),[[x],[x],[x]])\ncheck('isolated nodes',solve(2,[],[[x],[]]),[[x],[]])\ncheck('self edge',solve(1,[(0,0)],[[x]]),[[x]])\ncheck('no nodes',solve(0,[],[]),[])\ncheck('union incoming',solve(3,[(0,2),(1,2)],[[x],['a'],[]]),[[x],['a'],['a',x]])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":" 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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"z-static_analysis-propagation-fixpoint","generated_at":"2026-09-29T14:38:48.685003+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A deterministic offline analysis model exposing a specific soundness or precision boundary; it does not implement a complete language analyzer.","repair":"Repeat monotone union propagation until no node changes.","root_cause":"Nodes are visited only once even after a successor receives new information.","sha256":"a85cb1de95a5dac8bc6f3ad55ab796f1b5d56d9904150947e3d17850e5c8374d","title":"A single dataflow sweep misses facts across backward edges · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":39.382,"exit_code":1,"observations":[{"actual":[["d1"],["d1"],["d1"],[]],"check":"three reverse dependencies","expected":[["d1"],["d1"],["d1"],["d1"]],"passed":false},{"actual":[["d1"],["d1"],["d1"]],"check":"cycle converges","expected":[["d1"],["d1"],["d1"]],"passed":true},{"actual":[["d1"],[]],"check":"isolated nodes","expected":[["d1"],[]],"passed":true},{"actual":[["d1"]],"check":"self edge","expected":[["d1"]],"passed":true},{"actual":[],"check":"no nodes","expected":[],"passed":true},{"actual":[["d1"],["a"],["a","d1"]],"check":"union incoming","expected":[["d1"],["a"],["a","d1"]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"three reverse dependencies\", \"actual\": [[\"d1\"], [\"d1\"], [\"d1\"], []], \"expected\": [[\"d1\"], [\"d1\"], [\"d1\"], [\"d1\"]], \"passed\": false}, {\"check\": \"cycle converges\", \"actual\": [[\"d1\"], [\"d1\"], [\"d1\"]], \"expected\": [[\"d1\"], [\"d1\"], [\"d1\"]], \"passed\": true}, {\"check\": \"isolated nodes\", \"actual\": [[\"d1\"], []], \"expected\": [[\"d1\"], []], \"passed\": true}, {\"check\": \"self edge\", \"actual\": [[\"d1\"]], \"expected\": [[\"d1\"]], \"passed\": true}, {\"check\": \"no nodes\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"union incoming\", \"actual\": [[\"d1\"], [\"a\"], [\"a\", \"d1\"]], \"expected\": [[\"d1\"], [\"a\"], [\"a\", \"d1\"]], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":36.201,"exit_code":1,"observations":[{"actual":[["d1"],["d1"],[],[]],"check":"three reverse dependencies","expected":[["d1"],["d1"],["d1"],["d1"]],"passed":false},{"actual":[["d1"],["d1"],[]],"check":"cycle converges","expected":[["d1"],["d1"],["d1"]],"passed":false},{"actual":[["d1"],[]],"check":"isolated nodes","expected":[["d1"],[]],"passed":true},{"actual":[["d1"]],"check":"self edge","expected":[["d1"]],"passed":true},{"actual":[],"check":"no nodes","expected":[],"passed":true},{"actual":[["d1"],["a"],["a","d1"]],"check":"union incoming","expected":[["d1"],["a"],["a","d1"]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"three reverse dependencies\", \"actual\": [[\"d1\"], [\"d1\"], [], []], \"expected\": [[\"d1\"], [\"d1\"], [\"d1\"], [\"d1\"]], \"passed\": false}, {\"check\": \"cycle converges\", \"actual\": [[\"d1\"], [\"d1\"], []], \"expected\": [[\"d1\"], [\"d1\"], [\"d1\"]], \"passed\": false}, {\"check\": \"isolated nodes\", \"actual\": [[\"d1\"], []], \"expected\": [[\"d1\"], []], \"passed\": true}, {\"check\": \"self edge\", \"actual\": [[\"d1\"]], \"expected\": [[\"d1\"]], \"passed\": true}, {\"check\": \"no nodes\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"union incoming\", \"actual\": [[\"d1\"], [\"a\"], [\"a\", \"d1\"]], \"expected\": [[\"d1\"], [\"a\"], [\"a\", \"d1\"]], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":39.61,"exit_code":0,"observations":[{"actual":[["d1"],["d1"],["d1"],["d1"]],"check":"three reverse dependencies","expected":[["d1"],["d1"],["d1"],["d1"]],"passed":true},{"actual":[["d1"],["d1"],["d1"]],"check":"cycle converges","expected":[["d1"],["d1"],["d1"]],"passed":true},{"actual":[["d1"],[]],"check":"isolated nodes","expected":[["d1"],[]],"passed":true},{"actual":[["d1"]],"check":"self edge","expected":[["d1"]],"passed":true},{"actual":[],"check":"no nodes","expected":[],"passed":true},{"actual":[["d1"],["a"],["a","d1"]],"check":"union incoming","expected":[["d1"],["a"],["a","d1"]],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"three reverse dependencies\", \"actual\": [[\"d1\"], [\"d1\"], [\"d1\"], [\"d1\"]], \"expected\": [[\"d1\"], [\"d1\"], [\"d1\"], [\"d1\"]], \"passed\": true}, {\"check\": \"cycle converges\", \"actual\": [[\"d1\"], [\"d1\"], [\"d1\"]], \"expected\": [[\"d1\"], [\"d1\"], [\"d1\"]], \"passed\": true}, {\"check\": \"isolated nodes\", \"actual\": [[\"d1\"], []], \"expected\": [[\"d1\"], []], \"passed\": true}, {\"check\": \"self edge\", \"actual\": [[\"d1\"]], \"expected\": [[\"d1\"]], \"passed\": true}, {\"check\": \"no nodes\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"union incoming\", \"actual\": [[\"d1\"], [\"a\"], [\"a\", \"d1\"]], \"expected\": [[\"d1\"], [\"a\"], [\"a\", \"d1\"]], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}