本终点固定min-even。主线用一份确定监控器建立真正的输入/输出博弈，完成递归求解、控制器与反策略；选修再核LAR、Safra和进展度量。题面里的控制器看得到当前输入，不得借用下一轮输入。
第一题：确定监控器与完整行动表
环境每轮先给req、ready两个比特，控制器再给grant。目标为
公平前提失败只解除响应义务，安全义务始终保留。初始pending=false，读完每个联合字母后更新
若grant且非ready，永久进入D；否则pending′假时到Q，pending′真且ready假时到P₀，pending′真且ready真时到P₁。优先级为Q:0、P₀:2、P₁:1、D:1。
构图时Q、P₀、P₁为环境顶点；对每个q和输入i∈{00,01,10,11}，建控制器顶点qᶦ，输入比特按(req,ready)排列。环境边q→qᶦ标i，控制器边按grant标0或1，中间顶点优先级一律3。
四状态乘四种输入的朴素展开原有4×(1+4)=20个顶点。这里把D及其四个输入中间顶点合成一个优先级1的自环陷阱D，得到3×5+1=16个顶点。因为一旦进D，所有输入输出都永久拒绝，这个合并不改变任何获胜结论。D上的自环概括所有后续动作。
问题：写出12个控制器顶点的两条动作边，并解释为什么保留动作标签，即使两条边终点相同。
解答
| 控制器顶点 | grant=0 | grant=1 |
|---|---|---|
| Q⁰⁰ | Q | D |
| Q⁰¹ | Q | Q |
| Q¹⁰ | P₀ | D |
| Q¹¹ | P₁ | Q |
| P₀⁰⁰ | P₀ | D |
| P₀⁰¹ | P₁ | Q |
| P₀¹⁰ | P₀ | D |
| P₀¹¹ | P₁ | Q |
| P₁⁰⁰ | P₀ | D |
| P₁⁰¹ | P₁ | Q |
| P₁¹⁰ | P₀ | D |
| P₁¹¹ | P₁ | Q |
另有12条环境输入边及D自环，所以按动作边计为12+24+1=37条。Q⁰¹的两个输出都到Q，若只保存无标签简单图，可合并为36条不同端点边；提取实现时仍须知道选择的是grant=0还是1，不能从同一终点猜输出。
在从未进入D的运行中，Q无限出现等价于请求没有永久拖欠。若Q只有限出现，之后一直pending：ready无限则P₁无限、最小色1拒绝；ready有限则最终只到P₀、最小色2接受。D自环独立惩罚任何一次非法授权。这证明监控器识别给定公式，而非错误地把全部义务都放进环境假设的后件。
第二题：在16顶点图上执行Zielonka
按Zielonka的min-even递归求解，不先猜控制器。定义以下集合简记：
问题：验证A₀是Even到Q的吸引域，列两次顶层递归及全部非空子调用的结果。
解答
最小色0只在Q，故p=Even。A₀中的中间顶点都有一个输出直接到Q；其余中间顶点没有这样的边。P₀、P₁归环境，它们可选择ready=0的输入逃开A₀，因此不被加入；Q作为目标已经在内。故Attr₀(Q)=A₀。
第一次剩余图为H={D,P₁}∪Z。它的最小色1出现在D、P₁，Odd吸引域就是{D,P₁}：剩余控制器顶点都有去P₀的出口，P₀在H中只剩ready=0输入。
去掉{D,P₁}后是Z，最低色2在P₀，Even可以从所有Z顶点吸引到P₀，故Even赢全部Z。回H取Even吸引域，P₁的所有保留输入后继也都在Z，于是B=Z∪{P₁}；余下{D}由Odd在1自环获胜。因此首次递归准确返回：H中只有D由Odd胜，其余由Even胜。
回16顶点原图计算Attr₁({D})。任何控制器顶点都保留一个非D输出，没有新的点被强迫吸入；任何环境顶点也没有直接到D的边。因此顶层B={D}。
第二次递归G∖{D}再次取A₀，剩余H′={P₁}∪Z。H′去掉Odd目标P₁后是Z，由Even赢；回H′的Even吸引域为整个H′，所以H′全部由Even赢。此时顶层首次子结果的对手区为空，剩余15顶点全部归Even。
| 非空调用 | 第一个吸引域 | 首次子调用结果 | 第二步或返回 |
|---|---|---|---|
| G，全16点 | A₀ | Odd= | B={D}，再解G∖ |
| H={D,P₁}∪Z | Even=Z | B={P₁}∪Z，再解 | |
| Z | Z | 空图 | Even=Z |
| 空图 | Odd= | ||
| G∖ | A₀ | Even=H′，Odd为空 | Even全15点 |
| H′={P₁}∪Z | Even=Z | B=H′，余下空图 | |
| Z，再次出现 | Z | 空图 | Even=Z |
最终
第三题：控制器与两种失败接口
从第二题提取输出，并比较两种改动：一是硬件禁止grant=1，二是改成Moore时序，先输出后看到输入。给出获胜控制器或能响应其实际选择的环境反策略。
解答
选择以下Mealy输出：ready=0一律grant=0；ready=1时，若当前是P₀/P₁或req=1，则grant=1，否则grant=0。这就是两记忆状态的pending控制器。Q对应pending=false，P₀/P₁可合并为pending=true；它们的颜色区别用于监控历史，不是控制逻辑必须保留的额外一位。
安全性由输出式直接保证。只要某请求尚未回答，pending就保持真；GFready保证未来某轮ready，届时授权并清除欠账。该策略满足所有环境输入下的完整条件式，而不是只通过表中一条示例路径。
若禁止grant=1，环境始终输入(req,ready)=(1,1)。控制器只能输出0，监控器从Q到P₁后永久留P₁；环境公平成立，响应失败。从Q这一真正的初态已经不可实现，不只是在已坏的D上失败。
Moore接口中，环境一直req=true；见本轮输出grant=0就给ready=true，见grant=1就给ready=false。一旦授权，立即进入D；如果始终不授权，则ready始终true而永久欠请求，停留奇色。若希望反策略在出现非法授权后也显式维持公平，可在首次非法授权后改为永远ready=true；安全已被破坏，且GFready仍成立。
Q为Mealy可实现、Moore不可实现，同一公式在两种时序中有不同答案。反策略必须在它实际能观察输出的Moore回合中作选择，不能在Mealy版本里偷看尚未输出的grant。
第四题：同一个无限字的Muller、LAR与Rabin检查
取Q={a,b,c}，确定转移为读x就到x，接受族F={{a,b},{b,c}}。LAR初始排列abc，使用正文min-even公式：旧命中位置k的前缀在F时输出2(3−k)，否则再加1。
问题：对
解答
第一个字的Inf集合为{b,c}，Muller接受。前两个c先给命中位置3与1，可能输出1与5；后续读b、c后，排列最终在bca与cba之间交替，命中位置2且前缀总为{b,c}，无限输出2。因此LAR也接受，有限前缀中的1无关。
第二个字最终每次命中位置3，前缀为不在F中的{a,b,c}，无限输出1，LAR与Muller都拒绝。
min-even可写为两对Rabin：E₀=∅、F₀={优先级0顶点}；E₂={优先级0或1顶点}、F₂={优先级2顶点}。第一对处理0无限；第二对处理0、1都有限而2无限。若求语言补且自动机确定完整，Streett应把每对坐标交换成(F₀,E₀)、(F₂,E₂)，不能只换条件名称。
第五题：Safra名字与绿色为何缺一不可
给NBA：初态p、F={f}，p在a和b上都到{p,f}，f在a上到{f}，在b上无后继。名字池1到5，原树先序分配本轮开始时未使用的最小名字。
问题：写出aa及bb后的树，再判断
解答
首个a或b后均为根1:{p,f}、孩子2:{f}。第二个a使孩子2保留f；根的新孩子3被老2去重，2的新孩子4覆盖2，因此2变绿并删4。aa后仍为根1:{p,f}、孩子2*:{f}。
第二个b使旧孩子2标签为空，新孩子必须另取名字3，得到根1:{p,f}、孩子3:{f}，没有绿色。沿
两个输入的普通子集序列都从{p}变成{p,f}后不变。在
第六题：核验小进展度量与反策略边界
采用q/r/b/u四顶点度量例：q由Even行动、优先级1、后继r/b；r由Even行动、优先级0、后继q；b由Odd行动、优先级1、自环；u由Odd行动、优先级2、后继q/b。奇色1计数上界2。
问题：验证μ(q)=1、μ(r)=0、μ(b)=μ(u)=⊤是固定点，提取双方各一份策略。能否把所有⊤顶点任意选一条⊤后继视为一般Odd策略提取法？
解答
q的r后继需要Prog(0,1)=1，b后继需要⊤，Even取最小得到1。r优先级0对有限1重置为0。b从⊤提升仍⊤，u在q的有限值和b的⊤之间取最大为⊤，所以整轮不变。
Even取q→r、r→q，循环最小色0；Odd取u→b、b→b，循环最小色1。这份具体反策略可以直接验证，但⊤本身没有记录所有Odd顶点该怎样推进，不能据此证明任意⊤内部选择都获胜。一般应另提取反策略，或交换玩家并把优先级加1后再求有限度量。
验收清单
- 优先级约定、输入输出先后、monitor读字位置保持一致
- 16顶点来自明确的D陷阱合并；输出标签不因相同终点而丢失
- 第二次吸引域在正确的原当前图计算，子图删除后仍总有后继
- 获胜控制器覆盖所有环境路径，失败证书是可执行环境策略
- 接受条件转换在完整无限后缀上等价，不用有限好前缀代替
- 名字、绿色、有限度量与⊤分别承担的证明义务清楚可核对