有点简略，如果你已经知道时间自动机和 UPPAAL 就完全可以看懂…… 哎我尽量 self-contained，目标是让所有读者至少能看懂九成……
（如果想了解时间自动机和 UPPAAL，可以看一看 [译]时间自动机：语义，算法和工具，不看也行 ）
1
昨天晚上 ZH 同学在群里发了张图：
走迷宫，但是经过的圆点必须红蓝交替。
2
不一会，LJ 同学给出了一个解：
WX 等同学表示 LJ 真会玩。
HK 同学给出了另一个解，但我没看懂文字描述?
3
早上起来，发现昨晚 JSK 同学一点多的时候说了一句：
这不是形式化验证问题吗？
我有点兴奋，于是想到以前用过的模型检测工具 UPPAAL 来解一下。UPPAAL 有 GUI，有模拟器，有属性验证器，很适合这道题。
4
于是就去建模了。
考虑了时间自动机的 Location（i.e. 圆圈）应该表示题目中的”十字路口“还是”圆点“。结论是十字路口。
考虑了”被没有圆点的道路连接的十字路口 是否应该合并成一个 Location“的问题。经过失败的尝试：
结论是不应该合并。
在添加任何约束条件之前，模型是这样的：
考虑了“用 Channel + Synchronization 还是 变量 + Guard 来描述红蓝交替这个约束”的问题。结论是 Channel + Synchronization。因为在自动机进程图里有一大堆 Edge；在每个 Edge 上标记 r? 比 color==1 要简短和清晰……
于是，加了一个”乌鸦“自动机，用来发出信号；让原自动机接收信号。建模完的样子：
经过几次用模拟器 Debug，查了一些“忘写 Edge 的 Sync”的错误；否定了把乌鸦自动机的 Location 设为 Committed / Urgent 的想法；
然后用验证器验证这个属性：
E<> rbp.T
即：从系统初始状态出发，存在（E）一条执行路径，使得自动机 rbq 可以（<>）到达 Location T。
（在不涉及 时钟/变量 的时候，时间自动机系统的状态就是所有自动机的 Location 组成的向量/元组。）
好的，这俨然是个图论问题……（有什么模型检测问题不是图论问题吗（有什么问题不能转（juǎn）化成图论问题吗））
验证通过！然后设置 Diagnostic Trace 策略为 Shortest，再验证一次，输出执行路径：
这就是 LJ 同学的解嘛！好棒好棒的！
大致就是这样。
Appendix
-
建模时烦人的事：加 Edge；拖动 Edge 的控制点到美观的位置；给 Edge 加 sync；拖动 sync 文字（r? 和 b?）到美观的位置；给 Location 取名字……
必须有一门迷宫建模的 DSL 了！
（iOS 和 OS X 的）微信里发 GIF 动不起来？Bad。
群里聊这个题的时候我画了个图，解释 UPPAAL 在世界中的位置（啊，窝好喜欢“我们在世界中的位置”这个词……）：
对不对呢？感觉有必要跟贺师和罗师求教一下……UPPAAL 下载：http://www.it.uu.se/research/group/darts/uppaal/download.shtml
下载需要填个表格…… 不用太在意。
我用的是 OS X 4.0.13。刚才又下了一下，不能用…… Windows 4.0.14 版却能用……
模型文件：http://7tsy1b.com1.z0.glb.clouddn.com/program%2Fuppaal_red_blue_puzzle.xml
属性文件：http://7tsy1b.com1.z0.glb.clouddn.com/program%2Fuppaal_red_blue_puzzle.q
