
digraph G {
  graph [
    bgcolor="white", pad="0.28", nodesep="0.38", ranksep="0.58",
    fontname="WenQuanYi Zen Hei", fontcolor="#17212B", fontsize=24,
    labelloc="t", labeljust="l"
  ];
  node [
    shape=box, style="rounded,filled", margin="0.18,0.12",
    fontname="WenQuanYi Zen Hei", fontcolor="#17212B", fontsize=12,
    color="#CBD5E1", penwidth=1.3, fillcolor="#F8FAFC"
  ];
  edge [
    fontname="WenQuanYi Zen Hei", fontcolor="#64748B", fontsize=10,
    color="#64748B", penwidth=1.5, arrowsize=0.75
  ];

  label="图 1-0  Native concolic 与 Continuation/CAS 两条执行流";
  rankdir=TB;

  seed [label="输入种子", fillcolor="#FEF3C7", color="#D97706"];

  subgraph cluster_native {
    label="A. 经典 native concolic（默认）";
    color="#5EEAD4"; style="rounded,filled"; fillcolor="#F0FDFA";
    tag [label="TAG_WORK\n传输内容对象", fillcolor="#CCFBF1", color="#0F766E"];
    proc [label="新起 SymCC/SymSan\n目标进程", fillcolor="#FFEDD5", color="#C2410C"];
    b3n [label="B3 分支兴趣过滤\n严格/乐观求解", fillcolor="#FFEDD5", color="#C2410C"];
    shown [label="AFL showmap\nB2 本地判新", fillcolor="#DBEAFE", color="#2563EB"];
    tag -> proc -> b3n -> shown;
  }

  subgraph cluster_live {
    label="B. Continuation / CAS 状态级执行（opt-in）";
    color="#C4B5FD"; style="rounded,filled"; fillcolor="#F5F3FF";
    cas [label="初始 CAS checkpoint\nfenced state lease", fillcolor="#EDE9FE", color="#6D28D9"];
    restore [label="Worker 恢复 continuation\n有界执行与分叉", fillcolor="#EDE9FE", color="#6D28D9"];
    frontier [label="halted states +\nresumable frontier checkpoints", fillcolor="#EDE9FE", color="#6D28D9"];
    commit [label="Master 校验 fence\ncommit 并重新入队", fillcolor="#EDE9FE", color="#6D28D9"];
    cas -> restore -> frontier -> commit;
    commit -> restore [constraint=false, style=dashed, color="#6D28D9", label="下一 lease"];
  }

  triage [label="共同出口\n目标重放 → AFL bitmap triage → B1", fillcolor="#DBEAFE", color="#2563EB", penwidth=2.4];
  queue [label="被接受候选\n写入 helper / AFL 同步目录", fillcolor="#DCFCE7", color="#15803D"];
  seed -> tag [label="默认"];
  seed -> cas [label="SYMCC_LIVE_*", color="#6D28D9"];
  shown -> triage [label="TAG_RESULT"];
  commit -> triage [label="SAT 输入候选", color="#6D28D9"];
  triage -> queue;
  invariant [shape=note, label="共同不变量\nContinuation 候选也不能绕过\n目标重放和 B1 新颖性仲裁", fillcolor="#FEE2E2", color="#B91C1C"];
  triage -> invariant [style=dotted, arrowhead=none];

}
