about 1 year ago

有点简略,如果你已经知道时间自动机和 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

  1. 建模时烦人的事:加 Edge;拖动 Edge 的控制点到美观的位置;给 Edge 加 sync;拖动 sync 文字(r? 和 b?)到美观的位置;给 Location 取名字……

    必须有一门迷宫建模的 DSL 了!
    
  2. 录屏生成 GIF 的软体是 LICEcap,有 Windows 和 OS X 版,好使。从 小众软件这里看到的。

  3. (iOS 和 OS X 的)微信里发 GIF 动不起来?Bad。

  4. 群里聊这个题的时候我画了个图,解释 UPPAAL 在世界中的位置(啊,窝好喜欢“我们在世界中的位置”这个词……):


    对不对呢?感觉有必要跟贺师和罗师求教一下……

  5. 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

 
about 1 year ago

軟體工程師 = 軟體の工程師

 
about 1 year ago

Abstract

在糅杂了北邮和清华的教室里, 见到了初中到博士阶段的同学...

Background

昨晚考完了算法(学得一泡污). 结束了博一上学期仅有的两门考试…(其他很多用大作业结课嗯 不是我偷懒不选课…)

正文

  1. 我走进北邮宏福教一303, 准备上一门数值xx课. 但是QZ老板走进来, 要上电子商务概论课. “同学们, 改教室了. 电商课在这上, 数值xx课在斜对面教室上. 电脑排教室排出来的. 你看, 解释器是可以有毛病的; PCI = Program Counter Interpreter 是一种解释器; PCI 可以有毛病; PC 是 PCI 的一部分; PC 可以有毛病; PC = 电脑; 电脑有毛病导致排的教室有问题."

    (“可以有毛病”比”容易出问题”清晰/disambiguous… “这个知识点可能出问题")

  2. 我换到303斜对面教室(在我的脑海中, 那个教室摆满电路板). 进入之后, 看起来像(清华2015秋的)高等数值分析教室, 也像303, 也像很多阶梯教室 (也像2016-01-11算法的考场…). 我找准一个位子坐下, touch到三个初中同学: MX坐左边, 我俩”wo4cao!”, 拍背; YX坐右边, 我俩”Hi!”, 拍肩; WL从前面经过, 我俩”Hi!”.

  3. 数值xx这次似乎是期末习题课, 老师板书了若干题, 第一道是 “… 使 i^# j^# k^# = 0. 注: 左边 = i^{#\\向左倾斜{#1}} j^{#\\向左倾斜{#2}} k^{#\\向左倾斜{#3}}.”

  4. 右边变成了老四GR, 他是上这个课的, 我俩一起开始做题.

  5. 前边变成了高中班长XH, 他是要上电商课的, 也是被坑走错了教室, 我拉住他不让走, 说一起听. 他坐下了.

  6. 老师来看我做的题, 我:”啊老师我没选这课, 是来随便听听…” 老师: “哦, 你写的篇幅确实不够做出来..."

  7. Duang! 切换了场景, 换成了一个心理咨询室, 有沙发, 架子上摆着各种减压小玩具的那种. 旁边有做泥塑的/陶艺工作台. 军乐队少年LH在捏(?)泥人. 做完之后烤干, 烤干之后上色. 肥肠精美! 泥人很像某网红哲学生井越的头像[1]! 如图1. 惊了.


图1 井越的头像

Conclusion

我梦见的人名都是俩字的.

Reference

[1] http://weibo.com/u/5824686667 accessed at 2016-01-12 08:34:40

 
over 1 year ago

我第一次见到 X 大哥的时候, 他正独自坐在教一 5 楼空旷的实验室里, 用咔咔作响的黑轴键盘写代码, Emacs 的黑底 Buffer 显示在笔记本屏幕和一个外接显示器上, 每段代码的结尾有一串 ))). 他说他在用 Common Lisp 写一个 Python 的解释器. 旁边的桌上有画满了道道、写满了笔记、翻得卷边的《计算机程序的构造和解释》、《算法导论》和打印的《Common Lisp the Language, 2nd Edition》. 那是 2012 年的秋冬之交.

 
over 1 year ago

…… 标题一点都没谦虚。


1 - LoveLive and Pony


2 - 或且非